BuK-Kreativaufgabe04 G2

Aus ProgrammingWiki
Archivierte Version vom 2011-04-18T18:16:01+00:00. Aktuelle Version

Zeitbeschränkte Prozesse mit Engines

Folgender Satz soll auf dieser Seite mittels Scheme-Engines dargestellt werden:

Wenn ein Menge M semi-entscheidbar ist, dann ist sie aufzählbar.

Die Aufzählbarkeit einer Menge M wird hier nicht dargestellt.

Aus den ersten Teil des Satzes M ist semi-entscheidbar kann man folgenden Schluss ziehen:

Es existiert eine Funktion \chi_M '(w)=\begin{cases} true, \text{wenn }w \in M \\ n.d., sonst \end{cases} .

Die Funktion, die für den Beweis erstellt werden muss ist folgend definiert:

f(i)=\begin{cases} g(i),\text{wenn } \chi_M '(g(i))\\ a \in M, \text{sonst} \end{cases}

Wobei g: \mathbb{N}_0 \rightarrow A^*. Für das Beispiel wird die Menge mit M=\{a, b, c\} definiert.

Diese Funktion ist partiell berechenbar, d.h. es gibt Eingabeparameter für die \chi_M ' stoppt, und welche für die die Funktion nicht stoppt. Genau diese Wörter, welche nicht in der Menge M enthalten sind, stellen ein Problem dar, da \chi_M ' nicht terminiert und ewig läuft.

Die Idee zur Lösung besteht darin, dass man der Prozedur eine gewisse Taktrate vorgibt, wie lange der Berechnungsprozess dauern darf, oder besser gesagt, für jeden Eingabeparameter wird die Funktion nur ein Takt bearbeitet und erst dann für jeden Parameter einen weiteren Takt. Somit werden Wörter w \in M innerhalb von "kurzer Zeit" (hier: innerhalb weniger Sekunden) berechnet.

Hier die Prozedur von \chi_M ' in Scheme:

Die Funktion kann als Engine kann wiefolgt implementiert werden:

Die Engine in Scheme benötigt folgende Aufrufparameter:

- Anzahl der Takte (die für Berechnung zur Verfügung gestellt werden)

- Eine Erfolgs-Prozedur

- Eine Misserfolgs-Prozedur

Die Erfolgsprozedur liefert die Restzeit (Anzahl der Takte welche nicht zur Berechnung nötig gewesen sind) und das Ergebnis der Berechnung.

Bei einem Misserfolg wird die (vollständige) Engine gespeichert. Diese kann dazu verwendet werden um später die Berechnung forzusetzen, d.h. weitere Takte werden zur Verfügung gestellt.