Einfuehrung

In dieser Arbeit werden die Beweise des Church-Rosser-Theorems fuer die beta-, eta- und beta-vereinigt-eta-Reduktion des Lamda-Kalkuels gefuehrt.

Die Vorgehensweise wird dem Text More Church-Rosser Proofs von Tobias Nipkow entnommen, die Beweise erfolgen mit dem Saturate-System 2.6.1. Die folgende Beschreibung enthaelt Links zu allen Beweisen.

Die Lambda-Terme werden hierbei nach de-Bruijn-Notation mit Hilfe der folgenden Funktionen formalisiert:

var(I): Variable mit de-Bruijn-Nummer I

abs(S): Abstraktion

app(S,T): Applikation

Definition von lift und subst:

Vorgegeben waren die  Definitionen von

Integers:

X<Y, Y<Z -> X<Z.
X<X -> [].
X<Y, Y<X, X=Y.
X<Y -> X=<Y.
X=<Y -> X<Y,X=Y.
X=<X.

s(X)=s(Y) -> X=Y.
p(X)=p(Y) -> X=Y.
p(s(X))=X.
s(p(X))=X.
 

X<s(X).
X<Y -> s(X)=<Y.
X<Y -> X=<p(Y).
 

lift:

I<K -> lift(var(I),K) = var(I).
K=<I -> lift(var(I),K) = var(s(I)).

lift(app(S,T),K) = app(lift(S,K),lift(T,K)).

lift(abs(S),K) = abs(lift(S,s(K))).
 

und subst:

K<I -> subst(var(I),K,S)=var(p(I)).
       subst(var(I),I,S)=S.
I<K -> subst(var(I),K,S)=var(I).
 

subst(app(T,U),K,S)=app(subst(T,K,S),subst(U,K,S)).

subst(abs(T),K,S)=abs(subst(T,s(K),lift(S,0))).

Die folgende precedence-Deklaration wird bei allen Beweisen beibehalten:

precedence([subst,lift,app,abs,var,s,p,0]).

Die Beweise erfolgen durch Widerspruch:  Das zu beweisende Lemma wird negiert, wobei alle Allquantoren zu Existenzquantoren werden. Man kann dann alle Variablen direkt durch Skolemkonstanten ersetzen, wenn in dem Lemma keine Existenzquantoren vorkamen.

Die Option search_depth(i) dient dazu, die Komplexitaet des Suchraums einzuschraenken. Inferenzen, bei denen beide Praemissen nicht variablenfrei sind, werden nur maximal i mal auf eine Klausel ausgefuehrt (Jede Klausel besitzt einen entsprechenden Zaehler).

Da die meisten Lemmas durch die Negation bereits variablenfrei vorliegen, reicht hier search_depth(0).

Die Option var_overlaps(off) verhindert, dass bei einer Inferenz die Ueberlappung an der Stelle zweier Variablen in den beiden Praemissen stattfindet.

Mit sarp(+[15]) waehlt man eine aufwendigere Technik fuer Redundanzbeweise ("maximal level of reduction"), mit saci([2]) kann constraint inheritance eingestellt werden. Beides haelt den Suchraum kleiner, benoetigt aber selbst mehr Rechenzeit.

Weiterhin werden bei manchen Beweisen drei Lemmas hinzugenommen, die aus den obigen Integer-Axiomen folgen:

X<Y -> s(X)<s(Y).
X=<Y -> s(X)=<s(Y).
X<Y -> s(X)=<Y.
 

Lemmas ueber subst und lift:

Ebenfalls vorgegeben waren folgende sechs Lemmas mit Beweisen:
 

% Lemma 1
lemma1(T,I,K) == (I<s(K) => lift(lift(T,I),s(K))=lift(lift(T,K),I)).
(Beweis)

% Lemma 2
lemma2(T,S,J,I) ==
       (J<s(I) and 0=<J  => lift(subst(T,J,S),I) = subst(lift(T,s(I)),J,lift(S,I))).
(Beweis)
 

