As an example, consider the square function, square(x)=x*x. Suppose we don't care about the name and just want to talk about the function in the abstract. The lambda calculus gives us the syntax for such discussions. We express the square function as
- Every variable is a lambda term.
- If M is a lambda term then (λx.M) is a lambda term.
- If M and N are lambda terms then MN is a lambda term.
Free variables are those not closed off by a λ. For example in λy.xy the variable x is free and y is bound.
We use the notation M[x:=E] means replace every occurrence in the lambda term M of the free variable x by the lambda term E. There should not be any free variables in E that are bound in M as this could cause confusion.
There are two basic operations:
(renaming variables formally called α-conversion) λx.M to λy.M[x:=y] where y does not occur in M
(function evaluation formally called β-reduction) λx.M(E) to M[x:=E]
Church and Rossner have shown that if you have a complicated lambda-term it does not matter what order the β-reduction operations are applied.
What can you do with just these simple operations? You get the same power as Turing machines! It's instructive to see this connection and we'll go over the proof over several posts in the future.