Auswertung von Termen

The One and Only Markus
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 169
Registriert: 10. Nov 2005 19:28
Wohnort: Darmstadt

Auswertung von Termen

Beitrag von The One and Only Markus »

Hi,

bei mir kommt immer wenn ich über symbolische Auswertung nachdenke folgende Frage auf:

Angenommen ich habe eine Funktion f(x): nat -> nat. Diese Funktion terminiert nicht für alle x aus nat. Jetzt schreibe ich in meinem Programm einen Ausdruck wie if (f(x) = f(x)) then true else false. Jetzt wird mir ja Verifun sagen dass ich die Prozedur, die diesen Ausdruck enthält, nicht ausführen kann, weil f(x) nicht immer terminiert. Wieso ist das so? Ich interessiere mich ja eigentlich garnicht für den Wert von f(x) sondern nur dafür ob die beiden Terme gleich sind. Und da f(x) und f(x) ja schon syntaktisch gleich sind müssen sie doch auch semantisch gleich sein. Wieso wird das nicht sofort durch true ersetzt? Warum wird also f(x) überhaupt ausgewertet obwohl das Ergenis unwichtig ist? Das Beispiel ist natürlich jetzt etwas konstruiert, aber ich denke schon das solche trivialen Terme während der Auswertung eines Programms entstehen können.

Gruß
Markus

aderhold
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 212
Registriert: 21. Okt 2005 10:50

Re: Auswertung von Termen

Beitrag von aderhold »

Zuerst eine allgemeine Antwort: VeriFun ist für den Nachweis der totalen Korrektheit von Programmen konzipiert. Das umfasst Terminierung sowie partielle Korrektheit. Partielle Korrektheit heißt: Wenn das Programm terminiert, erfüllt es die gewünschte Eigenschaft. Wenn der Kunde eine Spezifikation vorgibt und ein Programm bestellt, das partiell korrekt sein soll, dann kann der Produzent also einfach ein niemals terminierendes Programm liefern und hat damit dem offiziellen Kundenwunsch entsprochen. Klingt unbefriedigend. Also lieber: Totale Korrektheit fordern.

Nun die spezielle Antwort: Es ist richtig, dass man in "f(x) = f(x)" die f-Aufrufe nicht auszuwerten braucht, sondern sofort den Term durch "true" ersetzen kann. VeriFun macht dies auch (Beispiel: "isort(k) = isort(k)" beweisen lassen). Dass im Falle einer nicht als terminierend nachgewiesenen Prozedur f erst gar nicht mit der Auswertung begonnen wird, hat mindestens zwei Gründe:
  1. Wenn man das Ersetzen der f-Aufrufe durch den instantiierten Rumpf erlaubt, führt das schnell zur Nicht-Terminierung der symbolischen Auswertung. Das hilft einem dann auch nicht viel. Wenn man das Ersetzen der f-Aufrufe durch den instantiierten Rumpf grundsätzlich verbietet, dann hängt die zu zeigende Aussage wohl gar nicht von dem ab, was f berechnet. Dann kann man die zu zeigende Aussage auch gleich generalisieren, indem man das "f(x)" weggeneralisiert.
  2. Die Weigerung von VeriFun, eine symbolische Auswertung ohne vorherigen Terminierungsnachweis zu beginnen, vermeidet, dass der Benutzer eine riesige partiell korrekte Theorie aufstellt, die aber nur deswegen partiell korrekt ist, weil nichts terminiert. Beispiel: Ausgehend von der für kein x terminierenden Funktion f schreibe ich eine Prozedur g:

    Code: Alles auswählen

    function g(x : nat) : nat <=
    if f(x) = f(x)
      then 0
      else 1
    end_if
    Offensichtlich terminiert g nicht. Trotzdem könnte ich "g(x) = 0" für alle x beweisen. Wenn man sich statt "f" und "g" nun deutlich komplexere Prozeduren vorstellt, dann wird auch der Nachweis der partiellen Korrektheit aufwendiger. Irgendwann feststellen zu müssen, dass alles "für die Katz war", wäre enttäuschend.
Zuletzt geändert von aderhold am 29. Jan 2009 12:26, insgesamt 1-mal geändert.
Grund: Missverständliche Formulierung korrigiert.

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Re: Auswertung von Termen

Beitrag von Christoph Walther »

Es gibt noch einen weiteren grund: Die symbolische auswertung muß ja die "richtige" auswertung durch den interpreter "eval_P" reflektieren. Formal heißt das: Wenn t symbolisch zu r ausgewertet wird, so werden jede konstruktorgrundinstanz t' und die entsprechende konstruktorgrundinstanz r' von r durch "eval_P" zu identischen konstruktorgrundtermen ausgewertet (bei stucktermen in t ' gilt das nicht, aber das ist hier egal).

Beispiel: 'plus(x, succ(y))=0' wird symbolisch zu 'false' ausgewertet. Damit weiß man, daß "eval_P" 'plus(N, succ(M))' für beliebige natürliche zahlen N und M (repräsentiert durch konstruktorgrundterme) zu 'false' ausrechnet.

Jetzt zu 'if{f(x)=f(x), true false}: Hier terminiert die berechnung durch "eval_P" nicht, denn um 'if{f(N)=f(N), true false} für eine beliebige natürliche zahl N auszurechnen, muß zunächst f(N) bestimmt werden. Da 'f' nicht terminiert, gerät "eval_P" in eine endlosschleife. Es müßte aber 'true' herauskommen, wenn die symbolisch auswertung 'f(x)=f(x)' durch 'true' ersetzt.

Antworten

Zurück zu „Archiv“