Für alle aeAexp ...

derDaniel
Mausschubser
Mausschubser
Beiträge: 76
Registriert: 2. Mai 2012 15:25

Für alle aeAexp ...

Beitrag von derDaniel »

Hallo,

in der Hausübung in Aufgabe 2 sollen wir gewissenmaßen das Beispiel aus der Vorlesung beweisen.
Ich habe mich gefragt, warum es 5 Fallunterscheidungen gibt, wenn a aus Aexp ist.
Wieso ist der Fall a=n für neN und a=x für xeLoc dabei.
Da sind doch andere Menge und eben disjunkt mit Aexp.

Wieso müssen die beachtet werden?

LG
Daniel

derDaniel
Mausschubser
Mausschubser
Beiträge: 76
Registriert: 2. Mai 2012 15:25

Re: Für alle aeAexp ...

Beitrag von derDaniel »

Achso, das sind die Voraussetzungen oder?

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: Für alle aeAexp ...

Beitrag von L4_ »

Hey,

bitte teile z.B. im Titel mit, auf welche Übung, welche Aufgabe du dich beziehst und erwähne unter anderem, auf welchen Folie(n) sich deine Fragen bezieht.
ich kann jetzt nur interpretieren was du meinst:

Ich nehme an du meinst Modul 6, Folie 24.
Dort steht das Beweisprinzip für Aexp, um somit eine Induktion für Aexp zu ermöglichen.
Das bedeutet, es wird für jede Regel des Kalküls eine Aussage formuliert (das sind genau 5 Regeln bei Aexp), wobei man für die jeweilige Regel alle auftauchenden Werte allquantifiziert und damit fordert, dass das Prädikat P gelten soll.

Bei der Regel rLoc lautet der arithmetische Audruck einfach nur "X", d.h. wir fordern, dass das Prädikat P für alle X gilt.
Analog für die Regel rN.

Bei den letzten drei Aussagen muss man folgendes beachten:
Für alle Allquantifizierungen von Aexp muss vorher jeweils die Annahme gemacht werden, dass diese zuvor wahr sind (deswegen taucht z.B. bei r+ bei der Aussage "P(a1) /\ P(a2) => P(a1+a2)" eine Implikation auf, da P(a1) und P(a2) erst als wahr angenommen werden müssen - das ist nämlich ein Induktionsschritt!).

Bei Allquantifizierungen von anderen Wertebereichen müssen wir diese Annahme nicht tun, da wir ja eine Induktion über Aexp und nichts anderes durchführen wollen.

Wenn man jetzt beispielsweise das Beweisprinzip für Bexp aufschreibt, so gilt bei der Induktion darüber das gleiche:
Alle Allquantifizierungen von Bexp müssen vorher erst als wahr angenommen werden, und für alle anderen Allquantifizierungen (in dem Fall auch über Aexp) müssen keine Annahmen gemacht werden.

Klärt das deine Fragezeichen? ;)

VG

derDaniel
Mausschubser
Mausschubser
Beiträge: 76
Registriert: 2. Mai 2012 15:25

Re: Für alle aeAexp ...

Beitrag von derDaniel »

Ja etwas.

rN und rLoc müssten ja auch für die Aufgabe 3 relevant sein und ich frage mich wie die Notation zu verstehen ist.
Ich versuche die Notation für Aufgabe 3 ähnlich der auf Folie 23-24 im Modul 6 zu machen.

Wie notiere ich das für die Fälle r= und r<=, dort muss man ja Variablen auf N verwenden, um auf den boolschen Wert zu schließen. Darf davon ausgehen, dass n1 und n2 in dem Kontext deterministisch ausgewertet werden oder muss man das wie auf den Folien irgendwie mit für alle in der Induktion noch angeben.

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Re: Für alle aeAexp ...

Beitrag von L4_ »

derDaniel hat geschrieben: Ja etwas.
rN und rLoc müssten ja auch für die Aufgabe 3 relevant sein und ich frage mich wie die Notation zu verstehen ist.
Nein, rN und rLoc sind Regeln aus Aexp.
Bei Aufgabe 3 betrachtest du lediglich Regeln aus Bexp.
Die "Notation" in diesen Beweisprinzipien stellt einfach nur die Aussagen auf, die erfüllt sein müssen, damit eine gewisse Eigenschaft (in Form eines Prädikates P) für alle Ausdrücke aus einem Kalkül gelten.
In der Vorlesung bzw. Übung wird also die Eigenschaft "Deterministische Auswertung" untersucht.
derDaniel hat geschrieben: Wie notiere ich das für die Fälle r= und r<=, dort muss man ja Variablen auf N verwenden, um auf den boolschen Wert zu schließen.
"Variablen auf N verwenden" verstehe ich nicht.
Du möchtest, dass P(a1 = a2) bzw. P(a1 <= a2) gilt.
Da du in Aufgabe 3 über Bexp induzierst, musst du lediglich fordern, dass das für alle a1, a2 aus Aexp gilt (so wie ich es in meiner vorigen Antwort ausführlich erklärt habe). Da muss man wirklich nicht allzuviel ins detail nachdenken, was mit den Elementen n aus N oder x aus Loc ist. Du betrachtest immer nur die sichtbaren elemente in dem Ausdruck, von dem du die Eigenschaft P forderst.
Somit wäre die zu beweisende Aussage recht einfach notiert ;)
derDaniel hat geschrieben: Darf davon ausgehen, dass n1 und n2 in dem Kontext deterministisch ausgewertet werden oder muss man das wie auf den Folien irgendwie mit für alle in der Induktion noch angeben.
Ja, das Wissen darfst du verwenden, aber zuvor fängst du auch erst mit jeweils zwei verschiedenen Auswertungen n1, n2 und n1', n2' an
Bitte den Hinweis zu Aufgabe 3 nicht missverstehen:
Mit dem Hinweis ist nur gemeint, dass man versuchen soll den Beweis durchzuführen, ohne sich den Beweis zu Aexp als Blaupause/Schema/Orientierung zu nehmen.

derDaniel
Mausschubser
Mausschubser
Beiträge: 76
Registriert: 2. Mai 2012 15:25

Re: Für alle aeAexp ...

Beitrag von derDaniel »

Ok damit komm ich weiter.
Thx :)

Antworten

Zurück zu „Archiv“