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.

History

Alonzo Church invented the lambda calculus in the 1930s, originally to provide a new and simpler basis for mathematics.^[1][2] However soon after inventing it major logic problems were identified with the definition of the lambda abstraction.^[3]

Haskell Curry studied of illative (deductive) combinatory logic in 1941.^[4] Combinatory logic is closely related to lambda calculus.

The Kleene–Rosser paradox is an implementation of Richard's paradox in combinatory logic. Combinatory logic is closely related to 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 this paradox meant that the combinatory logic, and lambda calculus, could not be both consistent and complete as a deductive system.^[5]

Later the lambda calculus was resurrected as a definition of a programming language.

Introduction

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.

Terminology

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;

Name	Notation
Lambda abstraction.	$\lambda v.y$
Application of the function f to x	$f\ x$
Multiplication of a by b	$a \cdot b$
Let x in y	$\operatorname{let} x \operatorname{in} y$
Mathematical equality	$m = n$
Beta reducible equality	$m =_\beta n$

Interpretation of lambda calculus as mathematics

In the mathematical interpretation, lambda terms represent values. Eta and beta reductions are deductive steps that do not alter the values of expressions.

$\operatorname{eta-reduct}[X] = X$

$\operatorname{beta-reduct}[X] = X$

Eta reduction as mathematics

An eta-reduct is defined by,

$x \not \in \operatorname{FV}(f) \to \operatorname{eta-reduct}[\lambda x.(f\ x)] = f$

In the mathematical interpretation,

$\operatorname{eta-reduct}[X] = X$

Taking f to be a variable then,

$\lambda x.(f\ x) = f$

or by letting $f\ x = y$

$f\ x = y \iff f = \lambda x.y$

This definition defines $\lambda x.y$ to be the solution for f in the equation,

$f\ x = y$

Beta reduction as mathematics

A beta reduct is,

$\operatorname{beta-reduct}[(\lambda x.b)\ z] = b[x:=z]$

and as,

$\operatorname{beta-reduct}[X] = X$

then,

$(\lambda x.b)\ z = b[x:=z]$

This rule is implied by the instantiation of quantified variables. If,

$\forall x: f\ x = y$

then $f\ z$ is the expression y with the quantified variable x instantiated as z.

$f\ z = y[x:=z]$

so,

$(\lambda x.y)\ z = y[x:=z]$

As beta reduction is implied from eta reduction, there is no contradiction between the two definitions.

Logical inconsistency

From eta reduction,

$f\ x = y \iff f = \lambda x.y$

This rule may be interpreted as defining $\lambda x.y$ to be the solution of the equation $f\ x = y$. In defining the solution to the equation in terms of x and y the definition implicitly assumes that there is one and only function f that satisfies the equation. However, for some equations there may be none or multiple solutions. The definition may be compared with defining $\sqrt{}$ by,

$y = x^2 \iff x = \sqrt{y}$

This is not a valid definition as the equation $y = x^2$ has two solutions. The proper definition is,

$(y = x^2 \and x \geq 0) \iff x = \sqrt{y}$

An expression in mathematics may represent multiple values if it has free variables. The variables may be existentially quantified. Existential quantification turns an equation into a disjunction of equations, with each variable populated with a single value in each equation.

The solution set for $f$ in $f\ x = y$ is,

$\{f: f\ x = y \}$

For the definition $(f\ x = y \iff f = \lambda x.y)$ to be valid there must be only one solution in this solution set.

$|\{f : f = y\}| = 1 \equiv (f\ x = y\ x \iff f = \lambda x.y\ x)$

The mathematical (or extensional) definition of function equality is that two functions are equal if they perform the same mapping;

$f = g \iff (\forall x f\ x = g\ x)$

So,

$|\{f : \forall x f\ x = y\ x\}| = 1 \equiv (f\ x = y\ x \iff f = \lambda x.y\ x)$

The left condition is,

$|\{f : \forall x f\ x = y\ x\}| = 1$

