#|
 Copyright (C) 1994 by Natarajan Shankar.  All Rights Reserved.
 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.
 NO WARRANTY
 Natarajan Shankar PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
 PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
 IN NO EVENT WILL Natarajan Shankar BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
 PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
 ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
 LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
 BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
 DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the initial thm theory.

;An Annotated Script of A MECHANICAL PROOF OF THE CHURCH-ROSSER THEOREM.
;                          by
;                    N. Shankar
;
;What follows is a list of events (definitions and lemmas) in the mechanical
;proof of the Church-Rosser theorem that was carried out with the Boyer-Moore
;theorem-prover.  The formal expressions below are subtle and complex and
;the annotations provide only a small amount of help.  The proof consists of
;the following parts -
;1. Formalization of Lambda-calculus in the standard notation.
;2. Formalization of Lambda-calculus in the de Bruijn notation.
;3. Proof of the Diamond property of walks in the de Bruijn notation.
;4. Proof of the Diamond property of sequences of beta-steps.
;5. Proof that a sequence of beta-steps is the transitive closure of
;   a walk.
;6. Proof that the standard notation translates into the de Bruijn notation.
;7. Proof that the Church-Rosser proof for the de Bruijn notation can be

;   translated back into the standard notation.
;8. Proof of the Diamond property of walks directly in the standard notation.
;standard formalization:  The prefix "N" stands for "normal".  The two shells
;NLAMBDA and NCOMB represent lambda-abstraction and application, respectively.
;Variables are represented by numbers and constants by literal atoms.

Event: Add the shell nlambda, with recognizer function symbol nlambdap and 2 accessors: nbind, with type restriction (one-of numberp) and default value zero; nbody, with type restriction (none-of) and default value zero.

Event: Add the shell ncomb, with recognizer function symbol ncombp and 2 accessors: nleft, with type restriction (none-of) and default value zero; nright, with type restriction (none-of) and default value zero.

;(NSUBST X Y N) is the result of substituting term Y for variable N in term X.

Definition: nsubst (x, y, n) = if nlambdap (x)

then if nbind (x) = n then x

else nlambda (nbind (x), nsubst (nbody (x), y, n)) endif elseif ncombp (x) then ncomb (nsubst (nleft (x), y, n), nsubst (nright (x), y, n)) elseif x ∈ N then if x = n then y else x endif

else x endif

;Variable X does not occur free in term Y.

Definition: not-free-in (x, y) = if nlambdap (y)

then if x = nbind (y) then t

else not-free-in (x, nbody (y)) endif elseif ncombp (y) then not-free-in (x, nleft (y)) ∧ not-free-in (x, nright (y)) else x ≠ y endif

;The free variables in Y are disjoint from the bound variables in X.

Definition: free-for (x, y) = if nlambdap (x) then not-free-in (nbind (x), y)

∧ free-for (nbody (x), y)

elseif ncombp (x) then free-for (nleft (x), y)

∧ free-for (nright (x), y)

else t endif

;Index of the first occurrence of N in the list LIST.

Definition: index (n, list) = if listp (list)

then if car (list) = n then 1

else 1 + index (n, cdr (list)) endif else 1 + n endif

;A and B are identical modulo bound-variables which are accumulated in
;X and Y, respectively.

Definition: alpha-equal (a, b, x, y) = if nlambdap (a) ∧ nlambdap (b)

then alpha-equal (nbody (a), nbody (b), cons (nbind (a), x), cons (nbind (b), y)) elseif ncombp (a) ∧ ncombp (b) then alpha-equal (nleft (a), nleft (b), x, y)

∧ alpha-equal (nright (a), nright (b), x, y) elseif (a ∈ N) ∧ (b ∈ N) then index (a, x) = index (b, y) else a = b endif

;X is a well-formed term in the standard notation.

Definition: ntermp (x) = if nlambdap (x) then ntermp (nbody (x))

elseif ncombp (x) then ntermp (nleft (x)) ∧ ntermp (nright (x))

else (x ∈ N) ∨ litatom (x) endif

;A goes to B by the beta-reduction of some non-overlapping redexes.

Definition: nbeta-step (a, b) = if a = b then t

elseif nlambdap (a) then nlambdap (b)

∧ (nbind (a) = nbind (b))

∧ nbeta-step (nbody (a), nbody (b)) elseif ncombp (a) then (nlambdap (nleft (a))

∧ free-for (nbody (nleft (a)), nright (a))

∧ (b = nsubst (nbody (nleft (a)), nright (a), nbind (nleft (a))))) ∨ (ncombp (b)

∧ nbeta-step (nleft (a), nleft (b)) ∧ nbeta-step (nright (a), nright (b)))

else f endif

;A goes to B by an alpha-or-beta-step.

Definition: nstep (a, b) = (alpha-equal (a, b, nil, nil) ∨ nbeta-step (a, b))

;A goes to B via a series of steps through terms in LIST.

Definition: nreduction (a, b, list) = if listp (list)

then nstep (car (list), b) ∧ nreduction (a, car (list), cdr (list))

else nstep (a, b) endif

;de Bruijn formalization:

Event: Add the shell lambda, with recognizer function symbol lambdap and 1 accessor: body, with type restriction (none-of) and default value zero.

Event: Add the shell comb, with recognizer function symbol combp and 2 accessors: left, with type restriction (none-of) and default value zero; right, with type restriction (none-of) and default value zero.

;BUMP increments all variables of stack-level greater than N by one.

Definition: bump (x, n) = if lambdap (x) then lambda (bump (body (x), 1 + n))

elseif combp (x) then comb (bump (left (x), n), bump (right (x), n))

elseif n < x then 1 + x

else x endif

;(SUBST X Y N) is the result of substituting Y for N in X.

Definition: subst (x, y, n) = if lambdap (x) then lambda (subst (body (x), bump (y, 0), 1 + n))

elseif combp (x) then comb (subst (left (x), y, n), subst (right (x), y, n)) elseif x ≄ 0 then if x = n then y

elseif n < x then x − 1

else x endif else x endif

;BUMP commutes with itself.

Theorem: bump-bump (n ≤ m) → (bump (bump (y, n), 1 + m) = bump (bump (y, m), n))

Definition: bump-subst-induct (x, y, n, m) = if lambdap (x) then bump-subst-induct (body (x), bump (y, 0), 1 + n, 1 + m)

elseif combp (x)

then bump-subst-induct (left (x), y, n, m)

∧ bump-subst-induct (right (x), y, n, m) else t endif

;BUMP distributes over SUBST.

Theorem: bump-subst (m < n) → (bump (subst (x, y, n), m) = subst (bump (x, m), bump (y, m), 1 + n))

Definition: subst-induct (x, y, z, m, n) = if lambdap (x)

then subst-induct (body (x), bump (y, 0), bump (z, 0), 1 + m, 1 + n)

elseif combp (x)

then subst-induct (left (x), y, z, m, n)

∧ subst-induct (right (x), y, z, m, n) else t endif

