Praktium 1, Permutation Variante 3

[fetzer]

Hi,

hat jemand einen Tipp für Variante 3? Unsere Definitionen für "all-permutations ist vollständig" und Co. schlagen leider fehl und so langsam fallen uns keine neue Lemmata mehr ein. Für einen Tipp wären wir also sehr dankbar

Grüße

[Blubberer]

same here
hatten die ersten aufgaben bis auf variante 3.3 inerhalb von 1 tag und seitdem quälen wir uns mit ihr durch
ein kleiner denkanstoss wäre sehr sehr hilfreich...

grüße

[Nathan Wasser]

Wieso wollt ihr zeigen, dass all-permutations vollständig ist?

Wenn man versucht das Lemma isort permutes (Variante 3) zu beweisen, so kommt man ohne Hilfslemma zum Goalterm:

\(hd(k) \oplus isort(tl(k)) \in all\!-\!insert\!-\!each(hd(k), all\!-\!permutations(tl(k)))\)

Ferner hat man folgende Induktionshypothese:

\(isort(tl(k)) \in all\!-\!permutations(tl(k))\)

Daraus sollte leicht ein (korrektes) Hilfslemma generalisiert werden können.

[Blubberer]

wir sind an der stelle wo wir nicht wissen wie wir all-insert-each beweisen müssen...

[dosinfo]

Hallo allerseits,
ich weiß nicht, ob es uns an der Stelle weiter bringen wird, aber "<>" ist auf jeden Fall assoziative. Taucht dann im Beweisbaum sofort auf, aber wie gesagt. Eine weitere Überlegung von mir ist, dies über die Mengen fortzusetzen, stehe im Moment allerdings auch auf dem Schlauch.

Gruß

Oleg

[charfi90]

Hallo,

wir versuchen seit mehrere Tage ohne Erfolg Lemmata dafür zu schrieben. Ich wäre für jeden Tip dankbar.

Gruss
Ahmed

[dschneid]

Wir saßen auch einige Tage an diesem letzten Lemma. Es ist vielleicht nicht zu viel verraten, wenn man folgendes sagt:

Man sieht ja zunächst, dass die verschiedenen Funktionen in einer Art Kette aufeinander aufbauen: all-permutations verwendet all-insert-each verwendet insert-each verwendet all-insert. Mit <> muss man -- zumindest habe ich das in meiner Beweisführung gemacht -- ein bisschen anders umgehen.

Man macht nach einigen aufgestellten Lemmata die Beobachtung, dass man die Funktion, über die momentan etwas bewiesen werden soll, in seinem Hilfslemma weggeneralisieren muss, damit der Beweis des Hilfslemmas nicht letztlich wieder auf genau das selbe Problem stößt wie der ursprünglich geführte Beweis.

Damit hat man eine Vorgehensweise, die sich daran orientiert, wie die verschiedenen Funktionen aufeinander aufbauen: Zum Anfang will man eine Aussage über all-permutations (nämlich das eigentlich Lemma) beweisen. all-permutations benutzt all-insert-each, was dann also im Beweisgoal auftauchen wird. Man sucht dann ein Hilfslemma, in dem all-permutations nicht mehr vorkommt, sondern nur noch all-insert-each. Diese verwendet wiederum insert-each und <>, diese beiden Funktionen werden also im Beweisbaum des Hilfslemmas auftauchen. Um auch dies zu beweisen, muss man also wiederum durch Generalisierung all-insert-each wegabstrahieren, damit diese Funktion nicht wieder beim Beweis des zweiten Hilfslemmas in die Quere kommt. So macht man dann immer weiter, bis man schließlich bei einem Lemma über all-insert, der untersten Funktion angekommen ist. Kann man das letzte Lemma beweisen, was dann irgendwann auch ohne weitere Hilfslemmas gehen müsste, dann wird damit die Beweiskette bis hinauf zum eigentlichen Lemma geschlossen.

Mir persönlich hat ein meet-in-the-middle-Ansatz geholfen, d.h. ich habe von oben heruntergearbeitet wie oben beschrieben, aber auch einmal gesehen, was man über die Funktionen ganz unten an Lemmas aufstellen kann. Das geht eventuell besser, weil die unteren Funktionen einfacher zu verstehen sind und die Lemmata dementsprechend auch etwas einfacher sind, d.h. vollständig automatisch bewiesen werden können. Wenn man die richtigen "Basislemmata" hat, kann man außerdem eventuell ein noch gesuchtes höheres Lemma einfacher aufstellen, weil man von unten kommend schon weiß, welche Eigenschaften die darin vorkommenden grundlegenderen Funktionen haben. Man kann sich auf diese Weise eine Generalisierung ersparen, die vielleicht nicht einfach zu finden ist.

Was auch hilfreich ist bei einer solchen längeren Beweiskette von aufeinander aufbauenden Lemmata: Mit der Beweisregel "Use Lemma" ein schon formuliertes, aber noch nicht bewiesenes Hilfslemma manuell anwenden. Dann weiß man zumindest, ob man prinzipiell auf der richtigen Spur ist und ob es sich lohnt, den Beweis dieses vorausgesetzten Lemmas weiter zu verfolgen.

Ich denke, damit ist niemandem die eigentliche Arbeit abgenommen, aber vielleicht wenigstens ein genereller Ansatz gegeben.

[Tapion]

Wieso wollt ihr zeigen, dass all-permutations vollständig ist?

Wenn man versucht das Lemma isort permutes (Variante 3) zu beweisen, so kommt man ohne Hilfslemma zum Goalterm:

\(hd(k) \oplus isort(tl(k)) \in all\!-\!insert\!-\!each(hd(k), all\!-\!permutations(tl(k)))\)

Ferner hat man folgende Induktionshypothese:

\(isort(tl(k)) \in all\!-\!permutations(tl(k))\)

Daraus sollte leicht ein (korrektes) Hilfslemma generalisiert werden können.

genau an dieser Stelle hängen wir aber. Weder gelingt es uns, ein Hilfslemma zu generalisieren, mit dem isort permutes (Variante 3) bewiesen wird, das ohne all-permutations() auskommt, noch gelingt es uns, isort() herauszugeneralisieren und eine Aussage über beliebige Listen zu machen, mit der isort permutes (Variante 3) bewiesen werden kann.

[Nathan Wasser]

Schauen Sie sich Kapitel 2, Folien 35 und 36 nochmal an. Beachten Sie insbesondere, dass Sie die Induktionshypothese nicht vernachlässigen dürfen.

Um Ihr Hilfslemma zu beweisen, werden Sie weitere Hilfslemmata benötigen.