Hausübung 1.3

cwb38
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 125
Registriert: 4. Okt 2010 15:53

Hausübung 1.3

Beitrag von 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?

Benutzeravatar
hymGo
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 209
Registriert: 4. Okt 2009 23:17

Re: Hausübung 1.3

Beitrag von 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 :wink:

Benutzeravatar
Domac
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 160
Registriert: 4. Okt 2010 16:11

Re: Hausübung 1.3

Beitrag von Domac »

Rischtiiiisch! :)
Die Aufgabe ist jedoch so auch recht einfach. VeriFun bringt keinen ersichtlichen Vorteil beim lösen dieser Aufgabe.
Gruß domac
Extend my dropbox space (here).
Thanks!

cwb38
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 125
Registriert: 4. Okt 2010 15:53

Re: Hausübung 1.3

Beitrag von 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
Windoof-User
Windoof-User
Beiträge: 38
Registriert: 10. Apr 2010 22:22

Re: Hausübung 1.3

Beitrag von 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
Mausschubser
Mausschubser
Beiträge: 65
Registriert: 9. Dez 2009 15:05

Re: Hausübung 1.3

Beitrag von erna »

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

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

Re: Hausübung 1.3

Beitrag von Christoph Walther »

cwb38 hat geschrieben: ... 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).

Antworten

Zurück zu „Archiv“