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).
the function
has the following derivation.