Methode treeordered ?

erna
Mausschubser
Mausschubser
Beiträge: 65
Registriert: 9. Dez 2009 15:05

Methode treeordered ?

Beitrag von erna »

Guten Abend :),

die Definition von treeordered: alle Zahlen im linken Teilbaum sind kleiner oder gleich, alle im rechten Teilbaum größer oder gleich dem Datum des inneren Knoten.

Demnach wäre der Baum also geordnet:
node(node(node(tip, 0, tip), 1, node(tip, 5, tip)), 2, node(tip, 3, tip))

Jedoch:

➩ treeordered(
node(node(node(tip, 0, tip), 1, node(tip, 5, tip)), 2, node(tip, 3, tip)))
➲ true (GMN=71)

➩ ordered(
flatten(
node(node(node(tip, 0, tip), 1, node(tip, 5, tip)), 2, node(tip, 3, tip))))
➲ false (GMN=117)

Müssen wir das berücksichtigen?
Die Implikation treeordered(t) => ordered(flatten(t)) kann eigentlich mit der Definition von treeordered nicht bewiesen werden!?

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Methode treeordered ?

Beitrag von dschneid »

Deine Prozedur treeordered stimmt nicht, bzw. du hast die Anforderung nicht ganz richtig verstanden: 5 ist im linken Teilbaum des obersten Knoten, aber 5 > 2, also ist dieser Baum nicht sortiert. Es geht nicht nur um die unmittelbaren Unterknoten.

erna
Mausschubser
Mausschubser
Beiträge: 65
Registriert: 9. Dez 2009 15:05

Re: Methode treeordered ?

Beitrag von erna »

aaah wer richtig liest der ist glatt ... oder so ähnlich :) ... da steht ja Teilbaum ups mein Fehler

kruse
Mausschubser
Mausschubser
Beiträge: 49
Registriert: 15. Okt 2009 15:10
Kontaktdaten:

Re: Methode treeordered ?

Beitrag von kruse »

Hi,

ich hab das gleiche Problem gehabt wie erna. Ich hab aber leider auch keine Idee wie ich prüfen soll, dass alle Elemente des linken Baums (rechts analog) kleiner gleich dem jetztigen data(t) sind, wenn ich nur die Eingabe t : tree[nat] hab.Kann mir vielleicht irgendjemand einen Tip geben der mich in die richtige Richtung wirft.

Gruse

Karsten

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

Re: Methode treeordered ?

Beitrag von Nathan Wasser »

Wie schafft es Insertionsort jedes Element in die sortierte Liste einzufügen, wenn es nur die Eingabe \(k : list[nat]\) hat?

kruse
Mausschubser
Mausschubser
Beiträge: 49
Registriert: 15. Okt 2009 15:10
Kontaktdaten:

Re: Methode treeordered ?

Beitrag von kruse »

omg,
manchmal ist die lösung echt zu naheliegent. Danke

The One and Only Markus
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 169
Registriert: 10. Nov 2005 19:28
Wohnort: Darmstadt

Re: Methode treeordered ?

Beitrag von The One and Only Markus »

Unterscheidet ihr auch bei treeordered zwischen den 3 Fällen

- linker Teilbaum leer + rechter Teilbaum leer
- nur links leer
- nur rechts leer?

Dadurch wird die Methode recht kompliziert und damit Sachen beweisen nicht gerade leichter :D

spyro.makedonski
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 102
Registriert: 18. Apr 2010 13:45

Re: Methode treeordered ?

Beitrag von spyro.makedonski »

wir haben diese Methode mit zwei Hilfsmethoden implementiert und sie funktionieren korrekt ("treesort(k) is ordered tree" haben wir ohne probleme bewiesen). Aber die Problemen kommen wenn wir "flattening keeps ordered" zu beweisen versuchen... also das Goal sieht nicht so kompliziert aus aber wir haben alles mögliche versucht (wir haben 20+ bewiesene Lemmata, die irgendwie nutzbar sein konnte), und trotzdem geht den Beweis nicht :(... vielleicht wenn wir 2 Hilfsmethode benutzen, macht das das ganzen Ding zu kompliziert... ist es möglich dass wir treeordered so implementieren, dass sie nicht so kmpliziert ohne hilfsmethoden wird?

The One and Only Markus
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 169
Registriert: 10. Nov 2005 19:28
Wohnort: Darmstadt

Re: Methode treeordered ?

Beitrag von The One and Only Markus »

Also wie gesagt, wir habens ohne Hilfsmethoden. Dafür halt mit einer Fallunterscheidung mit den 3 genannten Fällen. Dadurch wird der goalterm schon beim ersten Schritt recht fies :D

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

Re: Methode treeordered ?

Beitrag von Nathan Wasser »

- Eine Implementierung von \(treeordered\) ohne Hilfsprozeduren wird sehr wahrscheinlich inkorrekt sein.

- Der Beweis von "treesort(k) is ordered tree" bedeutet nicht zwangsläufig, dass \(treeordered\) korrekt implementiert wurde. Sonst würde function treeordered\((t : tree[nat]) : bool <=\) true ausreichen.

tobizZL
Windoof-User
Windoof-User
Beiträge: 34
Registriert: 19. Okt 2009 14:48

Re: Methode treeordered ?

Beitrag von tobizZL »

Kann man treeordered so ungünstig implementieren, dass man schwerwiegende Probleme beim Beweisen der Lemmas bekommen kann?

Also ich habe treeordered mit 2 Hilfsfunktionen implementiert und umfangreich getestet.. sie(treeordered) erfüllt definitiv die Anforderungen..
treesort is a ordered tree war auch relativ leicht zu beweisen.. aber flatten keeps ordered will einfach nicht grün werden ^^ der Goal-Term ist sogar recht einfach.. das Problem ist aber, dass meine Hilfsprozeduren darin auftauchen und ich zwischen diesen und flatten keine beweisbaren Hilfslemmas formuliert bekomme..

Ich wäre über jeden Tip dankbar.

jack_90
Mausschubser
Mausschubser
Beiträge: 75
Registriert: 29. Sep 2009 22:38
Wohnort: Darmstadt
Kontaktdaten:

Re: Methode treeordered ?

Beitrag von jack_90 »

@tobizzl:
Das Problem ist, dass vermutlich deine Hilfprozeduren auf einem Baum arbeiten und flatten eine Liste zurückgibt.
Wir haben es gelöst, indem wir analog zu den Hilfsprozeduren von treeordered noch 2 weitere geschriebenen haben,
welche praktisch die gleiche Funktionalität besitzen, aber auf einer Liste arbeiten.
Hiermit lässt sich dann ein Zusammenhang zw Baum und Liste herstellen.
EiSE Tutor WS 12/13

tobizZL
Windoof-User
Windoof-User
Beiträge: 34
Registriert: 19. Okt 2009 14:48

Re: Methode treeordered ?

Beitrag von tobizZL »

ah danke für die Rückmeldung!
ich habs zwischenzeitlich zum Glück auch gelöst.. hab jetz ingesamt 3 Hilfsprozeduren verwendet.. trotzdem mit ähnlicher Idee.. die 3. HP berechnet bei mir jetzt auch etwas von Listen..

insgesamt fand ich das Praktikum bis jetzt aber mit Abstand am Aufwendigsten.. ich kann mir eigentlich nicht vorstellen, dass es nur so "kompliziert" geht..

Bin mal gespannt, obs evtl wieder eine kleine Präsentation einer möglichen Musterlösung geben wird..

Viel Erfolg noch an alle,

Gruß Tobi..

Antworten

Zurück zu „Archiv“