The next step is to chop this condition up so that the cardinality is tested for each value of $x$, For any condition $c$, the following result holds,

$|\{f : c\}| = 1 \equiv \exists f \forall x |\{z : z = f\ x \and c\}| = 1$

Apply this formula gives,

$\exists f \forall x |\{z : z = f\ x \and \forall w\ f\ w = y\ w\}| = 1$

The inner condition only constrains $f\ x$ where $x = w$. So,

$(\exists f \forall x |\{z : z = f\ x \and f\ x = y\ x\}| = 1) \equiv (f\ x = y\ x \iff f = \lambda x.y\ x)$

The structure of y

The condition is,

$\exists f \forall x |\{z : z = f\ x \and f\ x = y\ x\}| = 1$

Where $x$ is not a function of $f$, $f = y$ and the cardinality is 1. This leaves only the case where $x$ is a function of $f$

$\exists f \forall x (\exists a\ x = a\ f) \to |\{z : z = f\ x \and f\ x = y\ x\}| = 1$

The $f\ x = y\ x$ may be written,

$f\ (a\ f) = y\ (a\ f)$

If a condition on $f\ (a\ f)$ is to be formed then $y$ must be in the form of a function of $f\ (a\ f)$. Call this function $g$,

$f\ (a\ f) = g\ (f\ (a\ f))$

As $z = f\ (a\ f)$.

$z = g\ z$

Then $y$ and $g$ are related by,

$y\ (a\ f) = g\ (f\ (a\ f))$

The $y$ function must use some mechanism to construct $f\ (a\ f)$ from $a\ f$. For this to be true for any $f$ there must be some way of extracting $f$ from $a\ f$. Call this function $b$, defined by,

$\forall m\ b\ (a\ m) = m$

Then $y$ and $g$ are related by,

$\forall n\ y\ n = g\ ((b\ n)\ n)$

Plugging the results back in and simplifying gives,

$(\exists g\ (\exists a \exists b\ (\forall n\ y\ n = g\ ((b\ n)\ n)) \and (\forall m\ b\ (a\ m) = m)) \to |\{z : z = g\ z\}| = 1)$

$\equiv (f\ x = y\ x \iff f = \lambda x.y\ x)$

No solutions

Starting with $g\ z = \neg z$, where z is a Boolean, an equation with no solutions is formed,

$z = \neg z$

Then letting $a$ and $b$ be the identity function,

$y\ n = \neg (n\ n)$

As,

$|\{z : z = \neg z\}| = 0$

then it is not true that,

$f\ x = \neg (x\ x) \iff f = \lambda x.\neg (x\ x)$

If we go ahead anyway,

$f = \lambda x.\neg (x\ x)$

And then,

$f\ f$

$= (\lambda x.\neg (x\ x)) (\lambda x.\neg (x\ x))$

$= \neg ((\lambda x.\neg (x\ x)) (\lambda x.\neg (x\ x)))$

$= \neg (f\ f)$

Then $f\ f$ is neither true or false, and as $f\ x$ is a Boolean value then this violates the principle of bivalence.

Multiple solutions

Also it is possible to construct lambda expressions for which there are multiple values. In the real number domain, starting with,

$g\ n = \frac{4}{n}$

then,

$z = \frac{4}{z}$

$z^2 = 4$

Then letting $a$ and $b$ be the identity function,

$y\ n = \frac{4}{n\ n}$

As,

$|\{z : z = \frac{4}{z}\}| = 2$

then it is not true that,

$f\ x = \frac{4}{x\ x} \iff f = \lambda x.\frac{4}{x\ x}$

If we go ahead anyway,

$f = \lambda x.\frac{4}{x\ x}$

And then,

$f\ f$

$= (\lambda x.\frac{4}{x\ x}) (\lambda x.\frac{4}{x\ x})$

$= \frac{4}{(\lambda x.\frac{4}{x\ x}) (\lambda x.\frac{4}{x\ x})}$

