Einleitung, Überblick

Inhalt und Ziel der Vorlesung

(Quelle: Modulbeschreibung)

Ist jede Funktion \(\mathbb{N}\to\mathbb{N}\) berechenbar?

Nein! (Das ist ein wichtiges Resultat und wir sehen eine wichtige Beweismethode.)

Eigenschaften von Grammatiken

gesucht ist jeweils Algorithmus mit dieser Eigenschaft:

Eingabe ist Paar \((G_1,G_2)\) von Grammatiken,
Ausgabe ist 1, falls \(L(G_1)=L(G_2)\), sonst 0

praktische Motivation: Test bzw. Verkleinerung von regulären Ausdrücken, von Grammatiken (automatische Bewertung von Übunsgaufgaben zu AFS!)

Methode: Reduktion: wenn \(E_2\) entscheidbar, dann auch …

Sind diese Aufgaben gleich schwer?

(eine typische Frage der Komplexitätstheorie)

Praktische Problemstellungen

Berechenbarkeitsmodell \(=\) Programmierparadigma

für jede dieser Def.:

zwischen diesen Def.:

Geschichte des Algorithmenbegriffs

Suche nach Lösungsverfahren für mathematische Aufgaben (symbolische Differentiation, Integration, Gleichungssysteme)

…bzw. nach Beweisen für deren Nicht-Existenz

Bedeutung des Algorithmenbegriffs

(nach K. Wagner: Theor. Inf., Springer 2003)

Literatur

(akt.) Lehrbücher

Klassisch:

Registermaschinen

Motivation, Eigenschaften

wir formalisieren das imperative Programmieren:

Eigenschaften dieses Modells:

Semantik: Speicher

Syntax: Befehle und Programme

Bsp. für ein Programm:

[GotoZ 1 5,Dec 1,Inc 0,Inc 0,Goto 0,Stop] 

Semantik: Befehle

Semantik: Programme

Ü: ein \(p\), das die Funktion \(b(x_1)=42\) berechnet?
Ü: die Semantik des leeren Programms (mit \(|p|=0\)) ist?

Ein Programm für \(x\mapsto 2x\)

[GotoZ 1 5,Dec 1,Inc 0,Inc 0,Goto 0,Stop] 

wirklich? glauben wir das? nein. wir beweisen:

wir ordnen jeder Konfiguration \((l,s)\) zu:

und zeigen (für die Teilfolge aller Konfig. mit \(l=0\)):

Elementare goto-berechenbare Fkt.

diese Funktionen sind goto-berechenbar:

Abschluß-Eigenschaften

Zusammenfassung GOTO (bis jetzt)

später werden wir sehen

Übungsaufgaben

  1. GOTO-Programme für elementare Funktionen: in Olat/Autotool ausprobieren. (Ggf. Highscore-Wertung für kurze Programme.)

  2. Ü: gilt \(s[a:=b][c:=d] = s[c:=d][a:=b]\) ?

  3. Beweisen Sie: die Relation \(\operatorname{step}_p^*\cap \{(C_1,C_2)\mid C_2 \text{ist final}\}\) ist eine partielle Funktion.

    (Dabei Wdhlg. Begriffe und Notation für Relationen und partielle Funktionen.)

  4. Sei \(A\) die Menge der partiellen Fkt., die durch ein Goto-Programm berechnet werden können, in dem der Befehl Goto nicht vorkommt. Beweisen Sie \(\text{GOTO} = A\).

    Das sind zwei Inklusionen, die eine ist trivial, für die andere übersetzen Sie einen unbedingten in einen bedingten Sprung.

  5. Sei \(B\) die Menge der partiellen Fkt., die durch ein Goto-Programm berechnet werden können, in dem der Befehl GotoZ nicht vorkommt (m.a.W., nur unbedingte Sprünge),

    Geben Sie ein Verfahren an, das entscheidet, ob ein \(B\)-Programm eine totale Funktion berechnet.

  6. Sei \(C\) die Menge der partielle Ftk., die durch ein Goto-Programm berechnet werden können, in dem weder Goto noch GotoZ vorkommen (m.a.W., die Geradeaus-Programme).

    Welche Geradeaus-Programme berechnen totale Funktionen?

    Beweisen Sie \(B=C\). (zwei Inklusionen, d.h. zwei Compiler)

Vergangenheit und Zukunft

Aktueller Stand der Vorlesung: wir sind hier

Strukturierte Programmierung

Motivation

