Notes:Lambda calculus

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

Lambda terms

We define [ilmath]\lambda[/ilmath]-terms as follows:
Let the following be given:

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

The set of expressions called [ilmath]\lambda[/ilmath]-terms is defined inductively as follows:

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

Examples

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