$= \frac{4}{f\ f}$

and,

$(f\ f)^2 = 4$

Having an equation with multiple solutions is not an inconsistency. However the derivation demonstrated that, for all $(f\ f)$,

$(f\ f)^2 = 4 \implies (f\ f) = (\lambda x.\frac{4}{x\ x})\ (\lambda x.\frac{4}{x\ x})$

Then substituting $(f\ f)$ with 2 gives,

$\operatorname{true} \implies (\lambda x.\frac{4}{x\ x})\ (\lambda x.\frac{4}{x\ x}) = 2$

Substituting $(f\ f)$ with -2 gives,

$\operatorname{true} \implies (\lambda x.\frac{4}{x\ x})\ (\lambda x.\frac{4}{x\ x}) = -2$

Then,

$(\lambda x.\frac{4}{x\ x})\ (\lambda x.\frac{4}{x\ x}) = 2 = -2$

which is a contradiction, because the values 2 and -2 are defined not equal in the real domain.

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^{[6] [7]} 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.

One way to describe this is that extensional equality describes equality of functions, where as intensional equality describes equality of function implementations.

The mathematical (or extensional) definition of function equality is that two functions are equal if they perform the same mapping;

$f = g \iff (\forall x f\ x = g\ x)$

The extensional definition of equality is incompatible with the intensional definition. This can be seen in the example below, where applying a mathematical law changes a function to an equivalent function, yet the intensional interpretation of equality says that the two functions are not equal. This shows the untyped lambda calculus with intensional equality is inconsistent with mathematics as a deductive system.

This incompatibly is created by considering lambda terms as values. In typed lambda calculus this is not a significant problem, because built-in types may be added to carry values that are in a canonical form and have both extensional and intensional equality.

Example

In arithmetic, the distributive law implies that $2 * (r + s) = 2*r + 2*s$. Using the Church encoding of numerals the left and right hand sides may be represented as lambda terms.

So the distributive law says that the two functions,

$\lambda r.\lambda s.2 * (r + s) = \lambda r.\lambda s.2*r + 2*s$

are equal. The distributive law should apply if the church numerals provided a satisfactory implementation of numbers.

Left hand side;

$\lambda r.\lambda s.\operatorname{mult}\ 2\ (\operatorname{plus}\ r\ s)$

$\lambda r.\lambda s.(\lambda m.\lambda n.\lambda f. m\ (n\ f))\ (\lambda f.\lambda x.f\ (f\ x))\ ((\lambda m.\lambda n.\lambda f.\lambda x. m\ f\ (n\ f\ x))\ r\ s)$

$\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (s\ f\ (r\ f\ (s\ f\ x)))$

Right hand side;

$\lambda r.\lambda s.\operatorname{plus}\ (\operatorname{mult}\ 2\ r)\ (\operatorname{mult}\ 2\ s)$

$\lambda r.\lambda s.(\lambda m.\lambda n.\lambda f.\lambda x. m\ f\ (n\ f\ x))\ ((\lambda m.\lambda n.\lambda f. m\ (n\ f))\ (\lambda f.\lambda x.f\ (f\ x))\ r)\ ((\lambda m.\lambda n.\lambda f. m\ (n\ f))\ (\lambda f.\lambda x.f\ (f\ x))\ s)$

$\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (r\ f\ (s\ f\ (s\ f\ x)))$

Comparison;

$\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (s\ f\ (r\ f\ (s\ f\ x)))$

$\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (r\ f\ (s\ f\ (s\ f\ x)))$

The two terms beta reduce to similar expressions. Still they are not alpha convertible, so according to intensional equality, the left hand side and the right hand side are different functions, and are not equal. But according to the distributive law the two functions are the same. If the two functions are applied to the same Church numerals they produce the same result, so in that sense the distributive law holds. But the functions themselves are not equal.

This is a significant problem because all values in the untyped lambda calculus are terms that define functions. So any mathematically correct transformation of a lambda calculus program may change the meaning of the program.

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,

