Seite 1 von 1

Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 10:30
von oren78
Hallo miteinander,

ich versuche gerade in verifun das aufsteigende sortieren einer liste mit hilfe von zwei hilfsfunktionen zu realisieren...
Eine der hilfsfunktionen wird in verifun zur hälfte grün zur anderen hälfte lila angezeigt, dieses merkwürdige icon,
welches in der legende bei verifun übrigens nicht aufgelistet ist, ist mir schon im vierten praktikum aufgefallen,
jedoch hab ich das ignoriert, weil dort auch ein entsprechender hinweis war...

nun gut jedenfalls, seien folgende prozeduren gegeben:

Code: Alles auswählen

function minimum(k : list[ℕ]) : ℕ <=
if ?ø(k)
  then ⋆
  else if ?ø(tl(k))
         then hd(k)
         else if hd(k) ≤ hd(tl(k))
                then minimum(hd(k) :: tl(tl(k)))
                else minimum(tl(k))
              end_if
       end_if
end_if

function remove(n : ℕ, k : list[ℕ]) : list[ℕ] <=
if ?ø(k)
  then k
  else if hd(k) = n
         then tl(k)
         else hd(k) :: remove(n, tl(k))
       end_if
end_if

function minsort(k : list[ℕ]) : list[ℕ] <=
if ?ø(k)
  then k
  else minimum(k) :: minsort(remove(minimum(k), k))
end_if
remove(...) ist die besagte prozedur, welche halb lila halb grün angezeigt wird, minimum(...) ist widerum grün angezeigt und minsort(...) dagegen lila !

Mir leuchtet es gerade nicht ein, wo der fehler liegt das minsort(...) die liste nicht sortieren kann, ich habe die anderen beiden prozeduren getestet und
sie erfüllen offensichtlich ihren zweck, daraus müsste eigentlich folgen das die prozedur minsort(...) ebenfalls ihr zweck erfüllen sollte, zumal sie gerade
die schritte rekursiv ausführt, welche korrekterweise einzeln getestet funktionieren:

Code: Alles auswählen

➩ minimum(9 :: 3 :: 0 :: ø)
➩ 0 (GMN=62)
sowie:

Code: Alles auswählen

➩ remove(minimum(9 :: 3 :: 0 :: ø), 9 :: 3 :: 0 :: ø)
➩ 9 :: 3 :: ø (GMN=88)
was jemand also, wo genau das problem liegt...??

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 10:42
von mister_tt
Was ist denn jetzt eigentlich das Problem? Die Terminierung von minsort zu beweisen? Oder hast du das schon gemacht, testest gerade die minsort Prozedur und die funzt nicht?

Die Prozeduren sehen soweit richtig aus...

EDIT: Bei mir funzt es dann auch ohne Probleme, wenn man die Terminierung bewiesen hat...

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 11:00
von brotkasten
Bekommst Du die Terminierung von minsort nicht bewiesen?
Ich denke du musst VeriFun beibringen, dass minimum(k) in k selbst liegt, und
damit gilt, dass k>remove(minimum(k),k)

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 11:08
von mister_tt
brotkasten hat geschrieben:Bekommst Du die Terminierung von minsort nicht bewiesen?
Ich denke du musst VeriFun beibringen, dass minimum(k) in k selbst liegt, und
damit gilt, dass k>remove(minimum(k),k)
Du meinst \(length(k) > length(remove(minimum(k),k))\). Das ist schon richtig, length-Prozedur auf Listen definieren, \(length(k)\) als Maßterm für minsort angeben, an der Beweiswurzel generalisieren und fertig...

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 11:53
von oren78
done !

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 12:03
von mister_tt
oren78 hat geschrieben:
mister_tt hat geschrieben:Was ist denn jetzt eigentlich das Problem? Die Terminierung von minsort zu beweisen? Oder hast du das schon gemacht, testest gerade die minsort Prozedur und die funzt nicht?
genau darum gings das ding funzt nicht ;-) Naja, ich dachte eigentlich verifun beweist dies automatisch, zumal die anderen prozeduren ja korrekt terminieren, aber offensichlich liegt es wohl am remove(...) der eben den zustand halb lila halb grün hat - vermute daher das verifun deswegen die prozedur nicht automatisch beweisen kann, oder?
Öhm... oO ich raffs immer noch nicht... :D Also: Die Terminierung von minsort kannst du trotz halb lila halb grünem Icon wie oben beschrieben beweisen. Und dann funzt bei mir die Funktion auch wie gewünscht...

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 12:04
von oren78
mister_tt hat geschrieben:
brotkasten hat geschrieben:Bekommst Du die Terminierung von minsort nicht bewiesen?
Ich denke du musst VeriFun beibringen, dass minimum(k) in k selbst liegt, und
damit gilt, dass k>remove(minimum(k),k)
Du meinst \(length(k) > length(remove(minimum(k),k))\). Das ist schon richtig, length-Prozedur auf Listen definieren, \(length(k)\) als Maßterm für minsort angeben, an der Beweiswurzel generalisieren und fertig...
ok damit gehts ;-) Aber dennoch wüsste ich gerne WARUM genau ist remove(...) halb grün halb lila...? wieso kann verifun die prozedur nicht "ganz" grün labeln...??

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 12:12
von mister_tt
Da bin ich dann auch mal gespannt auf die Aussage eines Assistenten ;)

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 12:36
von Simon Siegler
Die Prozedur remove erhält ein blau/grünes Symbol, da das zugehörige Projektionslemma noch nicht bewiesen ist. Dieses Lemma lässt sich mit einer einfachen Induktion beweisen, diese wird jedoch nicht automatisch gestartet.

Der Terminierungsbeweis von minsort gelingt auch mit der von VeriFun vorgeschlagenen Terminierungshypothese, jedoch ist dazu ebenfalls Induktion erforderlich, die VeriFun in Terminierungsbeweisen nicht automatisch anwendet. Sie können jedoch im "Termination Analysis" Fenster auf "Proof" clicken und "Verify" aus der Toolbar oder dem Menü "Program" anwenden, um den Beweis von VeriFun führen zu lassen.

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 12:42
von mister_tt
Danke für die Antwort.
Simon Siegler hat geschrieben:Die Prozedur remove erhält ein blau/grünes Symbol, da das zugehörige Projektionslemma noch nicht bewiesen ist.
Das habe ich mir schon gedacht. Aber warum wird das überhaupt angelegt?

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 13:55
von brotkasten
jupp, Danke! Ich war da etwas ungenau, ich meinte eigentlich length(k).

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 16:45
von Nathan Wasser
mister_tt hat geschrieben:Danke für die Antwort.
Simon Siegler hat geschrieben:Die Prozedur remove erhält ein blau/grünes Symbol, da das zugehörige Projektionslemma noch nicht bewiesen ist.
Das habe ich mir schon gedacht. Aber warum wird das überhaupt angelegt?
Ein Projektionslemma ist kurz gesagt eine nette Sache. Es sagt aus - wenn es bewiesen ist - dass unter bestimmten Umständen ein komplizierter Term (hier \(remove(n, k)\)) zu einem simpleren Term (hier \(k\)) vereinfacht werden kann.

Re: Frage zu einigen L-Prozeduren...

Verfasst: 23. Mär 2010 18:17
von oren78
dann wäre das auch geklärt ;-)

Vielen Dank...