% Lemma 3
lemma3(T,S,I,J) ==
       (I<s(J) and 0=<I =>
                lift(subst(T,J,S),I) = subst(lift(T,I),s(J),lift(S,I))).
(Beweis)

% Lemma 4
lemma4(T,S,K) == (subst(lift(T,K),K,S) = T).
(Beweis)

% Lemma 5
lemma5(T,U,V,I,J) ==
        (I<s(J) and 0=<I =>
                subst(subst(T,s(J),lift(V,I)),I,subst(U,J,V)) =
                subst(subst(T,I,U),J,V)).
(Beweis)

% Lemma 6
lemma6(T,I)== (0=<I => subst(T,I,var(I))=subst(T,s(I),var(I))).
(Beweis)
 

beta-Reduktion:

Mit Hilfe von subst ist die Definition der beta-Relation ueber den Lambda-Termen als Praedikat einfach:

beta(app(abs(S),T),subst(S,0,T)).

beta(S,T) -> beta(app(U,S),app(U,T)).

beta(S,T) -> beta(app(S,U),app(T,U)).

beta(S,T) -> beta(abs(S),abs(T)).

Als naechstes wird die reflexive und transitive Huelle von beta definiert:

betas(S,S).

beta(S,T) -> betas(S,T).

(betas(S,T) and beta(T,U)) -> betas(S,U).

(zweite Zeile ist redundant; ich behalte sie bei, um nicht alle Beweise neu testen zu muessen)

Per Induktion ueber betas wird als naechstes bewiesen, dass betas eine Kongruenzrelation ist. Der Beweis gliedert sich in zwei Teile, da der erste die Aussage des zweiten benoetigt:
 

LemmaB3a:

lemmaB3a(S,T,X) == (betas(S,T) =>
                    (betas(abs(S),abs(T)) and
                     betas(app(S,X),app(T,X)) and betas(app(X,S),app(X,T)))).

Der Beweis ist besonders schnell gefunden, da man die Definitionen zu Integers und Substitutionen weglassen kann.

 
LemmaB3b:

lemmaB3b(S,T,U,V) == (betas(S,T) => (betas(U,V) => betas(app(S,U),app(T,V)))).

Mit LemmaB3a und seach_depth(1) ist der Beweis problemlos.

Weitere Lemmas ueber beta folgen spaeter.
 

Definition von free:

Das Praedikat free(S,I) ist genau dann erfuellt, wenn die Variable mit de-Bruijn-Nummer I in S frei ist:

free(var(J),I)<=>(J=I).

free(app(S,T),I)<=>(free(S,I) or free(T,I)).

free(abs(S),I)<=>free(S,s(I)).
 

Folgendes Lemma besagt,  dass bei Substitution einer gebundenen Variable der eingesetzte Term nur ein Dummy ist:
 

LemmaF1:

lemmaF1(S,T,U,I) == ((~free(S,I) and 0=<I) => (subst(S,I,T) = subst(S,I,U))).

Der Beweis gelingt per Induktion ueber die Lambda-Terme ohne Hilfslemmas.
 

Mit demselben Induktionsschema werden diese Lemmas bewiesen, die die Interaktion von free mit lift bzw. subst beschreiben:
 

LemmaF2:

lemmaF2(S,K,I) == ((0=<K and 0=<I) =>
                  (free(lift(S,K),I) <=> (( free(S,p(I)) and K < I) or (free(S,I) and I < K) ))).

Der relativ lange Beweis benoetigt keine weiteren Lemmas.
 

LemmaF3:

lemmaF3(S,T,K,I) == ((0=<I and 0=<K) =>
                    (free(subst(S,K,T),I) <=> ((free(S,K) and free(T,I)) or
                                              ((I<K and free(S,I)) or (K=<I and free(S,s(I))))))).
 

