Rechnergestütztes Beweisen (Hofmann, WS 2005/06)

2005-11-30 VL 13

Gleichungstheorien
==================

Motivation und Anwendung: 
Lineare Arithmetik + uninterpretierte Funktionssymbole

Bsp 1:  Zeige 0=1 aus
f(x-1)-1 = x+1
f(y)+1   = y-1
y+1 = x

Bsp 2: Zeige f(x)=x aus f^5(x)=x und f^3(x)=x

Zwei Entscheidungsverfahren:
----------------------------

Nelson-Oppen: Kombination zweier (entscheidbarer) Gleichungstheorien,
z.B. lin. Arith. und uninterp. F.S.

Shostak: Kombination einer Gleichungstheorie mit uninterp. F.S.  In
seinem Anwendungsfeld besser als N.-O.


Def. (Gleichung)  Sei L eine Sprache und t1 und t2 zwei Terme,
so dass

  K >L t1 : tau
  K >L t2 : tau

Eine Gleichung ist ein formaler Ausdruck

  K >L t1 = t2 : tau

kurz geschrieben als t1 = t2.

Ist II Interpretation von L und t1=t2 eine Gleichung, so erfüllt II
die Gleichung t1=t2, in Zeichen 

  II |= t1 = t2, 

falls [|t1|]_II,rho = [|t2|]_II,rho für alle Belegungen rho.

Def. (Gleichungstheorie)  Eine Gleichungstheorie ist eine Menge von T
von Gleichungen über einer Sprache L, die unter den folgenden Regeln
abgeschlossen ist:

  (REFL)  t=t in T  (für alle (wohltypisierten) t).

  (SYM)   Wenn t1=t2 in T, dann auch t2=t1 in T.

  (TRANS) Wenn t1=t2 und t2=t3 in T, dann auch t1=t3 in T.

  (CONG)  Wenn ti=ui in T für i=1..n, dann auch 
            f(t1..tn)=f(u1..un) in T.

  (SUBST) Wenn t1=t2 in T, dann auch t1(x:=u) = t2(x:=u) in T.

Zu jeder Menge M von Gleichungen existiert eine kleinste Gl.th. 
T = <M>  mit  M <= T  (das ist einfach der Abschluss von M unter den 5
Regeln).  Man schreibt

  M |- t = u

falls t=u in <M>.

Bem.  Ist II eine Interpretation, so ist

  Th(II) = { "t=u" | II |= t=u }

eine Gleichungstheorie.

Satz (Birkhoff).  Zu jeder Gleichungstheorie T existiert eine
Interpretation II, so dass T = Th(II).  Diese Int. ist das universelle
Modell von T.

Beweis.  Sei L_oo die Erweiterung von L durch unendlich viele
Konstanten von jedem Typ.  Identifiziere Variablen mit diesen neuen
Konstanten.  II wird wie folgt definiert:

  [|tau|] = { t | >L_oo t : tau }/~  wobei t1~t2 gdw. t1=t2 in T (*)

  [| f |]([t1]~..[tn]~) = [f(t1..tn)]~ (**)

(*) wobei auf der rechten Seite die neu eingeführten Konstanten als
Variablen aufgefasst werden.  ~ ist Äquivalenzrelation wegen (REFL),
(SYM), (TRANS).

(**) Wohldefiniert wegen (CONG).

Noch zu zeigen II |= t1 = t2 gdw. t1=t2 in T.

"<="  Sei t1=t2 in T.  Zeige [|t1|]_rho = [|t2|]_rho.  Sei

  rho = x1->[u1]~,...,xn->[un]~

Dann [|t1|]_rho = [t1(x1:=u1,...,xn:=un)]~  (durch Induktion über t1)
                = [t2(x1:=u1,...,xn:=un)]~  (wegen SUBST)
                = [|t2|]_rho                (durch Induktion über t2)

"=>" Sei II |= t1 = t2.  Setze rho(x)=[^x]~ wobei ^x die zu x gehörige
neue Konstante ist.  Dann gilt

     [|t1|]_rho = [t1(xi:=^xi)]~  (wieder durch Induktion über t1)
   = [|t2|]_rho = [t2(xi:=^xi)]~  (")

Also t1=t2 in T.


Beispiel: Sei L = {+,*,-,0,1} und T die Theorie der Ringe, d.h., T =
<M>, wobei M={Ringaxiome} (siehe Übung 5).

Satz von Jacobson.  Sei R ein Ring.  Falls zu jedem x in R ein n > 1
existiert, so dass x^n = x (d.h. der Ring ist nilpotent), dann ist R
kommuntativ (x*y=y*x).  (Bem. diese Spezifikation ist keine
Gleichungstheorie.)

Speziallfall: Erfüllt ein Ring die Gleichung x*x*x=x, so ist R
kommutativ.

Folgerung aus Birkhoff: Es existiert eine Herleitung von x*y=y*x aus
den Ringaxiomen und der Gleichung x^3=x mit den Gleichungsregeln
(REFL--SUBST).
Bew: Wende Satz von Jacobson auf das universelle Modell
<Ringaxiome,x^3=x> an.

Herleitung für n=3 (Thierry Coquand):

  e1 = 1-u     u=x^2
  e2 = u(1-v)  v=(1-x)^2
  e3 = uv

  xy = (e1 + e2 + e3)xy
     = e1xy + e2xy + e3xy
     = e2y - e3y
     = e1yx + e2yx + e3yx 
     = yx

Satz (Konvexität).
Sei T Gleichungstheorie.  Seinen t1=u1,...,tn=un Gleichungen, so dass
für jedes Modell II von T und Belegung rho ein i existiert, so dass
  
  [|ti|]_II,rho = [|ui|]_II,rho

(D.h.: T |= FORALL xs. t1=u1 OR ... OR tn=un.)
Dann existiert ein i, so dass ti=ui in T.  
(D.h. T |= ti=ui für dieses i.)

Beweis: Betrachte das universelle Modell II von T und die "universelle
Belegung" rho(x)=^x.  Nach Voraussetzung existiert ein i, so dass

  [ti]~ = [|ti|] = [|ui|] = [ui]~

Bem: Man sagt, jede Gleichungstheorie ist konvex.

Bsp: Die Theorie T der Bool'schen Werte ist nicht konvex, da gilt

  T |= FORALL x. x=true OR x=false

aber weder FORALL x.x=true noch FORALL x.x=false.  T ist eben keine
reine Gleichungstheorie.


Ziel: Gegeben Gleichungstheorie T.
- Entscheide, ob t=u in T für eine Gleichung t=u.
- Entscheide, ob T |= FORALL xs. t1=u1 AND ... AND tn=un IMPLIES t=u

Def. Eine Gleichungstheorie T ist kanonisierbar, wenn eine
berechenbare Funktion sigma : Terme -> Terme existiert, so dass

  (C1)  sigma(t) = t in T

  (C2)  Wenn t1 = t2 in T, dann ist sigma(t1)==sigma(t2) (identisch).

Folgerung: Falls sigma(t1)=sigma(t2), dann t1 = t2 in T.  (C1,TRANS)