Tipps für "MATCH is sound"?

JanK
Erstie
Erstie
Beiträge: 20
Registriert: 11. Apr 2008 20:30

Tipps für "MATCH is sound"?

Beitrag von JanK »

Bei dem Beweis des Lemmas "Match is sound" kommen wir bei den letzten beiden Induktionsschritten nicht weiter. Wir haben noch kein anwendbares Lemma für diesen Beweis gefunden.
Hat jemand Tipps dafür?

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

Re: Tipps für "MATCH is sound"?

Beitrag von fetzer »

Sitzen beim selben Problem und finden leider keinerlei Ansatzpunkte. Würde mich ebenfalls über Tipps oder Anfangspunkte freuen.

pigbird
Windoof-User
Windoof-User
Beiträge: 26
Registriert: 28. Apr 2008 23:34

Re: Tipps für "MATCH is sound"?

Beitrag von pigbird »

zu dem oberen der letzten Schritte habe ich ein Lemma über :: - Operator, eine Substitution σ angewandt auf eine Liste (nämlich tl(k)) gebraucht. Zu beachten ist die Induktionshypothese. Ich weiss nicht wie es bei euch ist, aber das Hilfslemma soll sich selbst beweisen, wenn Ihr die anderen Lemmas von anderen Aufgaben habt.
zu dem anderen, habe ich das Hilfslemma MATCH(k, l) ≠ ↯ → | k | = | l | mit "Use Lemma" benutzt. Weitere Lemmas über die Länge sind bei mir nötig. Ich hoffe, es kann euch weiter helfen.

_Peter_
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 170
Registriert: 1. Okt 2007 19:56

Re: Tipps für "MATCH is sound"?

Beitrag von _Peter_ »

habt ihr eine grobe Vorgehensweise für die 3.5? Brauch grad nen Denkanstoss.
Habe das Hilfslemma noch nicht beweisen können. :|

_Peter_
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 170
Registriert: 1. Okt 2007 19:56

Re: Tipps für "MATCH is sound"?

Beitrag von _Peter_ »

Ich hab ja ein Lemma, was wunderbar zum Beweis von MATCH(k, l) ≠ ↯ → | k | = | l | passen müsste, aber leider trotzdem nicht funktioniert.

Edit: das Lemma war zu lang und zu übertrieben. Ein kleines lemma über | zweier Listen und schwupp wars bewiesen :-)
Zuletzt geändert von _Peter_ am 7. Jan 2010 14:23, insgesamt 1-mal geändert.

hangman
Erstie
Erstie
Beiträge: 11
Registriert: 25. Aug 2008 08:52

Re: Tipps für "MATCH is sound"?

Beitrag von hangman »

Hallo,

wir haben auch Probleme mit 3.5. Beim 1. der 3 blauen "Äste" komme ich auf diesen Goalterm

Code: Alles auswählen

(result(MATCH(tl(k), tl(l))) ⊫ k) = l
Ich habe versucht die Vollständigkeit darauf anzuwenden aber ohne Erfolg. Die Aussage sieht ja ziemlich trivial aus.

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

Re: Tipps für "MATCH is sound"?

Beitrag von Nathan Wasser »

Ich finde die Aussage zwar nicht sonderlich trivial (gilt nur unter zusätzlichen Bedingungen), aber evtl wäre Unfold Procedure eine Überlegung wert.

Nadine
Mausschubser
Mausschubser
Beiträge: 78
Registriert: 4. Okt 2008 14:41
Wohnort: Mainhausen

Re: Tipps für "MATCH is sound"?

Beitrag von Nadine »

Tipps zu den zwei untersten blauen Zweigen wären hilfreich. :roll:

_Peter_
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 170
Registriert: 1. Okt 2007 19:56

Re: Tipps für "MATCH is sound"?

Beitrag von _Peter_ »

Tipps für den ersten blauen Zweig sind auch gerne gesehen :wink:

Benutzeravatar
C0RNi666
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 114
Registriert: 8. Jan 2008 12:51

Re: Tipps für "MATCH is sound"?

Beitrag von C0RNi666 »

Nathan Wasser hat geschrieben:Ich finde die Aussage zwar nicht sonderlich trivial (gilt nur unter zusätzlichen Bedingungen), aber evtl wäre Unfold Procedure eine Überlegung wert.
Dieser Tip bezieht sich auf den ersten der letzten drei blauen Zweige, allerdings komme ich bei den anderen auch nicht weiter und bin für jeden Hinweis dankbar :)
Win32: Reboot!
Unix: Be root!

hangman
Erstie
Erstie
Beiträge: 11
Registriert: 25. Aug 2008 08:52

Re: Tipps für "MATCH is sound"?

Beitrag von hangman »

Diese Behauptung muss Gelten wenn es ein Matcher für tl(k) und tl(l) gibt. Gibt es andere Bedingungen?

Code: Alles auswählen

(result(MATCH(tl(k), tl(l))) ⊫ k) = l

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

Re: Tipps für "MATCH is sound"?

Beitrag von mister_tt »

Wie kommst du denn darauf? Dies gilt keinesfalls ohne weitere Bedingungen. Da muss hd(k) ja noch mit hd(l) gematcht werden...

hangman
Erstie
Erstie
Beiträge: 11
Registriert: 25. Aug 2008 08:52

Re: Tipps für "MATCH is sound"?

Beitrag von hangman »

Unfold hat geholfen. Danke!

Benutzeravatar
petzchri
Erstie
Erstie
Beiträge: 14
Registriert: 29. Okt 2007 11:10
Wohnort: Worms
Kontaktdaten:

Re: Tipps für "MATCH is sound"?

Beitrag von petzchri »

Servus! Bin auch immer noch bei der letzten Aufgabe und komm beim vorletzten Zweig einfach nicht weiter als:

Bild

Ist jemand schon weiter gekommen? Wo setzt man denn da am bessten an? Lemmas über pair :: σ haben bei mir nicht geklappt :(

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

Re: Tipps für "MATCH is sound"?

Beitrag von Nathan Wasser »

Schauen Sie sich die Induktionshypothese an. Schauen Sie sich den Goalterm an. Was für ein (generalisiertes) Lemma bräuchten Sie um Goalterm und Induktionshypothese gleichzusetzen? Was für Bedingungen müssten da gelten? Sind diese zufällig in den globalen Hypothesen zu finden?

Antworten

Zurück zu „Archiv“