Praktium 1, Permutation Variante 3

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

Praktium 1, Permutation Variante 3

Beitrag von 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
Mausschubser
Mausschubser
Beiträge: 56
Registriert: 28. Apr 2009 03:29

Re: Praktium 1, Permutation Variante 3

Beitrag von 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
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Praktium 1, Permutation Variante 3

Beitrag von 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
Mausschubser
Mausschubser
Beiträge: 56
Registriert: 28. Apr 2009 03:29

Re: Praktium 1, Permutation Variante 3

Beitrag von Blubberer »

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

Benutzeravatar
dosinfo
Windoof-User
Windoof-User
Beiträge: 40
Registriert: 23. Okt 2007 20:59

Re: Praktium 1, Permutation Variante 3

Beitrag von 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
"Wichtig ist, dass man nicht aufhört zu fragen.
- Es genügt, wenn man versucht, an jedem Tag lediglich ein wenig von diesem Geheimnis zu erfassen.
- Es ist einfacher, radioaktives Plutonium zu entsorgen als das Böse im Menschen. ...."

charfi90
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 8. Sep 2010 15:40

Re: Praktium 1, Permutation Variante 3

Beitrag von 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
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Praktium 1, Permutation Variante 3

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

Benutzeravatar
Tapion
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 220
Registriert: 14. Okt 2006 19:16
Wohnort: Darmstadt

Re: Praktium 1, Permutation Variante 3

Beitrag von Tapion »

Nathan Wasser hat geschrieben: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.
WS 2010/11 - Tutor GDI 1
SS 2010 - Tutor FGI 1+2

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

Re: Praktium 1, Permutation Variante 3

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

Antworten

Zurück zu „Archiv“