Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Prüfungen im Bachelor-Studium (1. - 5. Semester) » Aufgabe 1
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