Freie  Universität  Berlin   24.01.2012  Institut  für  Informatik   Prof.  Dr.  Helmut  Alt  Proseminar:  Theoretische  Informatik   Referent:  Konrad  Riedel    

Entscheidbarkeit  der  Presburger-­‐Arithmetik    

Seite   1  

Worum  geht  es?  Zu  zeigen,  dass  die  Presburger-­‐Arithmetik  Th(N,  +)  entscheidbar  ist.    

Warum  ist  das  interessant?  Weil  Th(N,  +,  ×)  entgegen  unserer  Intuitionen  nicht  entscheidbar  ist.    

Welchen  Ansatz  verfolgen  wir  hier  allgemein?  Wir  betrachten  die  Aussagen  des  fraglichen  Teilgebiets  der  Mathematik  als  Worte  der  Sprache,  die  alle  wahren  Aussagen  dieses  Teilgebiets  und  nur  diese  enthält.  Dann  untersuchen  wir,  ob  die  Sprache  entscheidbar  ist.    

Wie  sieht  dieser  Ansatz  konkret  aus?    Wir  geben  einen  Algorithmus  an,  der  mit  Hilfe  von  endlichen  Automaten  entscheiden  kann,  ob  seine  Eingabe,  eine  Aussage  φ  in  der  Sprache  von  (N,  +),  in  dem  Modell  wahr  ist.    Sei     φ  =  Q1x1  Q2x2  ...  Qlxl  [  ψ  ],    wobei  Q1,  Q2,  ...,  Ql  jeweils  für  ∀  oder  ∃  stehen  und  ψ  eine  Formel  ohne  Quantoren  mit  Variablen  x1,  x2,  ...,  xl  ist.  Für  jedes  i  von  0  bis  l  definiere  φi  als       φi  =  Qi+1xi+1  Qi+2xi+2  ...  Qlxl  [  ψ  ].    Also  ist  φ0  =  φ  und  φl  =  ψ.    Formel  φi  hat  i  freie  Variablen.  Für  a1,  ...,  ai  ∈  N  sei  φi(a1,  ...,  ai)  die  Aussage,  die  man  erhält,  wenn  man  die  freien  Variablen  x1,  ...,  xi  in  φi  durch  die  Konstanten  a1,  ...,  ai  ersetzt.    Für  jedes  i  von  0  bis  l  konstruiert  der  Algorithmus  einen  endlichen  Automaten  Ai,  der  die  Menge  aller  Worte,  welche  i-­‐Tupel  von  Zahlen  darstellen,  akzeptiert,  die  eine  erfüllende  Belegung  von  φi  sind.    Der  Algorithmus  konstruiert  zuerst  Al.  Danach  konstruiert  der  Algorithmus  für  jedes  i  von  l  bis  0  Ai-­‐1  mit  Hilfe  von  Ai.  Schließlich  prüft  der  Algorithmus,  ob  A0  das  leere  Wort  ε  akzeptiert.  Tut  er  das,  so  ist  φ  wahr,  andernfalls  falsch.      

Definitionen    Wir  definieren  nun  zuerst  das  Nötige  um  den  Beweis  führen  zu  können.        

Freie  Universität  Berlin   24.01.2012  Institut  für  Informatik   Prof.  Dr.  Helmut  Alt  Proseminar:  Theoretische  Informatik   Referent:  Konrad  Riedel    

Entscheidbarkeit  der  Presburger-­‐Arithmetik    

Seite   2  

Das  Alphabet  unserer  Sprache  ist  {∧,  ∨,  ¬,  (,  ),  [,  ],  ,,  ∀,  ∃,  x,  R1,  ...,  Rk}.    

– R1,  ...,  Rk  bezeichnen  Relationen.  – x  bezeichnet  Variablen,  wobei  unterschiedliche  Variablen  nicht  mit  Indizes  

unterschieden  werden,  sondern  durch  unterschiedliche  Anzahl  an  Wiederholungen  (x,  xx,  xxx,  ...).  

– Die  übrigen  Symbole  sind  bekannt.    Eine  Formel  ist  ein  wohlgeformtes  Wort  über  diesem  Alphabet.  Ein  Wort  ist  eine  Formel,  wenn  es    

– eine  atomare  Formel  ist,  – die  Form  φ1  ∧  φ2  oder  φ1  ∨  φ2  oder  ¬φ1  hat,  wobei  φ1  und  φ2  kleinere  Formeln  

sind  oder  – die  Form  ∃xi  [  φ1  ]  oder  ∀xi  [  φ1  ]  hat,  wobei  φ1  eine  kleinere  Formel  ist.  

 Eine  atomare  Formel  hat  die  Form  Ri(x1,  ...,  xj).    Der  Wert  j  gibt  die  Stelligkeit  der  Relation  an.    Wir  gehen  davon  aus,  dass  alle  Formeln  in  Pränexform  vorliegen.  D.h.,  dass  alle  Quantoren  am  Anfang  der  Formel  stehen.    Eine  Formel  ohne  freie  Variablen  nennen  wir  Aussage.    Ein  Modell  M  ist  ein  Tupel  der  Art  (U,  P1,  ...,  Pk),  wobei  U  ein  Universum  ist  und  P1,  ...,  Pk  Relationen  sind,  die  den  Symbolen  R1,  ...,  Rk  zugewiesen  werden.    Die  Sprache  eines  Modells  ist  die  Menge  der  Formeln,  die  nur  die  Relationensymbole  nutzen,  denen  das  Modell  Relationen  zugewiesen  hat,  und  alle  Relationensymbole  mit  ihrer  korrekten  Stelligkeit  verwenden.    Die  Theorie  vom  Modell  M ,  geschrieben  Th(M),  nennen  wir  die  Menge  der  wahren  Aussagen  der  Sprache  des  Modells  M.         Beweis    Al  kann  problemlos  konstruiert  werden,  da  φl  =  ψ  keine  Quantoren  enthält,  also  nur  unsere  Additionsrelation  (+)  sowie  junktorenlogische  Verknüpfungen  (∧,  ∨,  ¬).    Die  Additionsrelation  +(a,  b,  c)  ist  genau  dann  wahr,  wenn  a+b=c  wahr  ist.  Ein  endlicher  Automat  zur  Auswertung  einer  Additionsrelation  kann  wie  folgt  konstruiert  werden:      

