User:Thepigdog/Church-Rosser Theorem

From Knowino

Jump to: navigation, search

This theorem says that reduction may proceed in different orders, and still arrive at the same expression. The theorem allows us to think of Lambda Calculus expressions as representing a value.

The Church-Rosser Theorem states that if you start with an initial expression and perform two different series of reductions on it, to reach two different expressions, there is always a set of reduction for each expression that will reduce it to the same expression. This gives the basis for considering reductions as evaluating expressions. If lambda expressions reduced too different expressions in normal form then it would not be possible to consider the normal form as the value of the function.

However Deductive lambda calculus shows that Lambda Calculus is mathematical under certain conditions, and that under those conditions each expression represents a value. This makes the Church-Rosser Theorem less important, but it does not prove the theorem.

1 Church-Rosser Theorem
2 Etymology of the proof
3 Outline of the proof
4 Defintion of beta redex function
5 Defintion of eta redex function
6 Proof that valid beta reduction functions commute
7 Proof of the substitution case
8 Proof that valid eta reduction functions commute
9 Proof that valid beta reduction functions commute with eta
10 Links
11 References

[edit] Church-Rosser Theorem

If L is a lambda expression, and M and N are both obtained from L by a series of beta or eta reductions then there exists a series of reductions for M and N that will reduce them to the same expression Z.

[edit] Etymology of the proof

The proof given below varies slightly from the proof given in ^[1] due to Tait and Martin-L¨of. That proof combines multiple reduction steps into a single step, and then considers the "Maximal one step reduction" as the point in the diamond. The theorem is then proved by combining the diamonds, to form a larger diamond like structure, the top of which is the original lambda expression, the edge points are the two expressions derived from it, and the bottom point is the Z which brings the values back together again.

This proof creates a definition of a beta reduction step based on the name of the variable in the lambda abstraction. This also allows multiple beta reduction steps to be considered as one step. With this definition, the reduction is commutative, but with some conditions. The conditions do not restrict the construction of the diamond structure as for the above proof.

This proof is given because I found the existing proof long and hard to follow. Also I found it disconcerting that the actual series of reductions to obtain Z was not constructed. Thirdly I like the fact that the reductions are commutative (under conditions), and I thing this gives a clearer intuitive insight into why the Church-Rosser Theorem is true.

[edit] Outline of the proof

Each beta reduction is a function that transforms a lambda expression into another lambda expression. If we have an initial expression L and M and N obtained from L by beta reductions then,

$M = m_1 \circ m_2 ... \circ m_r(L)$

$N = n_1 \circ n_2 ... \circ n_s(L)$

where

m 1, m 2,... m r, n 1, n 2,... n s

are beta reductions.

then,

$O = m_1 \circ m_2 ... \circ m_r(N) = m_1 \circ m_2 ... \circ m_r \circ n_1 \circ n_2 ... \circ n_s(L)$

$P = n_1 \circ n_2 ... \circ n_s(L) = n_1 \circ n_2 ... \circ n_s \circ m_1 \circ m_2 ... \circ m_r(L)$

and the Church-Rosser Theorem is proved if O = P.

If we could prove that the order of the application of beta reductions does not effect the result then we would have proved that O = P. So this would mean that if two reductions as x and y are composed then,

$x \circ y = y \circ x$

This result will be proved but with restrictions on when it is valid. However with the restrictions will not block the proof that O = P.

[edit] Beta and Eta Reduction Functions

The definitions of beta and eta reductions do not give us an explicit representation of a specific beta or eta reduction. The proof will proceed by creating functions that represent reductions. A beta reduction is defined as being applied to any lambda abstraction in the expression. But the function should be a beta reduction applied to a particular lambda abstraction. How is the sub-expression the beta or eta reduction is to be applied to identified?

If canonical renaming is applied then every lambda expression expression has it's own unique variable. Then the name of the variable can be used to identify the lambda expression to which to apply the reduction. Two functions will be defined,

$β f [x]$ performs a beta reduction $β r$ on all lambda abstractions with the name $x$
$η f [x]$ performs an eta reduction $η r$ on all lambda abstractions with the name $x$

