====== Aufgabe 1 ======
(Warnung: Diese Aufgabe ist potentiell so nicht richtig)
Wir definieren ein Termersetzungssystem über das aus zwei binären
Funktionssymbolen
º und ∗ (in Infixnotation geschrieben) bestehenden Signatur
Σ durch:
(x º y) º z → (x º y) ∗ z
x º y → (y º x) º x
1. Zeigen Sie mittels Polynomordnungen, dass das Sytem stark normalisierend
ist.
2. Ist das System konfluent? Geben Sie einen Beweis bzw. ein Gegenbeispiel
an.
====== Aufgabe 2 ======
Man erinnere sich an folgende auf Church-Kodierung definierte Funktionen:
• Church-Numerale
succ n = λ f a. f(n f a)
pred n = f st(n(λp.pair(snd p)(succ(snd p)))(paird0ed0e))
isZero n = n(λx. f alse) true
geq n m = isZero(n pred m)
• Church-Booleans
true = λxy.x
f alse = λxy.y
• Church-Paare
pair a b = λ select.select a b
f st p = p(λxy.x)
snd p = p(λxy.y)
Man erinnere sich ferner, dass die Zahl n durch den λ-Term n = λ f a. f
n
a
dargestellt wird, also z.B.
0 = λ f a.a
1 = λ f a. f a
2 = λ f a. f(f a)
1. Geben Sie die ersten vier δβ-Rekursionsschritte des Terms sub(pred(pair 0 2)) 1
unter a) normaler und b) applikativer Reduktion an. Markieren Sie
(durch Unterstreichen) in jedem Schritt den zu reduzierenden Redex.
Nevenbemerkung: Wir sehen (anders als für die Operationen one,
two, etc. inder Probeklausur!) dne als Abkürzung für den entsprechenden
λ-Term an.
Hinweis: die Reduktionsstrategie bezieht sich ausdrücklich auch auf
δ-Reduktion. D.h. bei normaler Reduktion werden zuerst die linken
Seiten von Funktionsanwendungen (also die Funktionen βδ-
reduziert, von außen nach innen, und erst dann die Argumente von
3
Funktionsanwendungen, bei applikativer Reduktion dagegen zuerst
die Argumente von Funktionsanwendungen.
2. Man erinnere sich, dass die Church-Numerale und die Church-Booleans
in System F den Typ N := ∀a(a → a) → a → a bzw. B :=
∀a.a → a → a haben.
Nicht bekannt...
====== Aufgabe 3 ======
Wir erinnern an den Datentyp der Listen und einige hierauf rekursiv
definierte Standadfunktionen:
data L i s t a = Nil | Cons a ( L i s t a )
length(Nil) = 0
length(Cons x xs) = 1 + length(xs)
Nil ⊕ ys = ys
( Cons x xs ) ⊕ ys = Cons x ( xs ⊕ ys )
cMap f Nil = Nil
cMap f ( Cons x xs ) = Cons ( f x ) ( cMap f xs )
Beweisen Sie mittels struktureller Induktion, dass
1. ∀ x xs.length(cMap x xs) = length(xs)
2. ∀ z xs ys.cMap z(xs ⊕ ys) = (cMap z xs) ⊕ (cMap z ys)
Geben Sie im Induktionsschritt die Induktionsannahme explizit an, und
erläutern Sie alle Schritte des Beweises.
====== Aufgabe 4 ======
Alternierender Signalwert zwischen x und y
codata Signal where
cur : Signal −> Boolean
next : Signal −> Signal
Dann konstruiert die wie folgt korekursiv definierte Funktion square
aus ihren Argumenten x,y ein zw. x und y alternierendes Signal:
cur ( square x y ) = x
next ( square x y ) = square y x
1. Definieren Sie korekursiv eine Funktion ''alt: Signal -> Signal'', so dass ''alt s''
den jeweils gesetzten Wert für ein gesetztes Bit ausgibt ( Ist x gesetzt, gebe x aus. Sind beide Werte gesetzt, nichts)
Hinweis: Sie dürfen bei der Definition die üblichen Operationen auf
Basistypen (z.B. Arithmetik auf Boolean) als gegeben annehmen.
2. Geben Sie die Bedingungen an, die eine Relation erfüllen muss, um
eine Bisimulation auf signal zu sein. (Diese ergeben sich durch Spezialisierung
des allgemeinen Begriffs aus der Vorlesung auf den Kodatentyp
signal)
3. Beweisen Sie die folgende Eigenschaft durch Koinduktion:
...
====== Aufgabe 5 ======
Sei L die Sprache über Σ = {a, b, c}*, die gerade aus allen Worten über Σ
besteht, die w und w gespielt bestehen. Z.B. sind ε, aa und abccba in L, nicht aber ε, aba, abcabc, ...
Ist L regulär? Wenn ja, geben sie einen regulären Ausdruck für L an und
erläutern Sie, warum dieser L definiert. Andernfalls zeigen Sie mittels des
Pumping-Lemma, dass L nicht regulär ist.
Das darf gerne noch jemand in ,tex übertragen, ich hab' erstmal genug von ThProg...
by Cerox