Slide 12.1: The lambda calculus
Slide 12.3: Syntax of the lambda calculus
Home

Concepts and Examples

The mathematical concept of a function expresses dependence between two quantities, one of which is given (the independent variable, argument of the function, or its “input”) and the other produced (the dependent variable, value of the function, or “output”). In other words, a function is a mapping from the elements of a domain set to the elements of a codomain set given by a rule—for example, 
     cube: Integer → Integer    where cube(n) = n3
Church's lambda notation allows the definition of an anonymous function, that is, a function without a name: 
     λn . n3
defines the function that maps each n in the domain to n3. We say that the expression represented by λn.n3 is the value bound to the identifier “cube.” The number and order of the parameters to the function are specified between the λ symbol and an expression. For instance, the “add-two” function f such that f(x) = x + 2 would be expressed in lambda calculus as 
     λx . x + 2     or     λy . y + 2
the name of the formal parameter is immaterial and the application of the function f(3) would be written as 
     (λx . x + 2) 3
The expression n2+m is ambiguous as the definition of a function rule: 
     (3, 4) |→ 32 + 4 = 13   or   (3, 4) |→ 42 + 3 = 19
Lambda notation resolves the ambiguity by specifying the order of the parameters: 
     (λn.λm.n2+m) 3 4 = 13   or   (λm.λn.m2+n) 4 3 = 19

Demonstration