But after a beta reduction a lambda abstraction may have been substituted a number of times. The $β f$ and $b e t a f$ functions are defined to reduce all lambda abstractions matching the name. A proof that this definition implies $x \circ y = y \circ x$ is given later, but there are conditions, and the definition needs to be refined further.

[edit] Valid reductions

A lambda abstraction without a parameter is a function. A beta reduction may substitute a lambda expression for a variable, giving it a parameter. This would mean that the $β f$ applied before the beta reduction cannot be applied, because there is no parameter, but after the beta reduction the $β f$ can be applied. This would break $x \circ y = y \circ x$ .

To avoid this situation we define valid application of a beta or eta reduction,

For a $β f [x]$ be validly applied, every lambda expression matching the name x must have a parameter.

[edit] A problem with names

A betaredexf is defined to perform all reductions on lambda abstractions matching the variable name. But this does not define a single beta reduction. For the first beta reduction a canonical renaming can be performed first. But for the second step a beta reduction may have created multiple copies of the lambda abstraction all with the same name.

We want to keep the names so that the betaredexf can be re-ordered, but change them so that they are distinct.

To achieve this add a name qualification scheme. An alpha renaming can change a name by adding a suffix after a period. So x is renamed to x#a.

Betaredexf is redefined to beta reduce all lambda abstractions matching the prefix.

A new kind of canonical renaming is defined that keeps the existing name but adds the unique name as a suffix. Then the betaredexf is the same before and after the canonical renaming.

[edit] Defintion of beta redex function

