5. Übung

a_naseri
Neuling
Neuling
Beiträge: 9
Registriert: 10. Feb 2008 12:10

5. Übung

Beitrag von a_naseri » 23. Mär 2009 16:45

Hi,

bei der Aufgabe 5.4 Teil b als Maßterme wurden length(k) und hd(k) angegeben!
aber wie kann es überhaupt vorkommen, dass: length(k) = length(tl(k)) und was ist denn mit der Aussage if{length(k) = length(tl(k)), hd(k) > hd(tl(k)), false} gemeint?


vielen Dank

Christoph B
Computerversteher
Computerversteher
Beiträge: 370
Registriert: 15. Okt 2006 18:28
Wohnort: Wiesbaden
Kontaktdaten:

Re: 5. Übung

Beitrag von Christoph B » 23. Mär 2009 17:29

prinzipiell gilt ja: dein Ausgewählter Maßtherm muss mit JEDEM rekursiven Aufruf kleiner werden.
Da reicht length(k) nicht aus, da es ja auch einen rekursiven Aufruf mit k / pred((hd(k))::tl(k)) geben kann (da gilt halt nicht length(k) > length( pred((hd(k))::tl(k)))
Da die Länge aber zumindest gleich bleibt (das ist das minimum dessen, was ein forderer Maßtherm in einer Maßthermliste erfüllen muss!) und in dem Fall hd(k) abnimmt, wird hd(k) als weiterer Maßtherm benötigt.
D.h. zusammengesetzt einfach: mit jedem Rekursiven Aufruf wird entweder die Liste k kleiner, oder die Länge bleibt gleich, aber hd(k) wird kleiner.

Daher ist auch die Reihenfolge der Maßtherme in einer Maßthermliste entscheidend:

wenn die Maßthermliste z.B. hd(k),length(k) wäre, würd das in die Hose gehen, da hd(k) kleiner als hd(tl(k)) sein kann (und wie willst du Terminierung beweisen, wenn dein Maßtherm GRÖßER wird?).

und auch wenn der 2. Maßtherm unter bestimmten Bedingungen nicht benötigt wird, muss er in alle Terminierungshypothesen, daher "if{length(k) = length(tl(k)), hd(k) > hd(tl(k)), false}"

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

Re: 5. Übung

Beitrag von Simon Siegler » 23. Mär 2009 18:00

Das kann tatsächlich nicht vorkommen. Für den ersten rekursiven Aufruf wird also nur die Länge betrachtet. Für den zweiten Aufruf muss aber das erste Element der Liste betrachtet werden. Diese beiden Ordnungsrelationen werden hier lexikographisch kombiniert. Das bedeutet, wir sortieren erst nach der Länge der Liste, und falls diese gleich bleibt nach dem ersten Listenelement.

Die Terminierungshypothesen werden aber schematisch generiert, ohne das Wissen, an welcher Stelle nur der erste Teil der Relation betrachtet werden muss. Also wird auch für den ersten rekursiven Aufruf überprüft, ob die Länge der Liste gleich bleibt, da dann das erste Element verglichen werden müsste.

Antworten

Zurück zu „Archiv“