Übung 1
In dieser Übung überlegen wir uns, ob die in der ersten Hausaufgabe zusätzlich eingeführten Regeln die Sprache wesentlich verändern. Es geht also um eine Sprache mit dieser Syntax:
t ::= true ∣ false ∣ t ∧ t
Die ursprüngliche Semantik der Sprache wird durch eine Relation →1 zwischen Termen beschrieben:
true ∧ t →1 t
false ∧ t →1 false
t1 →1 t1′
t1 ∧ t2 →1 t′1 ∧ t2
Die erweiterte Semantik dieser Sprache wird durch eine Relation →2 zwischen Termen beschrieben:
true ∧ t →2 t
false ∧ t →2 false
t ∧ false →2 false
t ∧ t →2 t
t1 →2 t′1
t1 ∧ t2 →2 t′1 ∧ t2
t2 →2 t′2
t1 ∧ t2 →2 t1 ∧ t′2
Die zusätzlichen Regeln der Relation →2 sind so gewählt, daß sich die Semantik der Sprache gegenüber der Relation →1 “nicht wirklich” ändert.
Aufgaben
-
Formalisieren Sie die Eigenschaft, daß sich die Semantik der Sprache “nicht wirklich” ändert, als Theorem.
-
Beweisen Sie das Theorem.
Ergebnisse
Wir sind in der Übung nicht sehr weit gekommen, weil diese Aufgabe viel schwieriger als erwartet war. Wir haben den Teil des Beweises für die Regel
t ∧ false →2 false
angefangen, den ich versuchen werde, noch online zu stellen. Wichtige Erkenntnisse aus der Übung:
-
Vor dem Beweisen sollte man genau formulieren, was man beweisen möchte.
-
Vor dem Beweisen sollte man darüber nachdenken, ob die Eigenschaft überhaupt stimmt.