# 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`_{1}.exp

if the identifier `name`

!=`name`_{1}

and `name`

is free in `exp`

.
`name`

is free in `E`_{1}E_{2}

if `name`

is free in `E`_{1}

or if it is free in `E`_{2}

.

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

`name`

is bound in `λname`_{1}.exp

if the identifier `name`

=`name`_{1}

or if `name`

is bound in `exp`

.
`name`

is bound in `E`_{1}E_{2}

if `name`

is bound in `E`_{1}

or if it is bound in `E`_{2}

.