Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Prüfungen im Bachelor-Studium (1. - 5. Semester) » Aufgabe 1

Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen der Seite angezeigt.

Link zu der Vergleichsansicht

Nächste Überarbeitung		Vorherige Überarbeitung
Nächste ÜberarbeitungBeide Seiten, nächste Überarbeitung
pruefungen:bachelor:thprog-ws15-braindump [15.02.2016 12:18] – angelegt Ceroxpruefungen:bachelor:thprog-ws15-braindump [12.02.2020 08:34] – vulgrim
Zeile 1: Zeile 1:
 Aufgabe 1 Aufgabe 1
 +(Warnung: Diese Aufgabe ist potentiell so nicht richtig)
  
-Wir definieren ein Termersetzungssystem über das aus zwei binären Funktionssymbolen+Wir definieren ein Termersetzungssystem über das aus zwei binären  
 + 
 +Funktionssymbolen
 º und ∗ (in Infixnotation geschrieben) bestehenden Signatur º und ∗ (in Infixnotation geschrieben) bestehenden Signatur
 Σ durch: Σ durch:
 +
 (x º y) º z → (x º y) ∗ z (x º y) º z → (x º y) ∗ z
 +
 x º y → (y º x) º x x º y → (y º x) º x
  
 1. Zeigen Sie mittels Polynomordnungen, dass das Sytem stark normalisierend 1. Zeigen Sie mittels Polynomordnungen, dass das Sytem stark normalisierend
 ist. ist.
 +
 2. Ist das System konfluent? Geben Sie einen Beweis bzw. ein Gegenbeispiel 2. Ist das System konfluent? Geben Sie einen Beweis bzw. ein Gegenbeispiel
 an. an.
Zeile 14: Zeile 20:
  
 Aufgabe 2 Aufgabe 2
 +
 +Man erinnere sich an folgende auf Church-Kodierung definierte Funktionen:
 +<code>
 +• 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)</code>
 +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 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 Aufgabe 4
 +
 +Alternierender Signalwert zwischen x und y
 +<code>
 +codata Signal where
 +cur : Signal −> Boolean
 +next : Signal −> Signal
 +</code>
 +Dann konstruiert die wie folgt korekursiv definierte Funktion square
 +aus ihren Argumenten x,y ein zw. x und y alternierendes Signal:
 +<code>cur ( square x y ) = x
 +next ( square x y ) = square y x
 +</code>
 +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 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