Hausübung 1.3

[cwb38]

Hallo,

ich wollte meine Lösung für diese Aufgabe mit VeriFun testen, allerdings bleibt die Funktion "mix" nach dem Kopieren in ein neues Projekt und dem Einfügen der üblichen Listendefinition grau, d.h. sie wird ignoriert. Bisher sind mir graue Funktionen nur dann begegnet, wenn sie nicht terminieren, allerdings kann ich keinen Fall erkennen, bei dem das passieren könnte. Woran könnte es bei dieser Funktion liegen?

[hymGo]

VeriFun erkennt die Terminierung hier nicht automatisch. In so einem Fall muss man Terminierungshypothesen aufstellen um diese zu beweisen.
Diesen Teil der Hausübung ist somit durch überlegen einfacher zu lösen, als mit Hilfe von VeriFun

[Domac]

Rischtiiiisch!
Die Aufgabe ist jedoch so auch recht einfach. VeriFun bringt keinen ersichtlichen Vorteil beim lösen dieser Aufgabe.
Gruß domac

[cwb38]

Danke für die Antworten^^ Wie schon erwähnt habe ich die Aufgabe per Hand gelöst und wollte lediglich schnell überprüfen...

[Kai.S]

Mich würden die Terminierungshypothesen interessieren... Dazu vielleicht nähere Informationen oder gar eine Lösung für diesen Fall als Beispiel (nach Ende der Abgabe für die Hausübung falls es daran hängt)?

[erna]

length(k + l) > length(tl(k) + tl(l)) ?

[Christoph Walther]

... allerdings bleibt die Funktion "mix" nach dem Kopieren in ein neues Projekt und dem Einfügen der üblichen Listendefinition grau, d.h. sie wird ignoriert. Bisher sind mir graue Funktionen nur dann begegnet, wenn sie nicht terminieren, allerdings kann ich keinen Fall erkennen, bei dem das passieren könnte. Woran könnte es bei dieser Funktion liegen?

Prozeduren bleiben "grau", wenn das systen nicht die terminierung der prozedur beweisen kann. Natürlich bei nicht-terminierenden prozeduren, aber auch bei terminierenden wie in diesem fall. Wie alle(!) korrekten terminierungsbeweisverfahren ist auch das in VeriFun implementierte verfahren unvollständig, muß also bei (unendlich vielen) terminierenden prozeduren versagen. In solchen fällen muß der benutzer eine sogenannte terminierungsfunktion für die prozedur definieren. Bei mix verwendet man length(k) + length(l), denn die summe der listenlängen im rekursiven aufruf ist echt kleiner als die summe der eingabelisten. Damit der beweis klappt, muß zuvor die kommutativität von "+" gezeigt worden sein.

Terminierungsbeweise behandeln wir in kapitel 8. Wer bis dahin nicht warten will kann sich die folien aus dem vorjahr dazu anschauen => http://www.inferenzsysteme.informatik.t ... -10-22.pdf (die sich nur unwesentlich von den folien für dieses semester unterscheiden).