Goto-Programme sind flach (Listen von Befehlen), haben keine sichtbare Struktur. Das ist gut für die Hardware, schlecht für den Programmierer.

Struktur \(=\) Hierarchie \(=\) Bäume.

Programme sind ab jetzt Bäume. (entspricht etwa dem Schritt von Assembler/Fortran zu Algol, \(\approx\) 1960)

NB: Das ist immer noch imperative Programmierung, deswegen immer noch schlecht für den Programmierer (weil die Semantikdefinition einen Maschinenzustand benutzt, den man im Programm nicht sieht).

Ausweg: funktionale Programmierung (kein Zustand).

Syntax

Menge der While-Programme \(P\)

Beispiel:

Semantik (Prinzip, elementare Prog.)

Semantik eines Programms \(p\in P\)

ist Relation (genauer: partielle Funktion) \(\operatorname{sem}_p\subseteq S\times S\) auf Speicherbelegungen.

beachte: es gibt keinen program counter, diese Rolle übernimmt der Index \(p\).

Semantik für elementare Programme: \(\operatorname{sem}_p(s_1,s_2)=\)

Semantik für zusammengesetzte Prog.

\(\operatorname{sem}_p(s_1,s_2) = \dots\)

Notation \(p\cong q \iff \operatorname{sem}_p=\operatorname{sem}_q\). — Ü: Satz

Ü: \(\operatorname{\textsf{IfZ}}\) wird gar nicht benötigt, da man es simulieren kann.

While-berechenbare Funktionen

Übungsaufgaben:

Ein Interpreter für \(\operatorname{\textsf{WHILE}}\)

Interpreter realisiert Semantik. Echter autotool-Quelltext:

http://autolat.imn.htwk-leipzig.de/gitweb/?p=tool;f=collection/src/While/Step.hs;hb=for-ghc-7.8

Konfiguration \(c=(t,m)\) enthält

mit der Bedeutung: wenn \(t=[p_1,\ldots,p_n]\), dann ist \(\operatorname{\textsf{Seq}}(t):=\operatorname{\textsf{Seq}}(p_1,\ldots,\operatorname{\textsf{Seq}}(p_n,\operatorname{\textsf{Skip}})\dots)\) noch auszuführen.

Es wird jeweils das oberste Teilprogramm \((p_1)\) analysiert.

