Deductive lambda calculus
Deductive lambda calculus considers what happens when lambda terms are regarded as mathematical expressions. One interpretation of the untyped lambda calculus is as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. In this interpretation, if the expression never reduces to normal form then the program never terminates, and the value is undefined. Considered as a mathematical deductive system, each reduction would not alter the value of the expression. The expression would equal the reduction of the expression.
- 1 History
- 2 Introduction
- 3 Terminology
- 4 Interpretation of lambda calculus as mathematics
- 5 Logical inconsistency
- 6 Intensional versus extensional equality
- 7 Set theoretic domain
- 8 See also
- 9 References
Alonzo Church invented the lambda calculus in the 1930s, originally to provide a new and simpler basis for mathematics. However soon after inventing it major logic problems were identified with the definition of the lambda abstraction: The Kleene–Rosser paradox is an implementation of Richard's paradox in the lambda calculus. Haskell Curry found that the key step in this paradox could be used to implement the simpler Curry's paradox. The existence of these paradoxes meant that the lambda calculus could not be both consistent and complete as a deductive system.
Later the lambda calculus was resurrected as a definition of a programming language.
Lambda calculus is the model and inspiration for the development of functional programming languages. These languages implement the lambda abstraction, and use it in conjunction with application of functions, and types.
The use of lambda abstractions, which are then embedded into other mathematical systems, and used as a deductive system, leads to a number of problems, such as Curry's paradox. The problems are related to the definition of the lambda abstraction and the definition and use of functions as the basic type in lambda calculus. This article describes these problems and how they arise.
This is not a criticism of pure lambda calculus, and lambda calculus as a pure system is not the primary topic here. The problems arise with the interaction of lambda calculus with other mathematical systems. Being aware of the problems allows them to be avoided in some cases.
For this discussion, the lambda abstraction is added as an extra operator in mathematics. The usual domains, such as Boolean and real will be available. Mathematical equality will be applied to these domains. The purpose is to see what problems arise from this definition.
Function application will be represented using the lambda calculus syntax. So multiplication will be represented by a dot. Also, for some examples, the let expression will be used.
The following table summarizes;
|Application of the function f to x|
|Multiplication of a by b|
|Let x in y|
|Beta reducible equality|
Interpretation of lambda calculus as mathematics
Eta reduction as mathematics
An eta-reduct is defined by,
In the mathematical interpretation,
Taking f to be a variable then,
or by letting
This definition defines to be the solution for f in the equation,
Beta reduction as mathematics
A beta reduct is,
then is the expression y with the quantified variable x instantiated as z.
As beta reduction is implied from eta reduction, there is no contradiction between the two definitions.
Let z be a Boolean; then we can form an equation with no solutions,
To solve this equation by recursion, we introduce a new function f defined by,
where n is an auxiliary variable to hold the recursion value. (We take it that still returns a Boolean even if it is given a non-Boolean argument.) By an eta-reduction, we obtain,
Then f f is neither true or false, and as f f is a Boolean value (on any x, f returns the Boolean ) then this violates the principle of bivalence.
Intensional versus extensional equality
Another difficulty for the interpretation of lambda calculus as a deductive system is the representation of values as lambda terms, which represent functions. The untyped lambda calculus is implemented by performing reductions on a lambda term, until the term is in normal form. The intensional interpretation  of equality is that the reduction of a lambda term to normal form is the value of the lambda term.
This interpretation considers the identity of a lambda expression to be its structure. Two lambda terms are equal if they are alpha convertible.
The extensional definition of function equality is that two functions are equal if they perform the same mapping;
One way to describe this is that extensional equality describes equality of functions, where as intensional equality describes equality of function implementations.
The extensional definition of equality is not equivalent to the intensional definition. This can be seen in the example below. This inequivalence is created by considering lambda terms as values. In typed lambda calculus this problem is circumvented, because built-in types may be added to carry values that are in a canonical form and have both extensional and intensional equality.
So the distributive law says that the two functions,
are equal, as functions on Church numerals. (Here we encounter a technical weakness of the untyped lambda calculus: there is no way to restrict the domain of a function to the Church numerals. In the following argument we will ignore this difficulty, by pretending that "all" lambda expressions are Church numerals.) The distributive law should apply if the church numerals provided a satisfactory implementation of numbers.
The two terms beta reduce to similar expressions. Still they are not alpha convertible, or even eta convertible (the latter follows because both terms are already in eta-long form). So according to the intensional definition of equality, the expressions are not equal. But if the two functions are applied to the same Church numerals they produce the same result, by the distributive law; thus they are extensionally equal.
This is a significant problem, as it means that the intensional value of a lambda-term may change under extensionally valid transformations. A solution to this problem is to introduce an omega-rule,
- If, for all lambda-expressions t we have , then .
In our situation, "all lambda-expressions" means "all Church numerals", so this is an omega-rule in the standard sense as well. Note that the omega-rule implies the eta-rule, since by a beta-reduction on the right side.
Set theoretic domain
Lambda abstractions are functions of functions. A natural step is to define a domain for the lambda abstraction as a set of all functions.
The set of all functions from a domain D to a range R is given by K in,
Then the definition of the set of all functions of functions is given by F in,
This definition is an unsolved equation for F. Now lambda calculus is defined by beta reductions and eta reductions. Interpreting reduction as defining equality gives an implicit domain for the lambda calculus. The rules are,
- Every lambda abstraction has one value.
- The beta reduction of a lambda term has the same value.
- The eta reduction of a lambda term has the same value.
- Alpha convertible lambda terms are equal.
- [If the omega-rule is present] "omega-equivalent" lambda terms are equal.
- If two lambda terms can not be shown to be equal by the above rules, they are not equal.
If two lambda terms may be reduced to normal form then the Church–Rosser theorem may be used to show that they are equal if their normal forms are alpha convertible.
If one or both of the terms are not normalizing then the undecidability of equivalence shows that in general there is no algorithm to determine if two lambda terms are equal. In general this makes it impossible to know what the distinct elements of the lambda calculus domain are.
Example: No solutions → one solution
And the recursion is,
- ... (beta and then eta reduction)
Which is the first line and will recurse indefinitely. The expression never reduces to normal form. However every lambda term in the reduction represents the same value. This value is distinct from the encodings for true or false. It is not part of the Boolean domain but it exists in the lambda calculus domain.
Example: Multiple solutions → one solution
Using division and signed numbers, the Y combinator may be used to define an expression representing a whole number square root. The Church encoding may also be extended further to rational and real numbers, so that a real square root may be defined. The Church-Turing thesis implies that any computable operator (and its operands) can be represented in lambda calculus.
Using such an encoding,
Using the implementation of divide then,
represents two values in the domain of the signed numbers, if n is not equal to zero. However it is a lambda expression so has only one value in the lambda calculus domain. Beta reduction of this lambda term never reaches normal form. However it represents a value, so a single value in the lambda calculus domain represents two values in the signed number domain.
- A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
- For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
- Kleene, S. C. & Rosser, J. B. (1935). "The inconsistency of certain formal logics". Annals of Mathematics. 36 (3): 630–636. doi:10.2307/1968646.
- The Inconsistency of Certain Formal Logic Haskell B. Curry The Journal of Symbolic Logic Vol. 7, No. 3 (Sep., 1942), pp. 115-117 Published by: Association for Symbolic Logic Article Stable URL: http://www.jstor.org/stable/2269292
- Curry, Haskell B. (1941). "The Paradox of Kleene and Rosser". Transactions of the American Mathematical Society. 50: 454–516. doi:10.1090/S0002-9947-1941-0005275-6. MR 0005275. Retrieved 24 January 2013.
- Selinger, Peter. "Lecture Notes on Lambda Calculus (PDF)" (PDF). p. 6.
- "Lambda calculus - intensionality". Stanford. p. 1.2 Intensionality.