Theorem: lambdap-bump lambdap (x) → lambdap (bump (x, n))

Theorem: lambdap-subst lambdap (x) → lambdap (subst (x, y, n))

;BUMP distributes over SUBST in another way.

Theorem: another-bump-subst (n ≤ (1 + m)) → (subst (bump (x, 1 + m), bump (y, m), n) = bump (subst (x, y, n), m))

Theorem: bump-lambdap lambdap (x) → (body (bump (x, n)) = bump (body (x), 1 + n))

Theorem: subst-lambda lambdap (x) → (body (subst (x, y, n)) = subst (body (x), bump (y, 0), 1 + n))

Definition: left-instrs (x) = car (x)

Definition: right-instrs (x) = cadr (x)

Definition: command (x) = caddr (x)

;Result of applying walk-instruction W to M in an inside-out manner.

Definition: walk (w, m) = if lambdap (m) then lambda (walk (w, body (m)))

elseif combp (m)

then if (command (w) = 'reduce) ∧ lambdap (left (m)) then subst (body (walk (left-instrs (w), left (m))),

walk (right-instrs (w), right (m)),

                   1)

else comb (walk (left-instrs (w), left (m)),

walk (right-instrs (w), right (m))) endif

else m endif

Definition: bump-walk-ind (u, m, n) = if lambdap (m) then bump-walk-ind (u, body (m), 1 + n)

elseif combp (m)

