Massterme & TH.

oneway
Windoof-User
Windoof-User
Beiträge: 24
Registriert: 4. Feb 2008 23:00

Massterme & TH.

Beitrag von oneway »

Hallo,

Kann mir jemand sagen welche Massterm(e) und wie viele Terminierungshypothesen hat die Funktion von Hausuebung 3.4 a.

Danke

Simon Siegler
Computerversteher
Computerversteher
Beiträge: 369
Registriert: 16. Apr 2007 09:12

Re: Massterme & TH.

Beitrag von Simon Siegler »

Wie in Kapitel 8 auf Folie 10 beschrieben, wird für jede atomare rekursive Relationenbeschreibung pro Substitution eine Terminierungshypothese erzeugt. Nach Folie 12 aus Kapitel 7 wird für jeden Ergebnis- oder Bedingungsterm, der n rekursive Aufrufe erhält, eine atomare rekursive Relationenbeschreibung mit n Substitutionen erzeugt. Folglich wird für jeden rekursiven Aufruf eine Terminierungshypothese erzeugt.

Zu den Maßtermen sollten Sie sich überlegen, welche Argumente der rekursiven Aufrufe im Vergleich zu denen des Funktionsaufrufs kleiner werden.

Turing-Test
Mausschubser
Mausschubser
Beiträge: 91
Registriert: 17. Okt 2008 02:06

Re: Massterme & TH.

Beitrag von Turing-Test »

Simon Siegler hat geschrieben:Zu den Maßtermen sollten Sie sich überlegen, welche Argumente der rekursiven Aufrufe im Vergleich zu denen des Funktionsaufrufs kleiner werden.
Mir fehlt da noch mind. ein Schritt zum fertigen Maßterm. Wenn ich z.B. die Präsenzübung 5.2 (minus) betrachte, dann wird dort doch das y für jeden rekursiven Aufruf kleiner. Als Maßterm wird im Lösungsvorschlag aber x - y gewählt. Für meine Begriffe muss das y kleiner als das x werden, damit die Funktion in den Basisfall läuft und terminiert. Wie ist der Verfasser aber jetzt auf x - y gekommen?
File deletion is murder!

Simon Siegler
Computerversteher
Computerversteher
Beiträge: 369
Registriert: 16. Apr 2007 09:12

Re: Massterme & TH.

Beitrag von Simon Siegler »

Im rekursiven Aufruf wird x durch x und y durch succ(y) ersetzt, also wird y sogar immer größer.
Der Maßterm m muß hier so gewählt werden, dass m > m[x/x, y/succ(y)] gilt. Dies ist für den Maßterm y nicht der Fall, denn y > succ(y) gilt sicher nicht.

Wenn Sie sich Folie 15 aus Kapitel 8 ansehen, wird dort in der Terminierungshypothese immer der Maßterm mit dem Term verglichen, welcher entsteht, wenn man im Maßterm die formalen Parameter der Prozedur durch die aktualen Parameter des rekursiven Aufrufs ersetzt. Der Maßterm definiert also eine Maßfunktion, mit deren Hilfe die Argumente des rekursiven Aufrufs mit denen des ursprünglichen Aufrufs verglichen werden. Zum Terminierungsbeweis ist also eine Funktion zu finden, die für die Argumente der rekursiven Aufrufe kleinere Werte liefert als für die ursprünglichen Argumente.

Turing-Test
Mausschubser
Mausschubser
Beiträge: 91
Registriert: 17. Okt 2008 02:06

Re: Massterme & TH.

Beitrag von Turing-Test »

Ähm ja, kleiner ist nicht das gleiche wie größer. :D
Vielen Dank. Das klingt erstmal einleuchtend. Ich muss das nochmal durchgehen.
File deletion is murder!

Antworten

Zurück zu „Archiv“