There is a considerable body of
programming idioms for lambda calculus. Many of these were originally developed in the context of using lambda calculus as a foundation for
programming language semantics, effectively using lambda calculus as a
low-level programming language. Because several programming languages include the lambda calculus (or something very similar) as a fragment, these techniques also see use in practical programming, but may then be perceived as obscure or foreign.
Named constants In lambda calculus, a
library would take the form of a collection of previously defined functions, which as lambda-terms are merely particular constants. The pure lambda calculus does not have a concept of named constants since all atomic lambda-terms are variables, but one can emulate having named constants by setting aside a variable as the name of the constant, using abstraction to bind that variable in the main body, and apply that abstraction to the intended definition. Thus to use to mean
N (some explicit lambda-term) in
M (another lambda-term, the "main program"), one can say :
M N Authors often introduce
syntactic sugar, such as , to permit writing the above in the more intuitive order :
N M By chaining such definitions, one can write a lambda calculus "program" as zero or more function definitions, followed by one lambda-term using those functions that constitutes the main body of the program. A notable restriction of this is that the name may not be referenced in
N, for
N is outside the scope of the abstraction binding , which is
M; this means a recursive function definition cannot be written with . The construction would allow writing recursive function definitions, where the scope of the abstraction binding includes
N as well as
M. Or self-application a-la that which leads to combinator could be used.
Recursion and fixed points Recursion is when a function invokes itself. What would a value be which were to represent such a function? It has to refer to itself somehow inside itself, just as the definition refers to itself inside itself. If this value were to contain itself by value, it would have to be of infinite size, which is impossible. Other notations, which support recursion natively, overcome this by referring to the function
by name inside its definition. Lambda calculus cannot express this, since in it there simply are no names for terms to begin with, only arguments' names, i.e. parameters in abstractions. Thus, a lambda expression can receive itself as its argument and refer to (a copy of) itself via the corresponding parameter's name. This will work fine in case it was indeed called with itself as an argument. For example, will express recursion when
E is an abstraction which is applying its parameter to itself inside its body to express a recursive call. Since this parameter receives
E as its value, its self-application will be the same again. As a concrete example, consider the
factorial function , recursively defined by : . In the lambda expression which is to represent this function, a
parameter (typically the first one) will be assumed to receive the lambda expression itself as its value, so that calling it with itself as its first argument will amount to the recursive call. Thus to achieve recursion, the intended-as-self-referencing argument (called here, reminiscent of "self", or "self-applying") must always be passed to itself within the function body at a recursive call point: : ::: with to hold, so and : and we have : Here becomes
the same inside the result of the application , and using the same function for a call is the definition of what recursion is. The self-application achieves replication here, passing the function's lambda expression on to the next invocation as an argument value, making it available to be referenced there by the parameter name to be called via the self-application , again and again as needed, each time
re-creating the lambda-term . The application is an additional step just as the name lookup would be. It has the same delaying effect. Instead of having inside itself as a whole
up-front, delaying its re-creation until the next call makes its existence possible by having two
finite lambda-terms inside it re-create it on the fly
later as needed. This self-applicational approach solves it, but requires re-writing each recursive call as a self-application. We would like to have a generic solution, without the need for any re-writes: : ::: with to hold, so and : where ::: so that Given a lambda term with first argument representing recursive call (e.g. here), the
fixed-point combinator will return a self-replicating lambda expression representing the recursive function (here, ). The function does not need to be explicitly passed to itself at any point, for the self-replication is arranged in advance, when it is created, to be done each time it is called. Thus the original lambda expression is re-created inside itself, at call-point, achieving
self-reference. In fact, there are many possible definitions for this operator, the simplest of them being: : In the lambda calculus, is a fixed-point of , as it expands to: : : : : : Now, to perform the recursive call to the factorial function for an argument
n, we would simply call . Given
n = 4, for example, this gives: Every recursively defined function can be seen as a fixed point of some suitably defined higher order function (also known as functional) closing over the recursive call with an extra argument. Therefore, using , every recursive function can be expressed as a lambda expression. In particular, we can now cleanly define the subtraction, multiplication, and comparison predicates of natural numbers, using recursion. When
Y combinator is coded directly in a
strict programming language, the applicative order of evaluation used in such languages will cause an attempt to fully expand the internal self-application (x x) prematurely, causing
stack overflow or, in case of
tail call optimization, indefinite looping. A delayed variant of Y, the
Z combinator, can be used in such languages. It has the internal self-application hidden behind an extra abstraction through
eta-expansion, as (\lambda v.x x v), thus preventing its premature expansion: : Z = \lambda f.(\lambda x.f (\lambda v.x x v)) \ (\lambda x.f (\lambda v.x x v))\ .
Standard terms Certain terms have commonly accepted names: : : : : : : : : is the identity function. and form complete
combinator calculus systems that can express any lambda term - see
the next section. is , the smallest term that has no normal form. is another such term. is standard and defined
above, and can also be defined as , so that . and defined
above are commonly abbreviated as and .
Abstraction elimination If
N is a lambda-term without abstraction, but possibly containing named constants (
combinators), then there exists a lambda-term
T(,
N) which is equivalent to
N but lacks abstraction (except as part of the named constants, if these are considered non-atomic). This can also be viewed as anonymising variables, as
T(,
N) removes all occurrences of from
N, while still allowing argument values to be substituted into the positions where
N contains an . The conversion function
T can be defined by: :
T(, ) :=
I :
T(,
N) :=
K N if is not free in
N. :
T(,
M N) :=
S T(,
M)
T(,
N) In either case, a term of the form
T(,
N)
P is reduced by having the initial combinator
I,
K, or
S grab the argument
P, just like β-reduction of
N P would do.
I returns that argument.
K N throws the argument away, just like
N does when has no free occurrence in
N.
S passes the argument on to both subterms of the application, and then applies the result of the first to the result of the second, just like
MN is the same as
M N. The combinators
B and
C are similar to
S, but pass the argument on to only one subterm of an application (
B to the "argument" subterm and
C to the "function" subterm), thus saving a subsequent
K if there is no occurrence of in one subterm. In comparison to
B and
C, the
S combinator actually conflates two functionalities: rearranging arguments, and duplicating an argument so that it may be used in two places. The
W combinator does only the latter, yielding the
B, C, K, W system as an alternative to
SKI combinator calculus. == Typed lambda calculus ==