then if (command (u) = 'reduce) ∧ lambdap (left (m)) then bump-walk-ind (left-instrs (u), left (m), n)

∧ bump-walk-ind (right-instrs (u), right (m), n) else bump-walk-ind (left-instrs (u), left (m), n)

∧ bump-walk-ind (right-instrs (u), right (m), n) endif

else t endif

Theorem: lambda-walk lambdap (m) → lambdap (walk (w, m))

;BUMP and WALK commute with each other.

Theorem: bump-walk walk (u, bump (m, n)) = bump (walk (u, m), n)

Theorem: nlistp-walk (w ≃ nil) → (walk (w, m) = m)

;The `skolem' function generating the substitutive walk.

Definition: sub-walk (w, m, u, n) = if lambdap (m) then sub-walk (w, body (m), u, 1 + n)

elseif combp (m)

then if (command (w) = 'reduce) ∧ lambdap (left (m)) then list (sub-walk (left-instrs (w), left (m), u, n),

sub-walk (right-instrs (w), right (m), u, n),

                 'reduce)

else list (sub-walk (left-instrs (w), left (m), u, n),

sub-walk (right-instrs (w), right (m), u, n)) endif

elseif m ≄ 0

then if m = n then u else w endif

else w endif

Definition: walk-subst-ind (w, m, u, x, n) = if lambdap (m) then walk-subst-ind (w, body (m), u, bump (x, 0), 1 + n)

elseif combp (m)

then if (command (w) = 'reduce) ∧ lambdap (left (m))

then walk-subst-ind (left-instrs (w), left (m), u, x, n)

∧ walk-subst-ind (right-instrs (w), right (m), u, x, n) else walk-subst-ind (left-instrs (w), left (m), u, x, n)

∧ walk-subst-ind (right-instrs (w), right (m), u, x, n) endif

else t endif

;(BUMP X N) cannot contain N+1 free.

Theorem: subst-not-free-in subst (bump (x, n), y, 1 + n) = x

;SUBST distributes over itself.  A tricky one!

Theorem: subst-subst ((m ∈ N) ∧ (m < n)) → (subst (subst (x, bump (z, m), 1 + n), subst (y, z, n), 1 + m)

= subst (subst (x, y, 1 + m), z, n))

;The substitutivity of walks lemma.

Theorem: walk-subst (n ≄ 0) → (walk (sub-walk (w, m, u, n), subst (m, x, n))

= subst (walk (w, m), walk (u, x), n))

Theorem: walk-lambda lambdap (x) → (body (walk (u, x)) = walk (u, body (x)))

;`Skolem' function generating convergent walk.

Definition: make-walk (m, u, v) = if lambdap (m) then make-walk (body (m), u, v)

elseif combp (m)

then if (command (u) = 'reduce) ∧ lambdap (left (m))

then sub-walk (make-walk (left (m), left-instrs (u), left-instrs (v)), body (walk (left-instrs (u), left (m))), make-walk (right (m), right-instrs (u), right-instrs (v)),

                      1)

elseif (command (v) = 'reduce) ∧ lambdap (left (m)) then list (make-walk (left (m), left-instrs (u), left-instrs (v)),

make-walk (right (m), right-instrs (u), right-instrs (v)),

                 'reduce)

else list (make-walk (left (m), left-instrs (u), left-instrs (v)),

make-walk (right (m), right-instrs (u), right-instrs (v))) endif

else u endif

;The Diamond property of walks.

Theorem: main walk (make-walk (m, u, v), walk (u, m)) = walk (make-walk (m, v, u), walk (v, m))

;Result of applying a series of walks.

Definition: reduce (w, m) = if listp (w) then reduce (cdr (w), walk (car (w), m))

else m endif

;`Skolem' function constructing convergent walk given a walk W and a
;series of walks V.

Definition: make-walk-reduce (m, w, v) = if listp (v)

then make-walk-reduce (walk (car (v), m), make-walk (m, car (v), w), cdr (v))

else w endif

;`Skolem' function constructing convergent series of walks for same case as above.

Definition: make-reduce-walk (m, w, v) = if listp (v)

then cons (make-walk (m, w, car (v)),

make-reduce-walk (walk (car (v), m), make-walk (m, car (v), w), cdr (v)))

else nil endif

;The Rectangle property.

Theorem: walk-reduce reduce (make-reduce-walk (m, w, v), walk (w, m)) = walk (make-walk-reduce (m, w, v), reduce (v, m))

;`Skolem' function constructing convergent series of walks for Diamond property.

Definition: make-reduce (m, u, v) = if listp (u)

then cons (make-walk-reduce (m, car (u), v),

make-reduce (walk (car (u), m), cdr (u), make-reduce-walk (m, car (u), v)))

else u endif

Theorem: list-make-reduce listp (v) → (reduce (make-reduce (m, u, v), reduce (v, m))

= reduce (make-reduce (walk (car (v), m), make-reduce-walk (m, car (v), u), cdr (v)),

reduce (v, m)))

Theorem: list-make-reduce1 reduce (make-reduce (m, u, cons (x, y)), reduce (y, walk (x, m))) = reduce (make-reduce (walk (x, m), make-reduce-walk (m, x, u), y),

reduce (cons (x, y), m))

;The Diamond property of a series of walks.

Theorem: church-rosser reduce (make-reduce (m, u, v), reduce (v, m)) = reduce (make-reduce (m, v, u), reduce (u, m))

;Translation from standard to de Bruijn.  X a standard term, and
;BOUNDS bound variables accumulated so far.

Definition: translate (x, bounds) = if nlambdap (x) then lambda (translate (nbody (x), cons (nbind (x), bounds)))

elseif ncombp (x) then comb (translate (nleft (x), bounds), translate (nright (x), bounds)) elseif x ∈ N then index (x, bounds) else x endif

;Two alpha-equivalent terms have the same translation.

Theorem: alpha-translate alpha-equal (a, b, x, y) → (translate (a, x) = translate (b, y))

Definition: insert (x, bounds, n) = if n ≃ 0 then cons (x, bounds)

elseif listp (bounds) then cons (car (bounds), insert (x, cdr (bounds), n − 1)) else cons (x, nil) endif

Definition: nsubst-ind (x, y, z, bounds, n) = if nlambdap (x)

then if nbind (x) = z then t

else nsubst-ind (nbody (x), y, z, cons (nbind (x), bounds), 1 + n) endif elseif ncombp (x) then nsubst-ind (nleft (x), y, z, bounds, n)

∧ nsubst-ind (nright (x), y, z, bounds, n) else t endif

Definition: trans-insert-ind (x, z, bounds, n) = if nlambdap (x)

then trans-insert-ind (nbody (x), z, cons (nbind (x), bounds), 1 + n) elseif ncombp (x) then trans-insert-ind (nleft (x), z, bounds, n)

∧ trans-insert-ind (nright (x), z, bounds, n) else t endif

Definition: precede (x, bounds, n) = if n ≃ 0 then f

elseif listp (bounds) then (car (bounds) = x) ∨ precede (x, cdr (bounds), n − 1) else f endif Theorem: nprecede-index ((¬ precede (z, bounds, n)) ∧ (n ≤ length (bounds))) → (index (z, insert (z, bounds, n)) = (1 + n))

Theorem: precede-index1 ((n < index (x, bounds)) ∧ (n ≤ length (bounds))) → (index (x, insert (z, bounds, n))

= if x = z then 1 + n else 1 + index (x, bounds) endif)

Theorem: precede-index precede (z, bounds, n) → (index (z, insert (z, bounds, n)) < (1 + n))

Theorem: precede-index2 ((index (x, bounds) ≤ n) ∧ (n ≤ length (bounds))) → (index (x, insert (z, bounds, n)) = index (x, bounds))

Theorem: translate-insert (precede (z, bounds, n) ∧ (n ≤ length (bounds)) ∧ ntermp (x)) → (translate (x, insert (z, bounds, n)) = bump (translate (x, bounds), n))

Theorem: subst-nsubst (precede (z, bounds, n) ∧ ntermp (x) ∧ (n ≤ length (bounds))) → (subst (translate (x, insert (z, bounds, n)), y, 1 + n)

= translate (x, bounds))

Definition: not-free-ind (y, z, bounds, n) = if nlambdap (y)

then not-free-ind (nbody (y), z, cons (nbind (y), bounds), 1 + n)

elseif ncombp (y)

then not-free-ind (nleft (y), z, bounds, n)

∧ not-free-ind (nright (y), z, bounds, n) else t endif

Theorem: translate-insert1 (precede (z, cons (x, bounds), 1 + n) ∧ ntermp (y) ∧ (n ≤ length (bounds))) → (translate (y, cons (x, insert (z, bounds, n)))

= bump (translate (y, cons (x, bounds)), 1 + n))

Theorem: not-free-in-translate (not-free-in (z, y) ∧ (n ≤ length (bounds)) ∧ ntermp (y)) → (translate (y, insert (z, bounds, n)) = bump (translate (y, bounds), n))

Theorem: not-free-in-corr (ntermp (y) ∧ not-free-in (z, y)) → (translate (y, cons (z, bounds)) = bump (translate (y, bounds), 0))

Theorem: subst-nsubst2 (precede (z, cons (w, bounds), 1 + n) ∧ ntermp (x) ∧ (n ≤ length (bounds))) → (subst (translate (x, cons (w, insert (z, bounds, n))), y, 1 + (1 + n))

= translate (x, cons (w, bounds)))

Theorem: subst-nsubst2-corr ntermp (x) → (subst (translate (x, cons (z, cons (z, bounds))), y, 1 + (1 + 0))

= translate (x, cons (z, bounds)))

Theorem: index-insert ((x ≠ z) ∧ (n ≤ length (bounds))) → (index (x, insert (z, bounds, n)) ≠ (1 + n))

;Translation distributes over substitution.

Theorem: translate-preserves-subst (free-for (x, y) ∧ (¬ precede (z, bounds, n)) ∧ (n ≤ length (bounds)) ∧ ntermp (x) ∧ ntermp (y)) → (translate (nsubst (x, y, z), bounds)

= subst (translate (x, insert (z, bounds, n)), translate (y, bounds), 1 + n))

;Translation distributes over beta-reduction.

Theorem: translate-preserves-reduction (nlambdap (x) ∧ free-for (nbody (x), y) ∧ ntermp (x) ∧ ntermp (y)) → (translate (nsubst (nbody (x), y, nbind (x)), bounds)

= subst (body (translate (x, bounds)), translate (y, bounds), 1))

;Reduction is the transitive closure of a walk.
;X goes to Y in a beta-step, in the de Bruijn notation.

Definition: beta-step (x, y) = if x = y then t

elseif lambdap (x) then lambdap (y) ∧ beta-step (body (x), body (y)) elseif combp (x) then (lambdap (left (x)) ∧ (y = subst (body (left (x)), right (x), 1)))

∨ (combp (y) ∧ beta-step (left (x), left (y)) ∧ beta-step (right (x), right (y)))

else f endif

;A goes to B via LIST in a series of beta-steps.

Definition: reduction (a, b, list) = if listp (list)

then beta-step (car (list), b) ∧ reduction (a, car (list), cdr (list))

else beta-step (a, b) endif

Definition: make-walk-step (x, y) = if x = y then nil

elseif lambdap (x) then make-walk-step (body (x), body (y))

elseif combp (x)

then if lambdap (left (x))

∧ (y = subst (body (left (x)), right (x), 1))

         then '(nil nil reduce)

else list (make-walk-step (left (x), left (y)),

make-walk-step (right (x), right (y))) endif

else nil endif

Theorem: make-walk-step-walks beta-step (a, b) → (walk (make-walk-step (a, b), a) = b)

Definition: append (x, y) = if listp (x) then cons (car (x), append (cdr (x), y))

else y endif

Definition: make-reduce-reduction (a, b, list) = if listp (list)

then append (make-reduce-reduction (a, car (list), cdr (list)),

list (make-walk-step (car (list), b), nil))

else list (make-walk-step (a, b)) endif

Theorem: reduce-append reduce (append (x, y), a) = reduce (y, reduce (x, a))

;A reduction is a series of walks.

Theorem: make-reduce-reduction-reduction reduction (a, b, list) → (reduce (make-reduce-reduction (a, b, list), a) = b)

Definition: list-lambda (list) = if listp (list) then cons (lambda (car (list)), list-lambda (cdr (list)))

else nil endif Theorem: lambda-reduction reduction (a, a1 , list) → reduction (lambda (a), lambda (a1 ), list-lambda (list))

Definition: map-comb-left (a, list) = if listp (list)

then cons (comb (a, car (list)), map-comb-left (a, cdr (list)))

else nil endif

Definition: map-comb-right (a, list) = if listp (list)

then cons (comb (car (list), a), map-comb-right (a, cdr (list)))

else nil endif

Definition: list-comb (a, b, list1 , list2 ) = if listp (list1 )

then if listp (list2 )

then cons (comb (car (list1 ), car (list2 )),

list-comb (a, b, cdr (list1 ), cdr (list2 )))

else map-comb-right (b, list1 ) endif elseif listp (list2 ) then map-comb-left (a, list2 ) else nil endif

Theorem: map-comb-right-reduction2 reduction (a, a1 , list1 ) → reduction (comb (a, b1 ), comb (a1 , b1 ), map-comb-right (b1 , list1 ))

Theorem: map-comb-right-reduction (beta-step (b, b1 ) ∧ reduction (a, a1 , list1 )) → reduction (comb (a, b), comb (a1 , b1 ), map-comb-right (b, list1 ))

Theorem: map-comb-left-reduction2 reduction (b, b1 , list2 ) → reduction (comb (a1 , b), comb (a1 , b1 ), map-comb-left (a1 , list2 ))

Theorem: map-comb-left-reduction (reduction (b, b1 , list2 ) ∧ beta-step (a, a1 )) → reduction (comb (a, b), comb (a1 , b1 ), map-comb-left (a, list2 ))

Theorem: list-comb-reduction (reduction (a, a1 , list1 ) ∧ reduction (b, b1 , list2 )) → reduction (comb (a, b), comb (a1 , b1 ), list-comb (a, b, list1 , list2 ))

Theorem: beta-subst beta-step (comb (lambda (a), b), subst (a, b, 1))

Definition: make-reduction-walk (w, a) = if walk (w, a) = a then nil

elseif lambdap (a) then list-lambda (make-reduction-walk (w, body (a)))

elseif combp (a)

then if lambdap (left (a)) ∧ (command (w) = 'reduce)

then cons (subst (body (walk (left-instrs (w), left (a))), walk (right-instrs (w), right (a)), 1),

cons (comb (walk (left-instrs (w), left (a)),

walk (right-instrs (w), right (a))), list-comb (left (a),

right (a),

make-reduction-walk (left-instrs (w),

left (a)),

make-reduction-walk (right-instrs (w),

right (a)))))

else list-comb (left (a), right (a), make-reduction-walk (left-instrs (w), left (a)), make-reduction-walk (right-instrs (w),

right (a))) endif

else nil endif

;A walk is a series of beta-steps.

Theorem: make-reduction-walk-steps reduction (a, walk (w, a), make-reduction-walk (w, a))

Theorem: reduction-append (reduction (a, b, x) ∧ reduction (b, c, y)) → reduction (a, c, append (y, cons (b, x)))

Definition: make-reduce-steps (w, a) = if listp (w)

then append (make-reduce-steps (cdr (w), walk (car (w), a)),

cons (walk (car (w), a), make-reduction-walk (car (w), a)))

else nil endif

Theorem: make-reduce-steps-steps reduction (a, reduce (w, a), make-reduce-steps (w, a))

;`Skolem' function MAKE-W constructs the W to which Y and Z converge.

Definition: make-w (x, y, z, list1 , list2 ) = reduce (make-reduce (x,

make-reduce-reduction (x, y, list1 ), make-reduce-reduction (x, z, list2 )),

reduce (make-reduce-reduction (x, z, list2 ), x))

;MAKE-REDUCTION constructs the corresponding series of beta-steps.

Definition: make-reduction (x, y, z, list1 , list2 ) = make-reduce-steps (make-reduce (x,

make-reduce-reduction (x, z, list2 ), make-reduce-reduction (x, y, list1 )),

y)

;The next two events together give the Church-Rosser theorem for the de Bruijn
;representation.  The first one shows the existence of convergent reductions,
;and the second one shows that they converge.

Theorem: the-real-church-rosser (reduction (x, y, list1 ) ∧ reduction (x, z, list2 )) → (reduction (y,

make-w (x, z, y, list2 , list1 ),

make-reduction (x, y, z, list1 , list2 ))

∧ reduction (z, make-w (x, y, z, list1 , list2 ), make-reduction (x, z, y, list2 , list1 )))

Theorem: both-make-w-are-same (reduction (x, y, list1 ) ∧ reduction (x, z, list2 )) → (make-w (x, y, z, list1 , list2 ) = make-w (x, z, y, list2 , list1 ))

;Translating the proof back into the standard notation.
;A standard beta-step translates to a de Bruijn beta-step.

Theorem: nbeta-step-translates (ntermp (a) ∧ nbeta-step (a, b)) → beta-step (translate (a, x), translate (b, x))

Definition: trans-list (x) = if listp (x) then cons (translate (car (x), nil), trans-list (cdr (x)))

else nil endif

Theorem: ntermp-subst (ntermp (x) ∧ ntermp (y)) → ntermp (nsubst (x, y, n))

Theorem: ntermp-bstep (nbeta-step (a, b) ∧ ntermp (a)) → ntermp (b)

Theorem: ntermp-astep (alpha-equal (a, b, x, y) ∧ ntermp (a)) → ntermp (b)

Theorem: ntermp-list (nreduction (a, b, list) ∧ ntermp (a)) → ntermp (b)

;Standard reduction goes to de Bruijn reduction.

Theorem: reduction-translates (ntermp (a) ∧ nreduction (a, b, list)) → reduction (translate (a, nil), translate (b, nil), trans-list (list))

;Finds the largest free-variable in the de Bruijn term X.

Definition: find-m (x, n) = if lambdap (x) then find-m (body (x), 1 + n)

elseif combp (x)

then if find-m (left (x), n) < find-m (right (x), n)

then find-m (right (x), n) else find-m (left (x), n) endif

else x − n endif

;Translates the de Bruijn term X into a standard term given stack level N,
;and that M is the largest free variable in X.  Very tricky!

Definition: untrans (x, m, n) = if lambdap (x) then nlambda (m + (1 + n), untrans (body (x), m, 1 + n))

elseif combp (x)

then ncomb (untrans (left (x), m, n), untrans (right (x), m, n))

elseif n < x then x − (1 + n)

elseif x ≄ 0 then 1 + (m + (n − x))

else x endif

;X is a well-formed de Bruijn term.

Definition: termp (x) = if lambdap (x) then termp (body (x))

elseif combp (x) then termp (left (x)) ∧ termp (right (x))

else (x ≄ 0) ∨ litatom (x) endif Theorem: not-free-in-untrans (termp (x) ∧ (find-m (x, n) ≤ m) ∧ ((m + n) < y)) → not-free-in (y, untrans (x, m, n))

;An untranslated term is free for another untranslated term.

Theorem: free-for-untrans (termp (x) ∧ termp (y) ∧ (n2 ≤ n1 ) ∧ (find-m (y, n2 ) ≤ m)) → free-for (untrans (x, m, n1 ), untrans (y, m, n2 ))

Definition: trans-untrans-ind (x, bounds, m, n) = if nlambdap (x)

then trans-untrans-ind (nbody (x), cons (nbind (x), bounds), m, 1 + n)

elseif ncombp (x)

then trans-untrans-ind (nleft (x), bounds, m, n)

∧ trans-untrans-ind (nright (x), bounds, m, n) else t endif

;Generates a list of bound variables of length N.

Definition: bindings (m, n) = if n ≃ 0 then nil

else cons (m + n, bindings (m, n − 1)) endif

;A TRANSLATE followed by an UNTRANS leaves X unchanged (modulo bound variables).

Theorem: trans-untrans ((length (bounds) = n) ∧ ntermp (x) ∧ (find-m (translate (x, bounds), n) ≤ m)) → alpha-equal (x, untrans (translate (x, bounds), m, n), bounds, bindings (m, n))

Theorem: termp-ntermp ntermp (x) → termp (translate (x, bounds))

Theorem: ntermp-termp termp (x) → ntermp (untrans (x, m, n))

Theorem: index-freevar ((n < x) ∧ ((x − n) ≤ m)) → (index ((x − 1) − n, bindings (m, n)) = x)

;An UNTRANS followed by a TRANSLATE doesn't change a thing.

Theorem: untrans-trans (termp (x) ∧ (find-m (x, n) ≤ m)) → (translate (untrans (x, m, n), bindings (m, n)) = x)

Theorem: untrans-subst (termp (x) ∧ termp (y) ∧ lambdap (x) ∧ (find-m (y, n) ≤ m) ∧ (find-m (x, n) ≤ m)) → (translate (nsubst (nbody (untrans (x, m, n)),

untrans (y, m, n),

nbind (untrans (x, m, n))), bindings (m, n))

= subst (body (x), y, 1))

Theorem: litatom-translate litatom (translate (a, bounds)) → (translate (a, bounds) = a)

;If A and B have the same translation, then they are alpha-equal.

Theorem: translate-alpha (ntermp (a) ∧ ntermp (b) ∧ (translate (a, bounds) = translate (b, bounds2 ))) → alpha-equal (a, b, bounds, bounds2 )

Theorem: termp-bump termp (x) → termp (bump (x, n))

Theorem: termp-subst (termp (x) ∧ termp (y) ∧ (n ≄ 0)) → termp (subst (x, y, n))

;Returns an instruction corresponding to a beta-step.

Definition: make-bstep (a, b) = if a = b then nil

elseif lambdap (a) ∧ lambdap (b) then make-bstep (body (a), body (b)) elseif combp (a) then if lambdap (left (a))

∧ (b = subst (body (left (a)), right (a), 1)) then list (nil, nil, 'reduce) else list (make-bstep (left (a), left (b)),

make-bstep (right (a), right (b))) endif

else nil endif

;Applies the instruction to a term.

Definition: bstep (w, x) = if lambdap (x) then lambda (bstep (w, body (x)))

elseif combp (x)

then if lambdap (left (x)) ∧ (command (w) = 'reduce) then subst (body (left (x)), right (x), 1) else comb (bstep (left-instrs (w), left (x)),

bstep (right-instrs (w), right (x))) endif

else x endif

;The instruction works.

Theorem: make-bstep-beta-step beta-step (a, b) → (bstep (make-bstep (a, b), a) = b)

;A standard beta-step.

Definition: nbstep (w, x) = if nlambdap (x) then nlambda (nbind (x), nbstep (w, nbody (x)))

elseif ncombp (x)

then if nlambdap (nleft (x)) ∧ (command (w) = 'reduce) then nsubst (nbody (nleft (x)), nright (x), nbind (nleft (x))) else ncomb (nbstep (left-instrs (w), nleft (x)),

nbstep (right-instrs (w), nright (x))) endif

else x endif

Theorem: lambdap-untrans termp (x) → (nlambdap (untrans (x, m, n)) = lambdap (x))

Definition: find-m-subst-ind (x, y, m, n, ind) = if lambdap (x)

then find-m-subst-ind (body (x), bump (y, 0), m, 1 + n, 1 + ind) elseif combp (x) then find-m-subst-ind (left (x), y, m, n, ind)

∧ find-m-subst-ind (right (x), y, m, n, ind) else t endif

Theorem: find-m-bump find-m (y, n) ≮ find-m (bump (y, count), 1 + n)

Theorem: diff-zero (m ≤ n) → ((m − n) = 0)

Definition: untrans-bstep-ind (a, b, m, n) = if a = b then t

elseif lambdap (a) ∧ lambdap (b)

then untrans-bstep-ind (body (a), body (b), m, 1 + n)

elseif combp (a)

then if lambdap (left (a))

∧ (b = subst (body (left (a)), right (a), 1)) then t else untrans-bstep-ind (left (a), left (b), m, n)

∧ untrans-bstep-ind (right (a), right (b), m, n) endif

else t endif

Theorem: nbstep-nil (w ≃ nil) → (nbstep (w, a) = a)

;A beta-step translates back.

Theorem: untrans-beta-step (beta-step (a, b) ∧ termp (a) ∧ (find-m (a, n) ≤ m)) → nbeta-step (untrans (a, m, n), nbstep (make-bstep (a, b), untrans (a, m, n)))

Theorem: find-m-bump2 (count ≤ n) → (find-m (bump (y, count), 1 + n) = find-m (y, n))

Theorem: termp-beta-step (beta-step (a, b) ∧ termp (a)) → termp (b)

Theorem: termp-reduction (reduction (a, b, list) ∧ termp (a)) → termp (b)

Theorem: find-m-subst ((find-m (x, 1 + n) ≤ m) ∧ (find-m (y, n) ≤ m) ∧ (ind ≤ n)) → (m ≮ find-m (subst (x, y, 1 + ind), n))

;What a beta-step translates back into is alpha-equal to what would've
;been gotten by doing the step directly in the standard form.

Theorem: untrans-subst-nsubst (termp (x) ∧ termp (y) ∧ lambdap (x) ∧ (find-m (y, n) ≤ m) ∧ (find-m (x, n) ≤ m)) → alpha-equal (nsubst (nbody (untrans (x, m, n)),

untrans (y, m, n),

nbind (untrans (x, m, n))), untrans (subst (body (x), y, 1), m, n), bindings (m, n), bindings (m, n))

Theorem: untrans-nbstep (termp (x) ∧ (find-m (x, n) ≤ m)) → alpha-equal (nbstep (w, untrans (x, m, n)),

untrans (bstep (w, x), m, n),

bindings (m, n), bindings (m, n))

Theorem: another-find-m-subst ((find-m (y, n) ≤ m) ∧ (find-m (x, 1 + n) ≤ m) ∧ (ind ≤ n)) → (m ≮ find-m (subst (x, y, 1 + ind), n))

Theorem: untrans-nbstep-zero (beta-step (x, y) ∧ termp (x) ∧ (find-m (x, 0) ≤ m)) → alpha-equal (nbstep (make-bstep (x, y), untrans (x, m, 0)),

untrans (y, m, 0),

nil, nil)

Theorem: beta-step-find-m (beta-step (a, b) ∧ (find-m (a, n) ≤ m)) → (m ≮ find-m (b, n))

Theorem: another-beta-step-find-m beta-step (a, b) → (find-m (a, n) ≮ find-m (b, n))

Theorem: reduction-find-m reduction (a, b, list) → (find-m (a, n) ≮ find-m (b, n))

Event: Enable make-w; name this event ‘g0350’.

Event: Enable make-reduction; name this event ‘g0351’.

;Standard term corresponding to MAKE-W.

Definition: make-n-w (x, y, z, list1 , list2 ) = untrans (make-w (translate (x, nil),

translate (y, nil), translate (z, nil), trans-list (list1 ), trans-list (list2 )),

find-m (translate (x, nil), 0),

           0)

Theorem: alpha-equal-commutes alpha-equal (a, b, x, y) = alpha-equal (b, a, y, x)

Definition: end-cons (x, y) = if listp (y) then cons (car (y), end-cons (x, cdr (y)))

else cons (x, nil) endif

Theorem: end-cons-nreduction (nreduction (a, b, list) ∧ nstep (a1 , a)) → nreduction (a1 , b, end-cons (a, list))

;Translates reductions back.

Definition: make-nreduction (a, b, w, m) = if listp (w)

then cons (nbstep (make-bstep (car (w), b), untrans (car (w), m, 0)),

cons (untrans (car (w), m, 0),

make-nreduction (a, car (w), cdr (w), m)))

else cons (untrans (b, m, 0), cons (nbstep (make-bstep (a, b), untrans (a, m, 0)), nil)) endif

;Reductions translate.

Theorem: reduction-make-nreduction (reduction (a, b, list) ∧ termp (a) ∧ (find-m (a, 0) ≤ m)) → nreduction (untrans (a, m, 0), untrans (b, m, 0), make-nreduction (a, b, list, m))

;Standard convergent reduction corresponding to MAKE-REDUCTION.

Definition: nmake-reduction (x, y, z, list1 , list2 ) = end-cons (untrans (translate (y, nil), find-m (translate (x, nil), 0), 0),

make-nreduction (translate (y, nil),

make-w (translate (x, nil), translate (z, nil), translate (y, nil), trans-list (list2 ), trans-list (list1 )), make-reduction (translate (x, nil),

translate (y, nil), translate (z, nil), trans-list (list1 ), trans-list (list2 )),

find-m (translate (x, nil), 0)))

Theorem: trans-untrans-nil (ntermp (x) ∧ (find-m (translate (x, nil), 0) ≤ m)) → alpha-equal (x, untrans (translate (x, nil), m, 0), nil, nil)

;Church-Rosser theorem for standard representation.  FINALLY-CHURCH-ROSSER
;gives the complete form.

Theorem: standard-church-rosser (nreduction (x, y, list1 ) ∧ nreduction (x, z, list2 ) ∧ ntermp (x)) → nreduction (y,

make-n-w (x, z, y, list2 , list1 ),

nmake-reduction (x, y, z, list1 , list2 ))

Theorem: both-make-n-w-are-same (ntermp (x) ∧ nreduction (x, y, list1 ) ∧ nreduction (x, z, list2 )) → (make-n-w (x, y, z, list1 , list2 ) = make-n-w (x, z, y, list2 , list1 ))

Theorem: finally-church-rosser (ntermp (x) ∧ nreduction (x, y, list1 ) ∧ nreduction (x, z, list2 )) → (nreduction (y,

make-n-w (x, z, y, list2 , list1 ),

nmake-reduction (x, y, z, list1 , list2 ))

∧ nreduction (z, make-n-w (x, z, y, list2 , list1 ), nmake-reduction (x, z, y, list2 , list1 )))

;Now, the Diamond property of walks done directly in the standard notation.

Theorem: free-for-nsubst (free-for (exp, x) ∧ free-for (y, x)) → free-for (nsubst (exp, y, z), x)

Theorem: not-free-in-nsubst (not-free-in (x, exp) ∧ not-free-in (x, y)) → not-free-in (x, nsubst (exp, y, z))

Theorem: not-free-in-nsubst1 (not-free-in (x, y) ∧ (x ∈ N)) → not-free-in (x, nsubst (exp, y, x))

Definition: nwalk (w, x) = if nlambdap (x) then nlambda (nbind (x), nwalk (w, nbody (x)))

elseif ncombp (x)

then if nlambdap (nleft (x)) ∧ (command (w) = 'reduce)

then nsubst (nbody (nwalk (left-instrs (w), nleft (x))), nwalk (right-instrs (w), nright (x)), nbind (nwalk (left-instrs (w), nleft (x)))) else ncomb (nwalk (left-instrs (w), nleft (x)),

nwalk (right-instrs (w), nright (x))) endif

else x endif

Theorem: not-free-in-walk not-free-in (x, exp) → not-free-in (x, nwalk (w, exp))

Theorem: transitivity-of-alpha-equal (alpha-equal (a, b, x, y) ∧ alpha-equal (b, c, y, z)) → alpha-equal (a, c, x, z)

Theorem: free-for-in-walk free-for (exp, x) → free-for (nwalk (w, exp), x)

Definition: free-for-walk (w, x) = if nlambdap (x) then free-for-walk (w, nbody (x))

elseif ncombp (x)

then if nlambdap (nleft (x)) ∧ (command (w) = 'reduce) then free-for (nbody (nleft (x)), nright (x))

∧ free-for-walk (left-instrs (w), nleft (x)) ∧ free-for-walk (right-instrs (w), nright (x))

else free-for-walk (left-instrs (w), nleft (x))

∧ free-for-walk (right-instrs (w), nright (x)) endif

else t endif

Theorem: nlistp-free-for-walk (w ≃ nil) → free-for-walk (w, x)

Definition: free-for-trans-ind (w, x, bounds) = if nlambdap (x)

then free-for-trans-ind (w, nbody (x), cons (nbind (x), bounds))

elseif ncombp (x)

then free-for-trans-ind (left-instrs (w), nleft (x), bounds)

∧ free-for-trans-ind (right-instrs (w), nright (x), bounds) else t endif

Theorem: nbody-untrans (ntermp (x) ∧ lambdap (translate (x, bounds))) → (nbody (untrans (translate (x, bounds), m, n))

= untrans (translate (nbody (x), cons (nbind (x), bounds)), m, 1 + n))

Theorem: free-for-walk-untrans-trans (ntermp (x) ∧ (find-m (translate (x, bounds), length (bounds)) ≤ m)) → free-for-walk (w, untrans (translate (x, bounds), m, length (bounds)))

Theorem: free-for-in-walk1 free-for (x, y) → free-for (nwalk (w1 , x), nwalk (w2 , y))

Theorem: alpha-equal-nsubst (ntermp (x) ∧ ntermp (y) ∧ ntermp (x1 ) ∧ ntermp (y1 ) ∧ nlambdap (x) ∧ nlambdap (x1 ) ∧ free-for (nbody (x), y) ∧ free-for (nbody (x1 ), y1 ) ∧ alpha-equal (x, x1 , bnd, bnd1 ) ∧ alpha-equal (y, y1 , bnd, bnd1 )) → alpha-equal (nsubst (nbody (x), y, nbind (x)),

nsubst (nbody (x1 ), y1 , nbind (x1 )), bnd, bnd1 )

Theorem: nwalk-ntermp ntermp (a) → ntermp (nwalk (w, a))

Theorem: nlambdap-nwalk nlambdap (a) → nlambdap (nwalk (w, a))

Theorem: free-for-nwalk2 (nlambdap (x) ∧ free-for (nbody (x), y)) → free-for (nbody (nwalk (w1 , x)), nwalk (w2 , y))

Theorem: nwalk-alpha (ntermp (a) ∧ ntermp (b) ∧ alpha-equal (a, b, x, y) ∧ free-for-walk (w, a) ∧ free-for-walk (w, b)) → alpha-equal (nwalk (w, a), nwalk (w, b), x, y)

Theorem: nsubst-not-free-in not-free-in (x, a) → (nsubst (a, b, x) = a)

Theorem: nsubst-nsubst (free-for (a, b) ∧ not-free-in (x, c) ∧ (x ≠ y)) → (nsubst (nsubst (a, b, x), c, y) = nsubst (nsubst (a, c, y), nsubst (b, c, y), x))

Definition: sub-nwalk (w, m, u, n) = if nlambdap (m)

then if nbind (m) = n then w

else sub-nwalk (w, nbody (m), u, n) endif elseif ncombp (m) then if (command (w) = 'reduce) ∧ nlambdap (nleft (m))

then list (sub-nwalk (left-instrs (w), nleft (m), u, n), sub-nwalk (right-instrs (w), nright (m), u, n),

              'reduce)

else list (sub-nwalk (left-instrs (w), nleft (m), u, n),

sub-nwalk (right-instrs (w), nright (m), u, n)) endif

elseif m ∈ N then if m = n then u

else w endif else w endif

Theorem: nlambdap-nsubst nlambdap (x) → nlambdap (nsubst (x, y, z))

Theorem: nsubst-twice free-for (a, b) → (nsubst (nsubst (a, b, x), c, x) = nsubst (a, nsubst (b, c, x), x))

Theorem: nwalk-nsubst (free-for (m, x) ∧ free-for-walk (w, m)) → (nwalk (sub-nwalk (w, m, u, n), nsubst (m, x, n))

= nsubst (nwalk (w, m), nwalk (u, x), n))

Definition: free-forx (a, b, x) = if not-free-in (x, a) then t

elseif nlambdap (a) then if nbind (a) = x then t

else not-free-in (nbind (a), b) ∧ free-forx (nbody (a), b, x) endif elseif ncombp (a) then free-forx (nleft (a), b, x) ∧ free-forx (nright (a), b, x) else t endif

Theorem: nsubst-nsubstx (free-forx (a, b, x) ∧ not-free-in (x, c) ∧ (x ≠ y)) → (nsubst (nsubst (a, b, x), c, y) = nsubst (nsubst (a, c, y), nsubst (b, c, y), x))

Theorem: nsubst-twicex free-forx (a, b, x) → (nsubst (nsubst (a, b, x), c, x) = nsubst (a, nsubst (b, c, x), x))

Theorem: free-for-free-forx free-for (a, b) → free-forx (a, b, x)

Definition: free-forx-walk (w, x) = if nlambdap (x) then free-forx-walk (w, nbody (x))

elseif ncombp (x)

then if nlambdap (nleft (x)) ∧ (command (w) = 'reduce)

then free-forx (nbody (nwalk (left-instrs (w), nleft (x))), nwalk (right-instrs (w), nright (x)), nbind (nwalk (left-instrs (w), nleft (x))))

∧ free-forx-walk (left-instrs (w), nleft (x)) ∧ free-forx-walk (right-instrs (w), nright (x))

else free-forx-walk (left-instrs (w), nleft (x))

∧ free-forx-walk (right-instrs (w), nright (x)) endif

else t endif

Theorem: free-for-free-forx-walk free-for-walk (w, x) → free-forx-walk (w, x)

Theorem: free-forx-nsubst (free-forx (x, m, n) ∧ free-forx (x, y, z) ∧ not-free-in (z, m)) → free-forx (nsubst (x, m, n), y, z)

Theorem: free-forx-nsubst2 (free-for (x, m) ∧ free-forx (x, y, z)) → free-forx (x, nsubst (y, m, n), z)

Theorem: nwalk-nlambda1 nlambdap (x) → (nbody (nwalk (u, x)) = nwalk (u, nbody (x)))

Theorem: nwalk-nlambda2 nlambdap (x) → (nbind (nwalk (u, x)) = nbind (x))

Theorem: nwalk-nsubstx (free-for (m, x) ∧ free-forx-walk (w, m)) → (nwalk (sub-nwalk (w, m, u, n), nsubst (m, x, n))

= nsubst (nwalk (w, m), nwalk (u, x), n))

Definition: make-nwalk (m, u, v) = if nlambdap (m) then make-nwalk (nbody (m), u, v)

elseif ncombp (m)

then if (command (u) = 'reduce) ∧ nlambdap (nleft (m))

then sub-nwalk (make-nwalk (nleft (m), left-instrs (u), left-instrs (v)), nbody (nwalk (left-instrs (u), nleft (m))), make-nwalk (nright (m),

right-instrs (u), right-instrs (v)), nbind (nwalk (left-instrs (u), nleft (m))))

elseif (command (v) = 'reduce) ∧ nlambdap (nleft (m)) then list (make-nwalk (nleft (m), left-instrs (u), left-instrs (v)),

make-nwalk (nright (m), right-instrs (u), right-instrs (v)),

                 'reduce)

else list (make-nwalk (nleft (m), left-instrs (u), left-instrs (v)),

make-nwalk (nright (m), right-instrs (u), right-instrs (v))) endif

else u endif

Theorem: free-for-sub-nwalk (free-for (m, x) ∧ free-forx-walk (w, m) ∧ free-forx-walk (u, x)) → free-forx-walk (sub-nwalk (w, m, u, n), nsubst (m, x, n))

Theorem: free-forx-make-nwalk (free-for-walk (u, m) ∧ free-for-walk (v, m)) → free-forx-walk (make-nwalk (m, u, v), nwalk (u, m))

;The Diamond property of beta-walks.

Theorem: diamond-of-beta (free-for-walk (u, m) ∧ free-for-walk (v, m)) → (nwalk (make-nwalk (m, u, v), nwalk (u, m))

= nwalk (make-nwalk (m, v, u), nwalk (v, m)))

Index

alpha-equal, 3, 4, 10, 17–19, 22–26 alpha-equal-commutes, 23 alpha-equal-nsubst, 26 alpha-translate, 10 another-beta-step-find-m, 22 another-bump-subst, 5 another-find-m-subst, 22 append, 13

beta-step, 12–14, 16, 20–22 beta-step-find-m, 22 beta-subst, 14 bindings, 18, 19, 22 both-make-n-w-are-same, 24 both-make-w-are-same, 16 bstep, 20, 22 bump, 4–7, 11, 19–21 bump-bump, 5 bump-lambdap, 5 bump-subst, 5 bump-subst-induct, 5 bump-walk, 6 bump-walk-ind, 6

church-rosser, 9 comb, 4, 6, 10, 14, 15, 20 combp, 4–8, 12, 13, 15, 17, 19–21 command, 6–8, 15, 20, 24, 25, 27–29

diamond-of-beta, 29 diff-zero, 20

end-cons, 23 end-cons-nreduction, 23

finally-church-rosser, 24 find-m, 17–25 find-m-bump, 20 find-m-bump2, 21 find-m-subst, 21 find-m-subst-ind, 20 free-for, 2–4, 12, 18, 24–29 free-for-free-forx, 28 free-for-free-forx-walk, 28 free-for-in-walk, 25 free-for-in-walk1, 26 free-for-nsubst, 24 free-for-nwalk2, 26 free-for-sub-nwalk, 29 free-for-trans-ind, 25 free-for-untrans, 18 free-for-walk, 25–29 free-for-walk-untrans-trans, 25 free-forx, 27, 28 free-forx-make-nwalk, 29 free-forx-nsubst, 28 free-forx-nsubst2, 28 free-forx-walk, 28, 29

g0350, 22 g0351, 22

index, 3, 10–12, 18 index-freevar, 18 index-insert, 12 insert, 10–12

lambda, 4, 6, 10, 13, 14, 20

lambda-reduction, 14

lambda-walk, 6

lambdap, 4–8, 12, 13, 15, 17, 19–21,

25 lambdap-bump, 5 lambdap-subst, 5 lambdap-untrans, 20 left, 4–8, 12, 13, 15, 17, 19–21 left-instrs, 6–8, 15, 20, 24, 25, 27–29 length, 11, 12, 18, 25 list-comb, 14, 15 list-comb-reduction, 14 list-lambda, 13–15 list-make-reduce, 9 list-make-reduce1, 9 litatom-translate, 19

main, 8 make-bstep, 19–23 make-bstep-beta-step, 20 make-n-w, 22, 24 make-nreduction, 23 make-nwalk, 28, 29 make-reduce, 9, 16 make-reduce-reduction, 13, 16 make-reduce-reduction-reduction, 13 make-reduce-steps, 15, 16 make-reduce-steps-steps, 15 make-reduce-walk, 9 make-reduction, 16, 23 make-reduction-walk, 15 make-reduction-walk-steps, 15 make-w, 16, 22, 23 make-walk, 8, 9 make-walk-reduce, 8, 9 make-walk-step, 13 make-walk-step-walks, 13 map-comb-left, 14 map-comb-left-reduction, 14 map-comb-left-reduction2, 14 map-comb-right, 14 map-comb-right-reduction, 14 map-comb-right-reduction2, 14

nbeta-step, 3, 4, 16, 17, 21 nbeta-step-translates, 16 nbind, 2–4, 10–12, 18–21, 24–29 nbody, 2–4, 10–12, 18–21, 24–28 nbody-untrans, 25 nbstep, 20–23 nbstep-nil, 21 ncomb, 2, 17, 20, 25 ncombp, 2–4, 10, 11, 18, 20, 24, 25,

27, 28 nlambda, 2, 17, 20, 24 nlambdap, 2–4, 10–12, 18, 20, 24–29 nlambdap-nsubst, 27 nlambdap-nwalk, 26 nleft, 2–4, 10, 11, 18, 20, 24, 25, 27–

29 nlistp-free-for-walk, 25 nlistp-walk, 6 nmake-reduction, 23, 24 not-free-in, 2, 11, 18, 24–28 not-free-in-corr, 11 not-free-in-nsubst, 24 not-free-in-nsubst1, 24 not-free-in-translate, 11 not-free-in-untrans, 18 not-free-in-walk, 25 not-free-ind, 11 nprecede-index, 11 nreduction, 4, 17, 23, 24 nright, 2–4, 10, 11, 18, 20, 24, 25,

27–29 nstep, 4, 23 nsubst, 2, 4, 12, 16, 19–21, 24, 26–

29 nsubst-ind, 10 nsubst-not-free-in, 26 nsubst-nsubst, 26 nsubst-nsubstx, 27 nsubst-twice, 27 nsubst-twicex, 27 ntermp, 3, 11, 12, 16–19, 24–26 ntermp-astep, 17 ntermp-bstep, 17 ntermp-list, 17 ntermp-subst, 16 ntermp-termp, 18 nwalk, 24–29 nwalk-alpha, 26 nwalk-nlambda1, 28 nwalk-nlambda2, 28 nwalk-nsubst, 27 nwalk-nsubstx, 28 nwalk-ntermp, 26

precede, 10–12 precede-index, 11 precede-index1, 11 precede-index2, 11 reduce, 8, 9, 13, 15, 16 reduce-append, 13 reduction, 13–17, 21–23 reduction-append, 15 reduction-find-m, 22 reduction-make-nreduction, 23 reduction-translates, 17 right, 4–8, 12, 13, 15, 17, 19–21 right-instrs, 6–8, 15, 20, 24, 25, 27–

29

standard-church-rosser, 24 sub-nwalk, 26–29 sub-walk, 7, 8 subst, 4–7, 11–15, 19–22 subst-induct, 5 subst-lambda, 6 subst-not-free-in, 7 subst-nsubst, 11 subst-nsubst2, 12 subst-nsubst2-corr, 12 subst-subst, 7

termp, 17–23 termp-beta-step, 21 termp-bump, 19 termp-ntermp, 18 termp-reduction, 21 termp-subst, 19 the-real-church-rosser, 16 trans-insert-ind, 10 trans-list, 16, 17, 22, 23 trans-untrans, 18 trans-untrans-ind, 18 trans-untrans-nil, 24 transitivity-of-alpha-equal, 25 translate, 10–12, 16–19, 22–25 translate-alpha, 19 translate-insert, 11 translate-insert1, 11 translate-preserves-reduction, 12 translate-preserves-subst, 12

untrans, 17–25 untrans-beta-step, 21 untrans-bstep-ind, 21 untrans-nbstep, 22 untrans-nbstep-zero, 22 untrans-subst, 19 untrans-subst-nsubst, 21 untrans-trans, 19

walk, 6–9, 13, 15 walk-lambda, 8 walk-reduce, 9 walk-subst, 7 walk-subst-ind, 7