free(subst(abs(t),...,s),..) = free(abs(subst(t,...,lift(s,0))),...) = free(subst(t,...,lift(s,0)),s(...)) = (I.Vor.)
((free(t,...) and free(lift(s,0),...) usw.

Dieser kann nur mit LemmaF2 weiter reduziert werden.
 

eta-Reduktion:

Mir Hilfe von free kann nun auch die Definition der eta-Relation angegeben werden:

~free(S,0) -> eta(abs(app(S,var(0))),subst(S,0,U)).

eta(S,T) -> eta(app(S,U),app(T,U)).

eta(S,T) -> eta(app(U,S),app(U,T)).

eta(S,T) -> eta(abs(S),abs(T)).

Folgendes Lemma zeigt, dass die freien Variablen eines Termes bei der eta-Reduktion erhalten bleiben:
 

LemmaE1:

lemmaE1(S,T,I) == ((0=<I and eta(S,T)) => (free(T,I) <=> free(S,I))).
 

Die eta-Reduktion ist auch abgeschlossen unter Substitution:
 

LemmaE2:

lemmaE2(S,T,U,I) == ((0=<I and eta(S,T)) => eta(subst(S,I,U),subst(T,I,U))).
 

Wie bei beta wird die reflexive und transitive Huelle von eta definiert:

etas(S,S).

eta(S,T) -> etas(S,T).

(etas(S,T) and eta(T,U)) -> etas(S,U).

(zweite Zeile ist redundant)

Ebenfalls wie bei beta wird per Induktion ueber etas bewiesen, dass etas eine Kongruenzrelation ist. Das Beweisschema in zwei Teilen ist fast dasselbe wie bei betas:
 

LemmaE3a:

lemmaE3a(S,T,X) == (etas(S,T) =>
                    (etas(abs(S),abs(T)) and
                     etas(app(S,X),app(T,X)) and etas(app(X,S),app(X,T)))).

(Beweis)

 
LemmaE3b:

lemmaE3b(S,T,U,V) == (etas(S,T) => (etas(U,V) => etas(app(S,U),app(T,V)))).

(Beweis).
 

Parallele beta-Reduktion:

Um die Konfluenz von beta zu zeigen, reicht es nach Lemma (6) im Text, die diamond property einer zwischen beta und betas liegenden Relation zu zeigen. Diese wird als pbeta (par_beta) so definiert:

0=<I -> pbeta(var(I),var(I)).

pbeta(S,T) -> pbeta(abs(S),abs(T)).

(pbeta(S,T) => (pbeta(U,V) => pbeta(app(S,U),app(T,V)))).

(pbeta(S,T) => (pbeta(U,V) => pbeta(app(abs(S),U),subst(T,0,V)))).

Dass pbeta reflexiv ist, muss explizit definiert werden:

pbeta(S,S).

beta ist also eine Teilmenge von pbeta, wie ein kurzer Beweis per Induktion ueber beta zeigt.
Der Beweis, dass pbeta Teilmenge von betas ist, basiert auf der Kongruenzeigenschaft von betas.

Fuer den Beweis der diamond property wird ein Lemma ueber die Vertraeglichkeit von pbeta mit Substitutionen benoetigt. Hierzu zeigt man erst die Vertraeglichkeit mit lift:
 

LemmaP1:

lemmaP1(S,T,I) == ((0=<I and pbeta(S,T)) => pbeta(lift(S,I),lift(T,I))).

Der Beweis per Induktion ueber pbeta benoetigt Lemma2 zur Reduktion von lift(subst(...),...) im letzten Induktionsschritt sowie search_depth(1).

Mit LemmaP1 kann man dann das naechste Lemma per Induktion ueber pbeta(U,V) beweisen:
 

LemmaP2:

lemmaP2(S,T,U,V,I) == ((0=<I and pbeta(S,T) and pbeta(U,V)) =>
                       pbeta(subst(U,I,S),subst(V,I,T))).

Zusaetzlich zu LemmaP1 benoetigt man hier zum Beweis auch Lemma5 zur Umformung von subst(subst(...),...).
 

Takahashi's Proof

Die  diamond property von pbeta
 

dia_pbeta:

dia_pbeta(S,T,X) == ((pbeta(S,T) and pbeta(S,X))
                    => exists(Z,(pbeta(T,Z) and pbeta(X,Z)))).

wird bewiesen, indem man fuer jeden Term S das Z mit der gewuenschten Eigenschaft konstruktiv angibt:
 

comp_th:

comp_th(S,T) == (pbeta(S,T) => pbeta(T,cd(S))).
(completion theorem)

mit folgender Definition von cd:

cd(var(I)) = var(I).

cd(app(var(I),T)) = app(var(I),cd(T)).

cd(app(app(U,V),T)) = app(cd(app(U,V)),cd(T)).

cd(app(abs(S),T)) = subst(cd(S),0,cd(T)).

cd(abs(S)) = abs(cd(S)).

precedence([cd,subst]).

Der Beweis des completion theorem erfolgt per Induktion ueber pbeta(S,T), wobei beim Induktionsschritt nach pbeta(app(S,U),app(T,V))  gemaess der obigen Definition von cd eine Fallunterscheidung vorgenommen wird, naemlich zwischen S=var(I), S=app(X,Y) und S=abs(X).

Im letzteren Fall folgt aus der Annahme, dass die obige Definition von pbeta abgeschlossen ist, zusaetzlich, dass T von der Form abs(Y) fuer ein Y ist. Dann gilt weiterhin pbeta(X,Y).

Fuer den letzten Induktionsschritt wird ausserdem LemmaP2 benoetigt.

Der Beweis der diamond property von pbeta ist jetzt nur noch Formsache. Mit den Folgerungen aus dem Text ist die Konfluenz von beta also hiermit bewiesen.

Man kann den Beweis allerdings auch ohne das completion theorem fuehren. Dazu muss Saturate alle Kandidaten fuer den Existenzquantor, die oben durch cd explizit vorgegeben waren, selbst finden. Hierbei tritt aber ein Problem auf, dass sich am Beispiel folgendes Induktionsschrittes zeigen laesst:

((pbeta(s,t) and pbeta(s,x) and dia_pbeta(s,t,x)) =>
  (dia_pbeta(abs(s),abs(t),y)))

Aus obiger Definition von pbeta laesst sich nicht folgern, welche Form y annehmen muss, denn es wurde nur definiert, wann pbeta gilt, aber nicht, wann pbeta nicht gilt. y kann die Form abs(x) annehmen, aber es laesst sich nicht schliessen, dass dies die einzige Moeglichkeit ist. Das waere aber fuer den Beweis notwendig.

Abhilfe wuerde die Definition des Komplements von pbeta schaffen, aber die laesst sich ohne Existenzquantoren nur aufwendig erstellen (wegen der Komplexitaet des subst).

Einfacher ist es, bei jedem Induktionsschritt eine Fallunterscheidung fuer die verschiedenen Moeglichkeiten durchzufuehren. Im obigen Beispiel gibt es nur eine Wahl fuer y:

((pbeta(s,t) and pbeta(s,x) and dia_pbeta(s,t,x)) =>
  (dia_pbeta(abs(s),abs(t),abs(x))))

Bei anderen Induktionsschritten ist der Aufwand groesser, siehe Beweis.  Mit search_depth(2) findet Saturate dann allerdings alle Kandidaten fuer den Existenzquantor.

Konfluenz von eta

Die Konfluenz von eta folgt laut Text schon aus folgendem Lemma:
 

LemmaE8:

lemmaE8(S,T,X) == ((eta(S,T) and eta(S,X))
                  => exists(Z,((Z=T or eta(T,Z)) and (Z=X or eta(X,Z))))).
 

(~free(s,0) => lemmaE8(abs(app(s,var(0))),subst(s,0,u),subst(s,0,u))),

((~free(s,0) and eta(s,t)) =>
  lemmaE8(abs(app(s,var(0))),subst(s,0,u),abs(app(t,var(0))))), (*)

Beim naechsten Induktionsschritt gibt es vier verschiedene Variationen fuer X:

(eta(s,t) => (

((eta(s,x) and lemmaE8(s,t,x))
   => (lemmaE8(app(s,u),app(t,u),app(x,u))
   and lemmaE8(app(u,s),app(u,t),app(u,x)))) and

(eta(a,b)
   => (lemmaE8(app(s,a),app(t,a),app(s,b))
   and lemmaE8(app(a,s),app(a,t),app(b,s))))

              )),

Der letzte Induktionsschritt von eta liefert zwei Moeglichkeiten,

((eta(s,t) and eta(s,x) and lemmaE8(s,t,x))
   => lemmaE8(abs(s),abs(t),abs(x))),

((~free(s,0) and eta(s,t)) =>
  lemmaE8(abs(app(s,var(0))),abs(app(t,var(0))),subst(s,0,u))),

wobei die letztere aequivalent zu (*) ist und im Beweis weggelassen wird.

Alle Z werden von Saturate automatisch gefunden, wenn man search_depth(4) einstellt und LemmaE1 sowie LemmaE2 hinzunimmt.

Wesentlich schwieriger ist der Beweis der Konfluenz von beta vereinigt eta. Er benoetigt weitere vier Lemmas ueber die Interaktion von beta und eta mit free, lift und subst:
 

LemmaB1:

lemmaB1(S,T,I) == (0=<I => (beta(S,T) => (free(T,I) => free(S,I)))).
 

LemmaB2:

lemmaB2(S,T,U,I) == (0=<I => (beta(S,T) => beta(subst(S,I,U),subst(T,I,U)))).

Zum Beweis mit search_depth(1) benoetigt man Lemma5 zur Umformung von subst(subst(...),...).
 

LemmaE6:

lemmaE6(S,T,I) == ((0=<I and eta(S,T)) => eta(lift(S,I),lift(T,I))).

Der Beweis per Induktion ueber eta benoetigt search_depth(1). Er greift auf zwei weitere Lemmas zurueck, die die Umwandlung von lift(subst(...),...) und free(lift(...),...) beim Induktionsanfang erlauben: Lemma2 und LemmaF2.

Das letzte Lemma ist schliesslich
 

LemmaE7:

lemmaE7(S,T,U,I) == ((0=<I and eta(S,T)) => etas(subst(U,I,S),subst(U,I,T))).
 

Das commutation lemma ist jetzt der Schluessel zum Beweis der Konfluenz von beta vereinigt eta:
 

comm_lemma:

comm_lemma(S,T,X) == ((beta(S,T) and eta(S,X))
                  => exists(Z,(etas(T,Z) and betar(X,Z)))).
 

Die ersten drei bilden den Induktionsanfang, die naechsten beiden den Induktionsschritt beta(S,T) -> beta(abs(S),abs(T)).
Dann folgen noch vier Beweisschritte fuer beta(S,T) -> (beta(app(S,U),app(T,U)) and beta(app(U,S),app(U,T))).
Sie koennen zusammen bewiesen werden, wenn man search_depth(3) einstellt und die eben eingefuehrten Lemmas B1, B2 und E7 hinzunimmt (ausserdem LemmaF1 und LemmaE2  sowie die Kongruenzeigenschaft von etas).

Auffaellig ist, dass die Induktionsvoraussetzung in vielen Faellen nicht benoetigt wird.

Es gibt noch eine weitere Moeglichkeit fuer X beim Schritt beta(S,T) -> beta(abs(S),abs(T)), die allerdings Lemma6 benoetigt:

lemma6(T,I)== (0=<I => subst(T,I,var(I))=subst(T,s(I),var(I))).

Das Lemma muesste von links nach rechts angewandt werden - das laeuft aber der eingestellten lexikographischen Ordnung zuwider. Probiert man es stattdessen in einer separaten Datei mit ordering(sto), gelingt der Beweis.

Fuer die Korrektheit dieses Beweises spricht, dass er alle im Text dafuer vorgesehenen Lemmas benoetigt.

Mit diesem letzten Lemma ist das Church-Rosser-Theorem auch fuer beta vereinigt eta bewiesen.
 
 

Ausblick

Obiges aufwendiges Beweisschema koennte man vereinfachen, indem man das Komplement von beta und eta definiert (Clark's completion). Man koennte  den Beweis des commutation lemma dann per (eventuell mehrfach geschachtelter) Induktion ueber die Lambda-Terme fuehren (erfolgreich ausgefuehrt habe ich das aber noch nicht).

Die Definition ist aufwendig, da sie keine Existenzquantoren enthalten darf.

% Definition des Komplements von beta

beta(var(I),T) -> [].

beta(abs(S),app(U,V)) -> [].
beta(abs(S),var(I)) -> [].
beta(abs(S),abs(T)) -> beta(S,T).

beta(app(var(I),T),var(J)) -> [].
beta(app(var(I),T),abs(S)) -> [].
beta(app(var(I),T),app(U,V)) -> (U=var(I) and beta(T,V)).

beta(app(app(U,V),T),var(J)) -> [].
beta(app(app(U,V),T),abs(S)) -> [].

beta(app(app(U,V),T),app(A,B)) ->
 ((beta(app(U,V),A) and T=B) or (beta(T,B) and A=app(U,V))).

beta(app(abs(var(I)),T),U) ->
 ((i=0 and U=T) or (0<I and U=var(I))).

beta(app(abs(app(U,V)),T),var(J)) -> [].

beta(app(abs(app(U,V)),T),app(A,B)) ->
 ((abs(app(U,V))=A and beta(T,B)) or
  (T=B and beta(abs(app(U,V)),A)) or
  (A=subst(U,0,T) and B=subst(V,0,T))).

beta(app(abs(app(U,V)),T),abs(S)) -> [].

beta(app(abs(abs(S)),T),var(I)) -> [].

beta(app(abs(abs(S)),T),app(U,V)) ->
 ((U=abs(abs(S)) and beta(T,V)) or (T=V and beta(abs(abs(S)),U))).

beta(app(abs(abs(S)),T),abs(X)) -> X=subst(S,s(0),lift(T,0)).
 

%------------------------------------------
 
 

% Definition des Komplements von eta

eta(var(I),T) -> [].
eta(app(U,V),var(I)) -> [].
eta(app(U,V),abs(S)) -> [].
eta(app(U,V),app(A,B)) ->
 ((U=A and eta(V,B)) or (V=B and eta(U,A))).

eta(abs(var(I)),S) -> [].
eta(abs(abs(S)),var(I)) -> [].
eta(abs(abs(S)),app(U,V)) -> [].
eta(abs(abs(S)),abs(T)) -> eta(abs(S),T).

eta(abs(app(U,V)),var(I)) ->
 (U=var(s(I)) and 0<s(I) and V=var(0)).

eta(abs(app(U,V)),abs(var(J))) -> [].
eta(abs(app(U,V)),abs(abs(T))) -> [].

eta(abs(app(U,V)),abs(app(A,B))) ->
 ((U=A and eta(V,B)) or (V=B and eta(U,A)) or
  (subst(U,0,X)=abs(app(A,B)) and ~free(U,0))).

eta(abs(app(U,V)),app(A,B)) ->
 (~free(U,0) and V=var(0) and subst(U,0,X)=app(A,B)).
 
 

Fazit

In vielen Faellen ist es sinnvoll, den Beweis vorher von Hand durchzurechnen, um die genaue Menge der benoetigten Lemmas festzustellen. Sind zuviele unnoetige Hilfslemmas dabei oder ist die Suchtiefe zu gross eingestellt, findet Saturate den Beweis oft nicht oder nicht in angemessener Zeit.

Grossen Einfluss auf das Gelingen eines Beweises hat die precedence-Deklaration. Ausserdem muss in vielen Faellen die Induktionsvorraussetzung mit expliziten Allquantoren verstaerkt werden, wie z.B. hier:

% step case for abstractions
((all(K,all(I,all(S,lemmaF3(t,S,K,I))))) => lemmaF3(abs(t),s,k,i)),

Am besten hat man mehrere Saturate-Laeufe mit verschiedenen Parametern auf verschiedenen Rechnern parallel laufen, um nicht zu lange warten zu muessen.

Nicht zu unterschaetzen sind aber auch Intuition und Erfahrung, die man nach einiger Zeit gewinnt.