# Definition

The `λ`

calculus consists of a single transformation rule (variable substitution) and a single function definition scheme. It was introduced in the 1930s by *Alonzo Church* as a way of formalizing the concept of effective computability. The `λ`

calculus is universal in the sense that any computable function can be expressed and evaluated using this formalism.

### Expression

```
<expression> := <name> | <function> | <application>
<function> := λ <name>.<expression>
<application> := <expression><expression>
```

A “name”, also called a “variable”, is an identifier which can be any of the letters a, b, c, . . .

The only keywords used in the language are `λ`

and the dot `.`

`λx.x`

An example of a function

This expression defines the * identity* function. The name after the

`λ`

is the identifier of the **argument**of this function. The expression after the dot (in this case a single x) is called the

**body**of the definition.

Functions can be

**applied to**expressions: such as

`(λx.x)y`

, This is the identity function applied to y. **Function applications**are evaluated by substituting the value of the argument x (in this case y) in the body of the function definition,

`(λx.x)y = [y/x]x = y`

## Free and bound variables

we say that a variable `name`

is **free** in an expression if one of the following three cases holds:

`name`

is free in`name`

.`name`

is free in`λname`

if the identifier_{1}.exp`name`

!=`name`

and_{1}`name`

is free in`exp`

.`name`

is free in`E`

if_{1}E_{2}`name`

is free in`E`

or if it is free in_{1}`E`

._{2}

And is **bound** if one of two cases holds:

`name`

is bound in`λname`

if the identifier_{1}.exp`name`

=`name`

or if_{1}`name`

is bound in`exp`

.`name`

is bound in`E`

if_{1}E_{2}`name`

is bound in`E`

or if it is bound in_{1}`E`

._{2}