Sie befinden sich hier: Termine » Prüfungsfragen und Altklausuren » Prüfungen im Bachelor-Studium (1. - 5. Semester) » thprog-ws15-braindump   (Übersicht)

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:

cur ( square x y ) = ...
next ( square x y ) = ...

1. Definieren Sie korrekursiv eine Fuktion 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