$f \in K \iff (\forall x : x \in D \implies f\ x \in R)$

Then the definition of the set of all functions of functions is given by F in,

$f \in F \iff (\forall x : x \in F \implies f\ x \in F)$

This definition is an unsolved equation for F. If there exists no function that may not be applied to itself, then there is a set F that satisfies the above definition of "all functions". This is the case with lambda calculus, as there are no restriction on the domain of parameters.

However consider the Church numerals. If the functions on Church numerals, such as plus, minus, times and divide were restricted so that they only apply to Church numerals then these are functions that may not be applied to them self. This restriction is desirable because the Church arithmetic functions do not meaningful apply to functions other than Church numerals.

However then we get a version of Russell's paradox. See also Rice's theorem, which relates to partial functions.

To show this assume g is a function that may not be applied to itself,

$g\ g \not \in F$

$x \ne g \implies g\ x \in F$

Firstly assume g is in F. This will be used to deduce a falsehood.

$g \in F \iff (\forall x : x \in F \implies g\ x \in F)$

instantiate x as g.

$\implies (g \in F \implies g\ g\in F)$

$\implies g\ g \in F$

which is false because.

$g\ g \not \in F$

Secondly assume g not in F. Again this will be used to deduce a falsehood. Starting with,

$g \not \in F$

From the definition of all functions of functions, it can be shown that,

$(\forall x : x \in F \implies g\ x \in F) \implies g \in F$

$(\forall x : x \in F \implies g \ne x \implies g\ x \in F) \implies g \in F$

$(\forall x : x \in F \implies \operatorname{true}) \implies g \in F$

$\operatorname{true} \implies g \in F$

$g \in F$

which is false because we assumed,

$g \not \in F$

So g is an element of F and not an element of F.

Therefore, if there exists a function that may not be applied to itself, then there is no set F satisfying the above definition of "all functions". This result limits what can be done with the set theoretic approach to lambda calculus, while not actually ruling out the lambda calculus domain. The lambda calculus domain is OK, defined as a set, but any modification to it may cause problems. The usual approach to defining sets of functions is to build a Von Neumann universe. However, because the only type in the untyped lambda calculus is the function, it is not clear how to do this.

Domain of lambda calculus

The problems with lambda abstraction arose when a domain was imposed on it. If the lambda abstraction is allowed to define the domain, instead of imposing the domain upon the lambda abstraction, these problems no longer appear.

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 two lambda terms can not be shown to be equal, they are not equal.

If lambda terms may be reduced to normal form then the Church–Rosser theorem may be used to show that lambda terms are equal if their normal forms are alpha convertible.

If not 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

For example the equation $x = \neg x$ may be coded with Church encoding and using Curry's Y combinator as,

$\operatorname{not}_1 = \lambda p.\lambda a.\lambda b.p\ b\ a$

$(\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))) (\lambda p.\lambda a.\lambda b.p\ b\ a)$

And the recursion is,

$(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))$

$(\lambda p.\lambda a.\lambda b.p\ b\ a)\ ((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))$

$\lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a$

...

$\lambda a.\lambda b.(\lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a)\ b\ a$

... (beta and then eta reduction)

$(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))$

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,

$x^2 = n \Rightarrow x = \frac{n}{x} \Rightarrow f\ x = \frac{n}{x} \and Y\ f = x$

Using the implementation of divide then,

$Y (\operatorname{divide} n)$

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.

See also

• Lambda calculus
• Let expression
• Church encoding

References

1. A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
2. For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
3. Kleene, S. C. & Rosser, J. B. (1935). "The inconsistency of certain formal logics". Annals of Mathematics 36 (3): 630–636. doi:10.2307/1968646.
4. 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.
5. 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
6. Selinger, Peter. "Lecture Notes on Lambda Calculus (PDF)" (PDF). p. 6.
7. "Lambda calculus - intensionality". Stanford. p. 1.2 Intensionality.