Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Prüfungen im Bachelor-Studium (1. - 5. Semester) » Aufgabe 1 (Übersicht)
Unterschiede
Hier werden die Unterschiede zwischen zwei Versionen der Seite angezeigt.
Beide Seiten, vorherige ÜberarbeitungVorherige ÜberarbeitungNächste Überarbeitung | Vorherige ÜberarbeitungLetzte ÜberarbeitungBeide Seiten, nächste Überarbeitung | ||
pruefungen:bachelor:thprog-ws15-braindump [15.02.2016 12:21] – Cerox | pruefungen:bachelor:thprog-ws15-braindump [12.02.2020 09:03] – vulgrim | ||
---|---|---|---|
Zeile 1: | Zeile 1: | ||
- | Aufgabe 1 | + | ====== |
+ | |||
+ | (Warnung: Diese Aufgabe ist potentiell so nicht richtig) | ||
Wir definieren ein Termersetzungssystem über das aus zwei binären | Wir definieren ein Termersetzungssystem über das aus zwei binären | ||
Zeile 10: | Zeile 12: | ||
x º y → (y º x) º x | x º y → (y º x) º x | ||
- | |||
- | |||
1. Zeigen Sie mittels Polynomordnungen, | 1. Zeigen Sie mittels Polynomordnungen, | ||
Zeile 20: | Zeile 20: | ||
- | 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: | ||
+ | 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, | ||
+ | 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: | ||
+ | < | ||
+ | next ( square x y ) = square y x | ||
+ | </ | ||
+ | 1. Definieren Sie korekursiv eine Funktion "alt: Signal -> Signal", | ||
+ | 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 | + | ====== |
- | Aufgabe 4 | ||
- | 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, | ||
+ | Das darf gerne noch jemand in ,tex übertragen, | ||
+ | by Cerox |