BuK-Kreativaufgabe04 G2
Aus ProgrammingWiki
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
.
Die Funktion, die für den Beweis erstellt werden muss ist folgend definiert:
Wobei .
Für das Beispiel wird die Menge mit
definiert.
Diese Funktion ist partiell berechenbar, d.h. es gibt Eingabeparameter für die 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
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 innerhalb von "kurzer Zeit" (hier: innerhalb weniger Sekunden) berechnet.
Hier die Prozedur von in Scheme:
Die Funktion kann als Engine implementiert werden:
Die Engine in Scheme benötigt folgende Aufrufparameter:
(1) Anzahl der Takte (die für Berechnung zur Verfügung gestellt werden)
(2) Eine Erfolgs-Prozedur In demFall wird die Zeit und das Ergebnis als Liste ausgegeben.
(3) Eine Misserfolgs-Prozedur Wenn die vorgegebene Zeit überschritten ist, wird expired ausgegeben.
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.
Nun folgt der Aufruf mit dem Wort "ab":
Durch die Engine können wir die Prozedur auch mit Wörtern die nicht Element der Menge sind aufrufen und diese stoppt nach endlicher Zeit.
Bisher liefert die Misserfolgs-Prozedur eine Meldung. Durch eine andere Definition erreichen wir, dass bei einem erneuten Aufruf die Bwerechnung forgesetzt wird:
Um das zu verdeutlichen, werden wir nun den Aufruf der Engine mit dem Wort "aabbc" starten. Durch mehrmaliges Ausführen wird die Berechnung bis zum Ergebnis weitergeführt, aber nur falls in endlicher Vorgabe, vorhanden.
