User:Thepigdog/Deductive Lambda Calculus

Deductive Lambda Calculus considers what happens when lambda expressions are regarded as mathematical expressions. Lambda calculus is defined as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. Considered as mathematics, 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. 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 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.

Later the Lambda Calculus was resurrected as a definition of a programming language.

Interpretation of Lambda calculus as mathematics

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

Eta reduction as mathematics

An eta-redex is defined by,

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

In the mathematical interpretation,

$\operatorname {eta-redex} [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 redex is,

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

and as,

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

then,

$\lambda x.bz=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}\land x>=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 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. Using the definition of function equality;

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

The left hand side may often be shown to be false where $x=f$

No solutions

Starting with the equation,

$x=\neg x$

defining $x=y\ y$ gives,

$yy=\neg (y\ y)$

or

$x=\operatorname {let} fy=\neg (y\ y)\operatorname {in} f\ f$

The cardinality is,

$|\{f\ f:f\ f=\neg (f\ f)\}|=0$

so it is not valid to get,

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

If we go ahead anyway and translate the let expression into lambda calculus,

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

Then,

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

There is no solution to the equation, and the value does not exist.

Multiple solutions

Also it is possible to construct lambda expressions for which there are multiple values. For example,

$4=x^{2}$

gives,

$x=4/x$

Defining $x=y\ y$

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "http://localhost:6011/enbaike.710302.xyz/v1/":): {\displaystyle y\ y = 4/(y\ y)}

or,

$x=\operatorname {let} f\ y={\frac {4}{y\ y}}\operatorname {in} f\ f$

The cardinality is given by,

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

If we go ahead anyway and translate the let expression into lambda calculus,

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

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}})}}$

so,

$(f\ f)^{2}=4$

Discussion

$f\ x=y\iff \exists f\forall xf\ x=y$

Every variable, except an argument, is implicitly existentially quantified. Parameters are implicitly universally quantified.

Existentially and universally quantified variables skolemizing.

Mathematical statement with Existentially and universally quantified variables as a disjunction of conjunctions.

The effects of copying an expression.

Deconstructing Lambda calculus

The alternate definition,

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

is valid in mathematics. Call mathematics with this definition deductive lambda calculus.

Translation function

Define a translation function between deductive and normal lambda calculus.

Existentially qualified variables

The locality implied by Lambda calculus semantics may be achieved by a one off unique renaming of the variables. This renaming may only be done once in the translation of Lambda calculus into Mathematics.

Implied variables

The meaning of a Lambda calculus program may be taken to be that every anonymous function definition has a unique variable associated with it. So Lambda calculus may be translated into a deductive, mathematical form by adding these implied variables. Beta-reduction on anonymous functions may change the meaning of the program, unless the implied variable is carried.

Changes to a Deductive program induced by reductions

Deduce the changes to the Deductive Lambda Calculus program made by,

• Beta reduction
• Alpha reduction

Two copies of a lambda abstraction, created by beta-reduction must have the same value in each dis-junction.

Beta reduction on an anonymous function changes the meaning

Two copies may have separate values. In Deductive LC one value.

Alpha renaming

Alpha-renaming after beta-reduction may change the meaning of the expression. This is because beta reduction may create multiple copies of an abstraction. The abstractions share the same variable and must have the same value in each dis-junction.

Alpha renaming is wrong.

A function is not a canonical value

Due to the undecidability of equivalence from Church's theorem in general it is not possible to prove that two functions are equal. Functions are not an appropriate choice as values because there is no canonical representation of a function. The intrinsic view of a function as a rule does not allow for the application of mathematical laws to a function to transform it into an equivalent function.

Implicit Variable Semantics

Implicit variable semantics resolves the problems of lambda expressions by creating implicit variables to hold the values. To describe this firstly I will introduce the "let" expression, as a mathematical object. The "let" expression is implemented in many functional languages.

Let Expression

The expression,

${\text{let }}C{\text{ in }}E$

