Frage zu einigen L-Prozeduren...

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Frage zu einigen L-Prozeduren...

Beitrag 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...??
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Frage zu einigen L-Prozeduren...

Beitrag 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...

brotkasten
Windoof-User
Windoof-User
Beiträge: 39
Registriert: 17. Jan 2005 08:20

Re: Frage zu einigen L-Prozeduren...

Beitrag 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)

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Frage zu einigen L-Prozeduren...

Beitrag 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...

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: Frage zu einigen L-Prozeduren...

Beitrag von oren78 »

done !
Zuletzt geändert von oren78 am 23. Mär 2010 12:05, insgesamt 1-mal geändert.
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Frage zu einigen L-Prozeduren...

Beitrag 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...

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: Frage zu einigen L-Prozeduren...

Beitrag 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...??
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Frage zu einigen L-Prozeduren...

Beitrag von mister_tt »

Da bin ich dann auch mal gespannt auf die Aussage eines Assistenten ;)

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

Re: Frage zu einigen L-Prozeduren...

Beitrag 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.

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Frage zu einigen L-Prozeduren...

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

brotkasten
Windoof-User
Windoof-User
Beiträge: 39
Registriert: 17. Jan 2005 08:20

Re: Frage zu einigen L-Prozeduren...

Beitrag von brotkasten »

jupp, Danke! Ich war da etwas ungenau, ich meinte eigentlich length(k).

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Frage zu einigen L-Prozeduren...

Beitrag 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.

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: Frage zu einigen L-Prozeduren...

Beitrag von oren78 »

dann wäre das auch geklärt ;-)

Vielen Dank...
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

Antworten

Zurück zu „Archiv“