Spezifikation (Korrektheit): \(\operatorname{sem}_{\operatorname{\textsf{Seq}}(t)}(i,f) \iff\) \(\left(|t|=0\wedge i=f\right) \vee \left(\exists t', m: (t,i)\to(t',m) \wedge \operatorname{sem}_{\operatorname{\textsf{Seq}}(t')}(m,f) \right)\)

es soll gelten: Satz: \(\operatorname{sem}_p(i,f)\iff ([p],i)\to^*([],f)\)

Beziehungen zw. Goto- und While-B.

Satz (Ziel): für jede part. Fkt. \(f\) gilt:

praktisches Argument für \(\Rightarrow\): das macht jeder Compiler (etwa von C nach Assembler/Maschinensprache)

Beweis (Ideen): folgen.

(Wenn man das genau macht, dann heißt die Vorlesung Compilerbau)

Von While zu Goto (Prinzip)

wir schreiben den Übersetzer:

\(\operatorname{\textsf{compile}}:\mathbb{N}\times\operatorname{\textsf{WHILE}}\to \mathbb{N}\times \operatorname{\textsf{GOTO}}\)

wobei \(\operatorname{\textsf{compile}}(a,p)=(e,q)\) bedeutet:

dabei bedeutet Äquivalenz:

\(\forall p\in\operatorname{\textsf{WHILE}},a\in\mathbb{N}:\) sei \((e,q)=\operatorname{\textsf{compile}}(a,p)\),

dann \(\forall s_1,s_2: \operatorname{sem}_p(s_1,s_2) \iff \operatorname{step}_q^*((a,s_1),(e,s_2))\)

Von While zu Goto (elementar, Seq)

einfache Programme:

zusammengesetzte:

Von While zu Goto (IfZ)

Ansatz:

compile (_, IfZ i p1 p2) =>
  A: GotoZ i M
     compile (_, p2) ; 
     Goto E ; 
  M: compile (_, p1); 
  E:

Realisierung:

compile (a, IfZ i p1 p2) = 
  let (h,q2) = compile (a+1,p2)
      (e,q1) = compile (h+1,p1)
  in  (e,   [GotoZ i (h+1)] ++ q2 
         ++ [Goto e] ++ q1)

Von While zu Goto (While)

Ansatz:

compile (_, While i p) =>
  A: GotoZ i E
     compile (_, p) ; 
     Goto A ; 
  E:

Realisierung:

compile (a, While i p) = 
  let (h,q) = compile (a+1,p)
      e = h+1
  in  (e, [GotoZ i e] ++ q ++ [Goto a] 

Von While zu Goto (insgesamt)

Satz: Für jedes While-Programm \(p\) existiert ein Goto-Programm \(q\), das dieselbe partielle Funktion berechnet wie \(p\).

(äquivalente Formulierung: \(\operatorname{\textsf{WHILE}}\subseteq\operatorname{\textsf{GOTO}}\))

Beweis(plan):

http://autolat.imn.htwk-leipzig.de/gitweb/?p=tool;f=collection/src/Compiler/While_Goto.hs;hb=for-ghc-7.8

Von Goto zu While

das scheint schwieriger:

Es geht aber, und das erzeugte While-programm hat eine ganz besondere (einfache) Struktur, die später noch ausgenutzt wird (Kleene-Normalform-Thm)

Von Goto nach While: Ansatz

Eingabe: goto-Programm \(p\),
Ausgabe: äquivalentes While-program \(q\)

bestimme \(c=\) das erste in \(p\) nicht benutzte Register, das verwenden wir als PC. Das nächste Register \(h\) verwenden wir zum Anhalten.

Struktur von \(q\) ist:

Inc h;
While (h) {
  if (c == 0) { ... } else {
    if (c == 1) { ... } else {   
      if (c == 2) { ... } else { 
        ..                  else Skip
} 

Von Goto nach While: Einzelheiten

für Befehl \(p_i\) erzeuge: if (c==i) q_i else mit \(q_i=\)

Ü: zeige: \(p\) erreicht \(\operatorname{\textsf{Stop}}\) \(\iff\) \(q\) hält.

beachte dabei auch den Fall \(\operatorname{\textsf{Goto}}l\) mit \(l\ge |p|\)

Ü: hier wird if(c==i) und \(c:=l\) benutzt,
das kann man jeweils mit While implementieren,
geht hier aber auch ohne Schleife, warum?

http://autolat.imn.htwk-leipzig.de/gitweb/?p=tool;f=collection/src/Compiler/Goto_While.hs;hb=for-ghc-7.8

Das Normalform-Theorem für While

Vorige Konstruktion zeigt den Satz:

zusammen mit \(\operatorname{\textsf{WHILE}}\subseteq\operatorname{\textsf{GOTO}}\) folgt

äquivalent\(=\) berechnet dieselbe partielle Funktion.

Ü: wie unterscheiden sich die Laufzeiten?

Garantierte Termination: Loop

Motivation

Loop-Programme

Syntax und Semantik wie While-Programme, außer:

Jede so berechenbare Fkt. heißt loop-berechenbar.

Satz: \(f\) ist prim.-rek \(\iff\) \(f\) ist loop-berechenbar.

Beweis: \(\Rightarrow\): folgt aus früherer Übersetzung

\(\Leftarrow\): durch Iteration der Zust-Überführungs-Funktion

Primitiven Rekursion und Softwaretechnik

Primitiven Rekursion und Softwaretechnik (II)

Kodierung strukturierter Daten

Motivation

Kodierung von Zahlenpaaren

gesucht sind (goto-berechenbare) Funktionen

mit Spezifikation (vgl. objektorientierte Datenmodellierung)

da gibt es viele verschiedene Möglichkeiten

Ü: jeweils \(C(2,3), C(3,2), T(10), T(12), P_1(12),P_2(12)\),

Algorithmen (goto-Programme) für \(T, P_i\).

Kodierung von Listen

Kostruktor: \(L:\mathbb{N}^*\to \mathbb{N}\), Destruktoren \(D_i:\mathbb{N}^*\hookrightarrow \mathbb{N}\).

zwei (von vielen) Möglichkeiten:

Ü: jeweils \(L([1,2,3])\), Algorithmus für \(D_i\)

Ü: die Funktion \(p:n\mapsto\) die \(n\)-te Primzahl, also \(p(0)=2, p(1)=3, p(2)=5,\dots\) ist goto-berechenbar

Kodierung von Bäumen

Motivation

Realisierung: \(B(t) = C(\text{num}(\text{root}(t)), L([B(t_1),\ldots,B(t_k)]))\)

mit \(\text{args}(t)=[t_1,\ldots]\), Paar-Kodierung \(C\),
Listen-Kodierung \(L\), sowie Symbol-Numerierung

Ü: Kodierung für endliche Mengen von Zahlen

Universelle Programme und Halteproblem

Kodierung von Programmen

man kann mit eben gezeigten Methoden nach \(\mathbb{N}\) kodieren:

Damit kann man in der Sprache GOTO
einen Interpreter für GOTO-Programme schreiben.

Ein universelles Goto-Programm

Das Halteproblem

Def: das (spezielle) Halteproblem ist die Menge \(K_0 = \{ x \mid \phi_x(x)\downarrow \}\subseteq\mathbb{N}\).

(die Menge der Kodierungen von Programmen, die anhalten, wenn man sie auf sich selbst, d.h. ihren eigenen Code, anwendet).

Satz: die charakteristische Funktion \(c_{K_0}:\mathbb{N}\to\{0,1\}\) der Menge \(K_0\) ist nicht goto-berechenbar.

Beweis (indirekt): falls doch, dann gibt es ein Programm, das \(c_{K_0}\) berechnet. Es gibt dann auch ein Programm

\(x\mapsto\) wenn \(c_{K_0}(x)=0\), dann 1, sonst \(\bot\) (eine nicht haltende Rechnung).

Sei \(q\) der Code dieses Programms. Ist \(q \in K_0\)? Gdw. \(\phi_q(q)\downarrow\), gdw. \(c_{K_0}(q)=0\), gdw. \(q\notin K_0\).

Das Halteproblem (Folgerung)

Es gibt also kein allgemeines Verfahren, mit dem man entscheiden kann, ob ein Programm für eine Eingabe nach endlich vielen Schritten hält.

Diagonalisierung

schon zweimal benutzt, und kommt noch öfter:

Anwendungen bisher:

Maschinenunabhängige Berechenbarkeitstheorie

Motivation

These von Church und Turing

alle intuitiv vernünftigen Berechenbarkeitsmodelle definieren die gleiche Klasse von partiellen Funktionen

ein Berechnungsmodell ist gegeben durch

und bestimmt \(M = \{ \vec{x}\mapsto \phi_p(C(\vec{x})) \mid p\in\mathbb{N}\}\)

Die C-T-These kann man als empirische Aussage auffassen oder als Definition (\(M\) ist vernünftig \(\iff\) es gibt beide Compiler \(M \leftrightarrow \Part\)), daraus folgt z.B.

Das \(s^m_n\)-Theorem

Anschaulich: Spezialisierung eines Programms. Formal:

Satz: es gibt eine berechenbare Funktion \(s^m_n:\mathbb{N}^{1+m}\to\mathbb{N}\),
die zu \((p,\vec{x})\) ein passendes \(q\) bestimmt.

Beachte: Programm \(p\) wird transformiert, nicht ausgeführt.

Ü: \(s^1_1\) (möglichst) konkret angeben

Ü: Sei \(p\) (ein Programm für) die Addition. Was ist \(s^1_1(p,1)\)?

Ein Fixpunktsatz

Satz (Stephen Kleene, 1938): Sei \(f\) total und berechenbar.
Dann gibt es ein \(i\) mit \(\phi_i = \phi_{f(i)}\).

Beweis:

Ü: wende Satz an auf die Funktion
\(f: x\mapsto\) ein Index für die konstante Funktion \(y \mapsto x\).

Der Fixpunkt-Index für \(f\) ist (indiziert) ein Programm,
das seinen eigenen Quelltext ausgibt.

Der Satz von Rice

Satz: jede nichttriviale semantische Eigenschaft von Programmen ist unentscheidbar.

dabei bedeuten:

Beispiele (semantisch oder nicht?)

Der Satz von Rice (Beweis)

wähle \(y\in E, n\in\mathbb{N}\setminus E\).

sei \(E\) entscheidbar, d.h., \(c_E\) berechenbar.

Dann ist dieses \(f\) berechenbar und total

\(f:x\mapsto\) wenn \(c_E(x)=1\), dann \(n\), sonst \(y\).

Nach Konstruktion \(x\in E \iff f(x)\notin E\).

nach Fixpunktsatz gibt es \(x\) mit \(\phi_x=\phi_{f(x)}\).

Damit \(x\in E\iff f(x)\in E\).

Plan der Vorlesung

Übersicht nach Kalenderwochen