$\beta _{f} [x][(\lambda w.y)\ z] = \beta _{r} [(\lambda w.\beta _{f} [x][y])\ \beta _{f} [x][z]] \and (x = w \or x\#s = w)$
$\beta _{f} [x][\lambda w.y] = \lambda w.\beta _{f} [x][y] \and \neg (x = w \or x\#s = w)$
$\beta _{f} [x][y \ z] = \beta _{f} [x][y]\ \beta _{f} [x][z]$
$β f [x][v] = v$

Note there is no case for $(x = w \or x\#s = w) \and \beta _{f} [x][\lambda w.y]$ , with no application of the function to a parameter. If this condition occurs it is not a valid reduction.

[edit] Defintion of eta redex function

$\eta _{f} [x][\lambda w.y\ w] = \eta _{f} [x][y] \and (x = w \or x\#s = w)$
$\eta _{f} [x][\lambda w.y\ z] = \lambda w.\eta _{f} [x][y]\ \eta _{f} [x][z] \and (w \ne z \or \neg (x = w \or x\#s = w))$
$\eta _{f} [x][y\ z] = \eta _{f} [x][y]\ \eta _{f} [x][z]$
$η f [x][v] = v$

[edit] Proof that valid beta reduction functions commute

$β f$ applied with $β f$ .

$\neg (x = y\#t \or y = x\#u)$

X = β f [x]

Y = β f [y]

$X \circ Y = Y \circ X$

or

X [Y [l]] = Y [X [l]]

Note that $(x = y\#t \or y = x\#u)$ is a condition where commutativity does not hold.

Proof by induction on all the cases of the lambda expression $l$ . In each inductive case assume that the theorem holds for the parameters.

The proof is summarized in the following table with columns,

Case name - The type of lambda expression, and any logical pre-conditions
- Lambda abstraction
- Application
- Variable
Expression - The expression that needs to be shown true
Simplified Expression - The expression re-arranged to show that it is true if the dependent cases, and inductive preconditios are true.
Dependent case - Conditions that must be proven separately.
Inductive preconditions - Conditions that are assumed true for the purpose of induction.

Case name	Expression	Simplified	Dependent cases	Inductive pre-condition
Abs $\neg (x = v \or x\#s = v)$ $\neg (y = v \or y\#r = v)$	$X [Y [λ v . m]] = Y [X [λ v . m]]$	$λ v . X [Y [m]] = λ v . Y [X [m]]$	none	$X [Y [m]] = Y [X [m]]$
Abs (no parameter) $(x = v \or x\#s = v)$ $\or (y = v \or y\#r = v)$	$X [Y [λ v . m]] = Y [X [λ v . m]]$	either X or Y is not valid $β f$	Invalid.	$X [Y [m]] = Y [X [m]]$
Abs $(x = v \or x\#s = v)$ $\neg (y = v \or y\#r = v)$	$X[ Y[\lambda v.m\ n] ] = Y[ X[\lambda v.m\ n] ]$	$Y [m][v : = Y [n]] = Y [m [v : = n]]$	$Y [m][v : = Y [n]] = Y [m [v : = n]]$ $\neg (y = v \or y\#r = v)$	None
Abs $\neg (x = v \and y = v)$ $(x = v \or x\#s = v)$ $(y = v \or y\#r = v)$	$X[ Y[\lambda v.m\ n] ] = Y[ X[\lambda v.m\ n] ]$	$X [m [v : = n]] = Y [m [v : = n]]$	Not commutative if, $(x = y\#t \or y = x\#u)$	None
Abs $\neg (x = v \and y = v)$	$X[ Y[\lambda v.m\ n] ] = Y[ X[\lambda v.m\ n] ]$	$X[ X[\lambda v.m\ n] ] = X[ X[\lambda v.m\ n] ]$	None	None
Application	$X[ Y[m\ n] ] = Y[ X[m\ n] ]$	$X [ Y[m] ]\ X[ Y[n] ] = Y[ X [m] ]\ Y[ X[n] ]$	none	$X [Y [m]] = Y [X [m]]$ $X [Y [n]] = Y [X [n]]$
Variable	$X [Y [v]] = Y [X [v]]$	$v = v$	none	none

[edit] Proof of the substitution case

Y = β f [y]

$Y[m][v := Y[n]] = Y[ m[v := n] ] \and \neg (y = v \or y = v\#r)$

Case name	Expression	Simplified	Dependent cases	Inductive pre-condition
Abstraction m	$Y[\lambda y.b\ c][v := Y[n]] = Y[ (\lambda y.b\ c)[v := n] ]$	$Y [b][y : = Y [c]][v : = Y [n]] = Y [b [v : = n]][y : = Y [c [v : = n]]]$ $Y [b][y : = Y [c]][v : = Y [n]] = Y [b][v : = Y [n]][y : = Y [c][v : = Y [n]]]$	$[y : = Y [c]][v : = Y [n]] = [v : = Y [n]][y : = Y [c][v : = Y [n]]]$	$Y [c][v : = Y [n]] = Y [c [v : = n]]$ $Y [b][v : = Y [n]] = Y [b [v : = n]]$
Abs not a = b	$Y[\lambda a.b\ c][v := Y[n]] = Y[ (\lambda a.b\ c)[v := n] ]$	$(\lambda a.Y[b][v := Y[n]]\ Y[c][v := Y[n]]) = (\lambda a.Y[b[v := n]]\ Y[c[v := n])] ]$	None	$Y [c][v : = Y [n]] = Y [c [v : = n]]$ $Y [b][v : = Y [n]] = Y [b [v : = n]]$
Application	$Y[p\ q][v := Y[n]] = Y[ (p\ q)[v := n] ]$	$Y[p][v := Y[n]]\ Y[q][v := Y[n]] = Y[p[v := n]]\ Y[q[v := n]]$	None	$Y [p][v : = Y [n]] = Y [p [v : = n]]$ $Y [q][v : = Y [n]] = Y [q [v : = n]]$
Variable	$Y [v][v : = Y [n]] = Y [v [v : = n]]$	$Y [n] = Y [n]$	None	None
Variable not w = v	$Y [w][v : = Y [n]] = Y [w [v : = n]]$	$w = w$	None	None

The dependent case,

[y : = Y [c]][v : = Y [n]] = [v : = Y [n]][y : = Y [c][v : = Y [n]]]

can be written as,

[y : = A][v : = B] = [v : = B][y : = A [v : = B]]

Proof omitted.

[edit] Proof that valid eta reduction functions commute

$η f$ applied with $η f$ .

X = η f [x]

Y = η f [y]

$X \circ Y = Y \circ X$

or

X [Y [l]] = Y [X [l]]

Proof by induction on all the cases of the lambda expression $l$ .

Case name	Expression	Simplified	Dependent cases	Inductive precondition
Abs $v \ne m \or$ $(\neg (x = v \or x\#s = v) \and$ $\neg (y = v \or y\#r = v))$	$X [Y [λ v . m n]] = Y [X [λ v . m n]]$	$\lambda v.(X[Y[m]]\ (X[Y[m]]) = \lambda v.(Y[X[m]]\ (Y[X[m]])$	none	$X [Y [m]] = Y [X [m]]$ $X [Y [n]] = Y [X [n]]$
Abs $(x = v \or x\#s = v) \or$ $(y = v \or y\#r = v)$	$X [Y [λ v . m v]] = Y [X [λ v . m v]]$	$X [Y [m]] = Y [X [m]]$	none	$X [Y [m]] = Y [X [m]]$
Application	$X[ Y[m\ n] ] = Y[ X[m\ n] ]$	$X [ Y[m] ]\ X[ Y[n] ] = Y[ X [m] ]\ Y[ X[n] ]$	none	$X [Y [m]] = Y [X [m]]$ $X [Y [n]] = Y [X [n]]$
Variable	$X [Y [v]] = Y [X [v]]$	$v = v$	none	none

[edit] Proof that valid beta reduction functions commute with eta

$\beta _{f} \!$ applied with $\eta _{f} \!$ .

$X = \beta _{f} [x] \!$

$Y = \eta _{f} [y] \!$

$X \circ Y = Y \circ X \!$

or

$X[ Y[ l ]] = Y[ X[ l ]] \!$

Proof by induction on all the cases of the lambda expression $l$ .

Case name	Expression	Simplified	Dependent cases	Inductive precondition
Abs $\neg (x = v \or x\#s = v) \!$ $\neg (y = v \or y\#r = v) \!$	$X[ Y[\lambda v.m n] ] = Y[ X[\lambda v.m n] ] \!$	$\lambda v.X[Y[m]]\ X[Y[n]] = \lambda v.Y[X[m]]\ Y[X[n]] \!$	none	$X[ Y[m] ] = Y[ X[m] ] \!$ $X[ Y[n] ] = Y[ X[n] ] \!$
Abs $\neg (x = v \or x\#s = v) \!$ $(y = v \or y\#r = v) \!$	$X[ Y[\lambda v.m v] ] = Y[ X[\lambda v.m v] ] \!$	$X[ Y[m] ] = Y[ X[m] ] \!$	none	$X[ Y[m] ] = Y[ X[m] ] \!$
Abs $(x = v \or x\#s = v) \!$ $\neg (y = v \or y\#r = v) \!$	$X[ Y[(\lambda v.m) n] ] = Y[ X[(\lambda v.m) n] ] \!$	$X[Y[m]][v := X[Y[n]]] = Y[X[m][v := X[n]] ] \!$	$X[Y[m]][v := X[Y[n]]] = Y[X[m][v := X[n]] ] \!$	None
Abs $(x = v \or x\#s = v) \!$ $(y = v \or y\#r = v) \!$	$X[ Y[(\lambda v.m\ v) n] ] = Y[ X[(\lambda v.m\ v) n] ] \!$	$X[Y[m]]\ X[Y[n]] = Y[X[m]]\ Y[X[n]] \!$	None	$X[ Y[m] ] = Y[ X[m] ] \!$ $X[ Y[n] ] = Y[ X[n] ] \!$
Abs $v \ne w \!$ $(x = v \or x\#s = v) \!$ $(y = v \or y\#r = v) \!$	$X[ Y[(\lambda v.m\ w) n] ] = Y[ X[(\lambda v.m\ w) n] ] \!$	$X[Y[m]\ Y[w]][v := X[Y[n]]] = Y[ (X[m]\ X[w])[v := X[n]] ] \!$	$X[Y[m]\ Y[w]][v := X[Y[n]]] = Y[ (X[m]\ X[w])[v := X[n]] ]$	None
Application	$X[ Y[m\ n] ] = Y[ X[m\ n] ] \!$	$X [ Y[m] ]\ X[ Y[n] ] = Y[ X [m] ]\ Y[ X[n] ] \!$	none	$X[ Y[m] ] = Y[ X[m] ] \!$ $X[ Y[n] ] = Y[ X[n] ] \!$
Variable	$X[ Y[v] ] = Y[ X[v] ] \!$	$v = v \!$	none	none