lambda calculus

the -calculus consists of a set of objects called -terms and some rules for manipulating them. it was originally designed to capture formally the notions of functional abstraction and functional application and their interaction.

the -calculus has had a profound impact on computing. one can see the basic principles of the -calculus at work in the functional programming language lisp and its more modern offspring SCHEME and DYLAN.

in mathematics, -notation is commonly used to represent functions. the expression denotes a function that on input computes . to apply this function to an input, one substitutes the input for the variable in the body and evaluates the resulting expression.

for example, the expression might be used to denote the successor function on natural numbers. to apply this function to the input 7, we would substitute 7 for in the body and evaluate: in the programming language DYLAN, one would write

(method (x) (+ x 1))

for the same thing. the keyword method is really in disguise. if you typed

((method (x) (+ x 1)) 7)

at a DYLAN interpreter, it would print out 8.

for another example, the expression denotes the composition of the functions and ; that is, the function that on input applies to , then applies to the result. the expression

denotes the function that takes functions and as input and gives back their composition . In DYLAN one would write

(method (f)
  (method (g)
    (method (x) (f (g x)))))

to see how this works, let's apply eq-lambda-calc-1 to the successor function twice.

we use different variables in the successor functions below for clarity. the symbol denotes one substitution step.

we could have substituted for in the second step or for in the third; we would have arrived at the same final result.

functions represented by -terms have only one input. a function with two inputs that returns a value is modeled by a function with one input that returns a function with one input that returns a value . The technical term for this trick is currying (after Haskell B. Curry).