Freie  Universität  Berlin   24.01.2012  Institut  für  Informatik   Prof.  Dr.  Helmut  Alt  Proseminar:  Theoretische  Informatik   Referent:  Konrad  Riedel    

Entscheidbarkeit  der  Presburger-­‐Arithmetik    

Seite   3  

 Wir  definieren  das  Eingabealphabet  wie  folgt:  

   Dabei  ist  jede  'Zeile'  als  eine  binärkodierte  Zahl  zu  lesen  und  die  Additionsrelation  ist  wahr  genau  dann,  wenn  die  Zahl  der  ersten  Zeile  +  die  Zahl  der  zweiten  Zeile  =  die  Zahl  der  dritten  Zeile.    Der  endliche  Automat,  der  genau  die  Worte  aus  ∑3*  die  einer  wahren  Additionsrelation  entsprechen  akzeptiert,  sieht  wie  folgt  aus:  

   Al  muss  mehrere  Additionsrelationen  im  Zusammenhang  auswerten.  Daher  erweitern  wir  unser  Eingabealphabet  wie  folgt:  

   Hiermit  können  wir  dem  Automaten  i  verschiedene  Zahlen  als  Eingabe  übergeben.  Wir  konstruieren  Al,  indem  wir  für  jede  abzubildende  Additionsrelation  einen  Automaten  wie  oben  beschrieben  konstruieren,  wobei  ein  Automat  jeweils  nur  die  drei  für  ihn  relevanten  Zeilen  liest.  Dann  verknüpfen  wir  diese  Automaten  durch  Anwendung  der  Konstruktionsregeln,  die  den  Mengenoperationen  Vereinigung,  Schnitt  und  Komplementbildung  entsprechen.    Da  die  Satzmenge,  die  von  einem  endlichen  Automaten  akzeptiert  wird,  eine  reguläre  Sprache  ist  und  die  regulären  Sprachen  gegenüber  Schnitt,  Vereinigung  und  Komplementbildung  abgeschlossen  sind,  können  wir  den  obigen  Automaten  also  so  erweitern,  dass  er  auch  die  junktorenlogischen  Verknüpfungen  verschiedener  Additionsrelationen  auswertet  und  immer  noch  ein  endlicher  Automat  ist.  

Freie  Universität  Berlin   24.01.2012  Institut  für  Informatik   Prof.  Dr.  Helmut  Alt  Proseminar:  Theoretische  Informatik   Referent:  Konrad  Riedel    

Entscheidbarkeit  der  Presburger-­‐Arithmetik    

Seite   4  

 Wir  können  also  den  Automaten  Al  konstruieren.  Dieser  Automat  akzeptiert  alle  Eingaben,  die  erfüllende  Belegungen  von  φl  darstellen.  Jetzt  wollen  wir  schrittweise  weitere  Ai  konstruieren  bis  wir  A0  konstruiert  haben.    A0  akzeptiert  alle  Eingaben,  die  erfüllende  Belegungen  von  φ0  darstellen.  Da  φ0  aber  keine  freien  Variablen  mehr  enthält,  akzeptiert  A0  jede  beliebige  Eingabe  genau  dann,  wenn  φ0  (und  damit  φ)  wahr  ist.    Dazu  geben  wir  an,  wie  man  aus  Ai  Ai-­‐1  konstruiert.  Dafür  unterscheiden  wir  zwei  Fälle:    1.)  φi-­‐1  =  ∃xi  φi  2.)  φi-­‐1  =  ∀xi  φi    Im  ersten  Fall  konstruieren  wir  Ai-­‐1  wie  Ai,  wobei  Ai-­‐1  nichtdeterministisch  den  Wert  von  ai  rät  anstatt  ai  als  Teil  der  Eingabe  zu  erhalten.    Im  zweiten  Fall  gilt  ∀xi  φi  =  ¬∃xi  ¬φi  und  wir  konstruieren  einen  endlichen  Automaten,  der  das  Komplement  der  Sprache  von  Ai  akzeptiert,  verfahren  dann  damit  wie  im  ersten  Fall  und  konstruieren  schließlich  einen  Automaten,  der  das  Komplement  der  Sprache  jenes  Automaten  akzeptiert.    Mit  diesen  beiden  Konstruktionsvorschriften  können  wir  alle  Automaten  von  Al-­‐1  bis  A0  konstruieren  und  da  A0  'berechnet',  ob  φ  wahr  ist,  sind  wir  fertig.    Dieser  Algorithmus  führt  letztlich  nur  zu  zwei  verschiedene  Automaten.  Dem,  der  jede  Eingabe  akzeptiert,  und  dem,  der  keine  akzeptiert.  

       

Quelle  M.  Sipser  Introduction  to  the  Theory  of  Computation  PWS  Publ.Comp.  1997  Kapitel  6.2