is defined by,

1. $\exists f:G({\text{let }}C{\text{ in }}E)=\exists f:C\land G(E)$ where f is a tuple of the free variables of C
2. ${\text{let }}A\land B{\text{ in }}E)={\text{let }}A{\text{ in }}({\text{let }}B{\text{ in }}E)$

[1] moves the condition C out. In [2] if B is a Boolean the let expression is the conjunction of C and B.

Redefining the lambda expression

A lambda expression with an explicit variable may be defined as,

$k:\lambda x.y=({\text{let }}k\ x=y{\text{ in }}k)$

Cardinality

The meta function "implicit" converts the explicit variable lambda expression into the implicit form, by removing all the implicit variables in the expression.

${\text{implicit}}[k:\lambda x.y]\equiv \lambda x.y$

The two expressions are equivalent if the cardinality of the expression is 1.

$(|\{c:c=e\}|=1)\iff (e={\text{implicit}}[e])$

Example 1. k can not be dropped in,

$(k:\lambda x.x\ x)\ (k:\lambda x.x\ x)$

because,

$|\{c:c=(k:\lambda x.x\ x)\ (k:\lambda x.x\ x)\}|$

$|\{c:c={\text{let }}k\ x=x\ x{\text{ in }}k\ k\}|$

$|\{c:c=k\ k\land k\ x=x\ x\}|$

$\infty$

Example 2.

$k:\lambda x.5\ y$

equals

$\lambda x.5\ y$

because,

$|\{c:c=k:\lambda x.\ y\}|$

$|\{c:c={\text{let }}k\ x=5{\text{ in }}k\ y\}|$

$|\{c:c=5\}|$

$|\{5\}|$

Example 3. k cannot be dropped in,

$k:\lambda x.{\frac {4}{x\ x}}\ k:\lambda x.{\frac {4}{x\ x}}$

because,

$|\{c:c=(k:\lambda x.{\frac {4}{x\ x}}\ k:\lambda x.{\frac {4}{x\ x}})\}|$

$|\{c:c={\text{let }}k\ x={\frac {4}{x\ x}}{\text{ in }}k\ k\}|$

$|\{c:c=k\ k\land k\ x={\frac {4}{x\ x}}\}|$

$|\{c:c=k\ k\land (k\ k)^{2}=4\}|$

$|\{2,-2\}|$

Cardinality and termination

If a lambda expression terminates (the series of reductions reaches a normal form), then this series of reductions shows that the original expression equals the reduction value. Therefore the cardinality of the expression is one and the implicit variable may be dropped.

The inverse is not necessarily true. Proving that an expression has a cardinality of one does not prove that it terminates. In particular the fixed point combinator Y may never terminate, when applied to a function, even where the functions has a single fixed point.

Implicit variable

Most lambda expressions have a cardinality of 1. Lambda expressions with a cardinality other than 1 do not obey mathematical rules. In particular substitution may not be performed.

Non-mathematical lambda expressions may be converted to mathematics by the "explicit" meta function, which realizes the implied variables.

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "http://localhost:6011/enbaike.710302.xyz/v1/":): {\displaystyle \text{explicit}[\lambda x.y] \equiv k:\lambda x.y }

where k is a unique variable implicitly defined with scope defined using implicit scoping rules.

Intrinsic versus extrinsic equality

The untyped lambda calculus is implemented by performing reductions on a lambda term, until the term is in normal form. The intrinsic 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 identify of a lambda expression to be its structure. Two lambda terms are equal if they are alpha convertible.

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

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

The extrinsic definition of equality is incompatible with the intrinsic definition. This can be seen in the example below, where applying a mathematical law changes a function to an equivalent function, yet the intrinsic interpretation of equality says that the two functions are not equal.

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 extrinsic and intrinsic 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.

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 expressions beta reduce to remarkable similar expressions. Still they are not alpha convertible, so according to intrinsic equality, the distributive law does not hold.

Links

• Lambda Calculus