Notes:Lambda calculus

This is a NOTES page, so it isn't an actual page in the wiki yet!

Lambda terms

We define $\lambda$-terms as follows:
Let the following be given:

• Variables: an infinite sequence of expressions, $v_1,\cdots,v_n\cdots$
• Atomic constants: a sequence of expressions again, that may also be finite or empty

The set of expressions called $\lambda$-terms is defined inductively as follows:

1. All variables and atomic constants are $\lambda$-terms
   • These are known as atoms
2. If $M$ and $N$ are $\lambda$-terms then $(MN)$ is a $\lambda$-term
   • Known as applications
   • this is a short hand for $M(N)$ in our modern terminology
3. If $M$ is any $\lambda$-term and $x$ any variable then $(\lambda x.M)$ is a $\lambda$-term
   • Any such expression is called an abstraction

Examples

• $(\lambda v_0.(v_0v_{00}))$ - a function that $x\mapsto x(v_{00})$ I think