Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Prüfungen im Bachelor-Studium (1. - 5. Semester) » Aufgabe 1 (Übersicht)
Dies ist eine alte Version des Dokuments!
Aufgabe 1
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: curren tSample ( square x y ) = x discardSample ( square x y ) = square y x 1. Definieren Sie korrekursiv eine Fuktion invert: Signal → Signal, so dass invert s das Vorzeichen jedes Wertes s umkehrt. Hinweis: Sie dürfen bei der Definition die üblichen Operationen auf Basistypen (z.B. Arithmetik auf Int) 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: ∀s ∈ Si g n al ∀x ∈ Int . discardSample ( square x −x ) = i n v e r t ( square x −x ) Rechtfertigen Sie alle Beweisschritte.
Aufgabe 5