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.

Link zu der Vergleichsansicht

Nächste Überarbeitung
Vorherige Überarbeitung
pruefungen:bachelor:thprog-ws15-braindump [15.02.2016 12:18] – angelegt Ceroxpruefungen:bachelor:thprog-ws15-braindump [12.02.2020 09:05] (aktuell) vulgrim
Zeile 1: Zeile 1:
-Aufgabe 1+====== Aufgabe 1 ======
  
-Wir definieren ein Termersetzungssystem über das aus zwei binären Funktionssymbolen+(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 º 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.
  
  
-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 
 +
 +
 +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 
 +
 +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 
 +<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 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 3+====== Aufgabe 5 ======
  
-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, dass L nicht regulär ist.
  
 +Das darf gerne noch jemand in ,tex übertragen, ich hab' erstmal genug von ThProg...
 +by Cerox