Difference between revisions of "Notes:Lambda calculus"

Revision as of 19:46, 11 August 2015

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:^[1]
Let the following be given:

• Variables: an infinite sequence of expressions, [ilmath]v_1,\cdots,v_n\cdots[/ilmath] ^{[Note 1]}
• 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^[1]
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

Notes

1. ↑ The book uses [ilmath]v_0,v_{00},v_{000},\cdots[/ilmath] for some yet unknown reason

References

1. ↑ ^{1.0 1.1} Lambda Calculus and Combinators, an introduction, J. Roger Hindley and Jonathan P. Seldin