> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/340-lambda-calculi/lambda-calculus/lambda-calculus-formal.md).

# Lambda Calculus

## Formal Definition

The syntax of LC defines some expressions (sequence of symbols allowed in LC) as valid and some as invalid. **Lambda term** is a valid LC expression.

These rules give an inductive definition that can be applied to build all syntactically valid lambda terms:

* 0: a variable (e.g. $$x$$) is a valid lambda term
* 1: if $$x$$ and $$M$$ are lambda terms, then $$(\lambda x.M)$$ is a lambda term
* 2: if $$M$$ and $$N$$ are lambda terms, then $$(MN)$$ is a lambda term
* nothing else is a lambda term.

**Variables**\
Above, the zero rule just states that $$x$$ is a lambda term, which would imply that $$x$$ on its own is a lambda term, but that's pretty vague; that $$x$$ alone is obviously not a function, and it couldn't stand for (represent) some other lambda term (that would be external binding). It can only be a **free variable**, meaning we're not seeing the entire expression; we have to zoom out to see the acual binding site for that $$x$$.

, called a *lambda abstraction*. , called an *application* (function application, lambda application).

Application, $$MN$$, associate to the left: $$fxyz$$ is $$((fx)y)z$$

Abstraction, $$\lambda x.M$$, associate to the right: $$\lambda f.xyz$$ $$\lambda f.(xyz)$$

Assume given an infinite set $$\mathcal{V}$$ of variables, denoted by $$x, y, z\dots$$\
The set of lambda terms is given by the following Backus-Naur Form\
($$M$$ and $$N$$ are lambda terms, $$x$$ is a variable):

$$
M, N ::= x \ |\ (MN)\ |\ (\lambda{x}.M)
$$

Traditional definition:

* Assume given an infinite set $$\mathcal{V}$$ of variables
* Let $$A$$ be an alphabet consisting of the elements of $$\mathcal{V}$$ and the special symbols, $$\lambda$$, `.`, `(`, `)`
* Let $$A^∗$$ be the set of strings (finite sequences) over the alphabet $$A$$
* The set of lambda terms is the smallest subset $$\Lambda \subseteq A^∗$$ such that:
  * Whenever $$x\in \mathcal{V}$$ then $$x\in \Lambda$$
  * Whenever $$M,N\in \Lambda$$ then $$(MN)\in \Lambda$$
  * Whenever $$x\in \mathcal{V}$$ and $$M\in \Lambda$$ then $$\lambda{x}.M \in \Lambda$$

Examples:

* Variables: `x`, `y`
* Applications: `xx`, `xy`, `(λx.(xx))(λy.(yy))`
* Abstractions: `λx.x`, `λf.ff`, `λf.(λx.(f(fx)))`
* Abstraction and application: `(λx.x)(2)`, `((λf.f(f))(λx.x+2))(3)`

This, `λx.x+1`, defines an anonymous function that takes a parameter `x` and evaluates (returns) it to `x+1`. This applies this function to the argument 5: `(λx.x+1)(5)`; the 5 replaces the `x` in the function's body, so this expression evaluates to 6.