Difference between revisions of "Lambda-calculus"
m (→Introduction.: links) |
m (→Currying.: link) |
||
Line 11: | Line 11: | ||
==Currying.== | ==Currying.== | ||
− | Although abstraction is provided only to form unary functions, also functions of more arguments can be represented in lambda calculus by iterated abstraction. For example <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700058.png" /> is a term such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700059.png" />. (To make notation easier, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700060.png" /> stands for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700061.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700062.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700063.png" />. Then one may write <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700064.png" />.) The method is due to M. Schönfinkel [[#References|[a9]]] but is called currying after H.B. Curry who made it popular. | + | Although abstraction is provided only to form unary functions, also functions of more arguments can be represented in lambda calculus by iterated abstraction. For example <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700058.png" /> is a term such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700059.png" />. (To make notation easier, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700060.png" /> stands for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700061.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700062.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700063.png" />. Then one may write <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700064.png" />.) The method is due to M. Schönfinkel [[#References|[a9]]] but is called [[currying]] after H.B. Curry who made it popular. |
==Representing computations.== | ==Representing computations.== |
Revision as of 18:23, 19 December 2014
lambda calculus.
Introduction.
The lambda calculus was introduced in 1932–1933 by A. Church (1903-1995) as part of a theory intended as a foundation for mathematics. This foundational theory consisted of a part dealing with logical symbols and rules and a part dealing with algorithms operating on these symbols. After it was shown by S.C. Kleene and J.B. Rosser [a7] that this foundational system was inconsistent, the part dealing with algorithms only was isolated as the (type-free) lambda calculus. It turned out to be quite successful in capturing the intuitive notion of computable function. Kleene [a6] showed that exactly the recursive functions (cf. Recursive function) are lambda definable in the sense given below. Then A.M. Turing [a10] introduced his machines (cf. Turing machine) and showed that Turing computable and lambda definable are equivalent notions. These are arguments for the Church–Turing thesis that the intuitive notion of computable is correctly formalised as lambda definable, Turing computable or recursive (cf. also Church thesis). Although many programming languages are based on the computational model of Turing (imperative programming), presently the model of Church enjoys a lot of attention in the form of functional programming.
Lambda terms.
Let be an infinite set of variables. The set of lambda terms, notation
, is the least set satisfying: if
, then
; if
, then
; if
and
, then
. The term
has as intended meaning:
considered as function applied to
considered as argument;
stands for the intuitive function that assigns to
the value
(possibly containing
). One uses
for syntactic equality between terms. So
and
. Examples of
-terms are:
, the identity;
, the function with constant value
; and
, the function with constant value
. Self-application is allowed:
is a correct
-term. In the expression
the occurrences of the variable
are said to be bound by
. If a variable occurrence is not bound, then it is said to be free in
. A
-term
is closed if
. E.g. in
the variable
occurs free and bound and
occurs free;
is a closed term. Terms that differ only in the names of bound variables are identified; e.g.
.
Conversion.
Following the intended meaning of the lambda expressions, the following so-called -rule is postulated as axiom:
, or, more generally,
, where the right-hand side stands for the result of substituting
for the free occurrences of
in
. When performing a substitution
, care should be taken that no free variable in
becomes bound. This can be accomplished by renaming all bound variables of
. E.g.
. If an equation
is provable from the
-rule alone, then one says that
is convertible to
.
Currying.
Although abstraction is provided only to form unary functions, also functions of more arguments can be represented in lambda calculus by iterated abstraction. For example is a term such that
. (To make notation easier,
stands for
and
for
. Then one may write
.) The method is due to M. Schönfinkel [a9] but is called currying after H.B. Curry who made it popular.
Representing computations.
From the -rule one can prove the following fixed-point theorem. For all
-terms
there exists a
-term
such that
. (Indeed, a proof is as follows. Take
and
. Then
.) This result will be used to represent recursion. Write
and
. Define for
(the set of natural numbers) the
-term
. The
are called Church numerals. A function
is said to be
-definable if there exists a
-term
such that for all
one has
. This definition is extended to functions of more arguments by requiring e.g.
. Integer addition is
-definable using the term
. The predecessor function is
-defined by
. Write
for
. Write
and
. Then "i fBthenXelseY" can be represented by
. Write
. Then
and
. Now suppose
is defined by recursion, e.g.
,
. Then it is possible to
-define
as follows. One wants an
such that
. This holds if
.
. Now
can be found using the fixed-point theorem. In a similar way minimalization (searching) can be represented by
-terms.
Reduction strategies.
If
-defines a function
, then
can be computed by evaluating
. Several strategies can be used in order to evaluate this
-term by giving priorities to the subexpressions
to be rewritten to
. (This replacement is called reduction.) If first the innermost such expressions are computed, then one has eager evaluation; if the outermost expressions are treated first, then one has lazy evaluation. For these and other reduction strategies, theoretical properties are given in [a1], Chapt. 13, and implementation issues are treated in [a4], Chapt. 9.
Types.
While -terms can be used to represent algorithms, types serve to keep an order in these representing terms. (A similar role is played by dimensions of physical entities.) Let
be a set of symbols considered as atomic types (
may e.g. contain nat and bool). Types form the least set
such that if
, then
; if
, then
. A statement is of the form
with
and
. The term
is the subject and
is the predicate of
. A basis is a set of statements with only distinct variables as subjects. If
is a basis, then the notion
(read:
in
is derivable from
; or:
yields
in
) is the least relation satisfying: If
, if
and
, then
; if
; then
. Examples of valid derivable statements are the following:
,
,
, and
. The term
cannot be typed.
The following theorems hold: 1) If , then all reductions starting with
are terminating. 2) It is decidable whether, given a term
, there are
and
such that
; moreover, these
and
can be constructed if they exist. See e.g. [a5] for proofs.
The programming language , see [a8], is based on the type-free lambda calculus in which to some terms types are assigned as above. The second theorem above makes it possible that the programmer does not need to write types: a compiler can construct them.
Semantics.
Since -terms act at the same time as a function and as an argument, one would like to have a set
such that its function space
is in a one-to-one correspondence with
in order to give a semantics to
-terms. This is impossible for cardinality reasons. D.S. Scott constructed models for
-terms by restricting
to the space of continuous functions from
to
(for an appropriate notion of continuity) which has the same cardinality as
. A simple model in this style has been constructed by E. Engeler as follows. Let
be a non-empty set. Let
be the smallest set containing
such that for
and finite
one has
. Take
the collection of all subsets of
. A function
is called continuous if
. For such
define
. In order to reconstruct
, form
, define for
the application
. Then
. Now
-terms can be interpreted in
. Let a mapping
be given (environment). Define for
the element
,
, where
is the environment
such that
and
for
. In order that this definition makes sense it should be verified that
depends continuously on
. This is the case because the application function is continuous in each of its variables.
is a model of the
-calculus in the sense that if
is provable, then
for each
. It can be shown that terms with little computational effect, like
, have as image in
the empty set.
References
[a1] | H.P. Barendregt, "The lambda-calculus, its syntax and semantics" , North-Holland (1984) |
[a2] | H.P. Barendregt, "Lambda calculi with types" , Handbook of Logic in Computer Science , Oxford Univ. Press (To appear (1990)) |
[a3a] | A. Church, "A set of postulates for the foundation of logic" Ann. of Math. (2) , 33 (1932) pp. 346–366 |
[a3b] | A. Church, "A set of postulates for the foundation of logic" Ann. of Math. (2) , 34 (1933) pp. 839–864 |
[a4] | A.J. Field, P.G. Harrison, "Functional programming" , Addison-Wesley (1988) |
[a5] | J.R. Hindley, J.P. Seldin, "Introduction to combinators and lambda calculus" , Cambridge Univ. Press (1986) |
[a6] | S.C. Kleene, "![]() |
[a7] | S.C. Kleene, J.B. Rosser, "The inconsistency of certain formal logics" Ann. of Math. (2) , 36 (1935) pp. 630–636 |
[a8] | R. Milner, "A proposal for standard ![]() |
[a9] | M. Schönfinkel, "Ueber die Bausteine der mathematische Logik" Math. Ann. , 92 (1924) pp. 305–316 |
[a10] | A. Turing, "On computable numbers with an application to the Entscheidungsproblem" Proc. London Math. Soc. , 42 (1936) pp. 230–265 |
[a11] | A. Turing, "Computability and ![]() |
Lambda-calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Lambda-calculus&oldid=35414