Deductive lambda calculus

An eta-reduct is defined by,

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

In the mathematical interpretation,

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

Taking f to be a variable then,

${\displaystyle \lambda x.(f\ x)=f}$

or by letting ${\displaystyle f\ x=y}$

${\displaystyle f\ x=y\iff f=\lambda x.y}$

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

${\displaystyle f\ x=y}$

A beta reduct is,

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

and as,

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

then,

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

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

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

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

${\displaystyle f\ z=y[x:=z]}$

so,

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

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

In arithmetic, the distributive law implies that ${\displaystyle 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,

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

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.

${\displaystyle {\begin{aligned}\lambda r.\lambda s.\operatorname {mult} \ 2\ (\operatorname {plus} \ r\ s)&=\lambda r.\lambda s.\operatorname {plus} \ (\operatorname {mult} \ 2\ r)\ (\operatorname {mult} \ 2\ s)\\{\scriptstyle \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)}&={\scriptstyle \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\ (s\ f\ (r\ f\ (s\ f\ x)))&=\lambda r.\lambda s.\lambda f.\lambda x.r\ f\ (r\ f\ (s\ f\ (s\ f\ x)))\end{aligned}}}$

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 ${\displaystyle f\ t\ {\underset {\beta }{=}}\ g\ t}$, then ${\displaystyle f\ {\underset {\beta }{=}}\ g}$.

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 ${\displaystyle f\ t\ {\underset {\beta }{=}}\ (\lambda x.f\ x)\ t}$ by a beta-reduction on the right side.

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

${\displaystyle \operatorname {not} _{1}=\lambda p.\lambda a.\lambda b.p\ b\ a}$

${\displaystyle (\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,

${\displaystyle (\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))}$

${\displaystyle (\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)))}$

${\displaystyle \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}$

...

${\displaystyle \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)

${\displaystyle (\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.

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,

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

Using the implementation of divide then,

${\displaystyle 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.