# Lambda Calculus

Lambda calculus is minimal programming language that's Turing complete. In lambda calculus, everything is an anonymous function. The language was invented by Alonzo Church.

## Grammar

Expression -> Variable | Application | Abstraction Variable -> ID Application -> (Expression Expression) Abstraction -> λID.Expression

Or condensed as:

e -> x | (e1 e2) | λx.e

## Definitions

- A lambda
**abstraction**`λx.e`

is a definition of an anonymous function capable of taking a single input`x`

and substituting it into (and thus evaluating) the expression`e`

. - An
**application**`(e1 e2)`

applies the`e1`

function to the`e2`

value, that is, it represents the act of calling function`e1`

on input`e2`

to product`e1(e2)`

. - In
`λx.e`

,`e`

is**bound**in`e`

(i.e.`x`

would have a value associated with it). - A
**free variable**is a variable that is not bound. Formally:FV(x) = {x} FV((e1 e2)) = FV(e1) U FV(e2) FV(λx.e) = FV(e) - {x}

- A
**combinator**is an expression with no free variables. - A
**value**is an expression in final form (can't be reduced any more), i.e. an abstraction. - An expression in the form
`(x e)`

is**stuck**.

## Reduction

The meaning of lambda expressions is defined by how expressions can be reduced. Evaluation consists of reducing until either one can't anymore or there is a problem. There are three kinds of reduction: α-conversion, β-reduction, and η-conversion.

### α-conversion

Allows bound variable names to be changed (effectively renaming a variable):
`e[b/a]`

means `e`

but with every occurrence of `a`

replaced with
`b`

. α-conversion of `λx.x`

might yield `λy.y`

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

). Terms
that differ only by α-conversion are called α-equivalent.

### β-reduction

Captures the idea of function application. In operational semantics, ```
(λx.M
N) -> M[N/x]
```

.

## Recursion

Since recursion consists of calling the function within itself, the technique can be tricky because every function is anonymous (that is, it doesn't have a name). To simulate recursion, make a function that you want to be recursive take an extra argument that will be that function itself, the write a wrapper that passes that function as the second argument. For example:

Fact = λn.λf.If (IsZero n) c1 (Times n (f (Pred n) f)) Factorial = λn.Fact n Fact

## Examples

The simplest function is the identity function `λx.x`

, it takes something and
returns that same thing.

### Booleans

True = λt.λf.t False = λt.λf.f If = λl.λm.λn.((l m) n)

### Pairs

Pair = λf.λs.λb.((b f) s) First = λp.(p True) Second = λp.(p False)

### Whole Numbers (Church Numerals)

c0 = λz.λs.z c1 = λz.λs.(s z) c2 = λz.λs.(s (s z)) cn = λz.λs.(s (s ... (s z))) IsZero = λm.((m True) (λx.False))