Programmierung
Sommer 2021
Abkürzung zum Übungsmaterial

Inhalte der Übungen

Im Rahmen der zur Lehrveranstaltung gehörenden Übungen wenden wir das in der Vorlesung erlernte Wissen an und versuchen die Theorie an Beispielen zu illustrieren:

  • Grundlagen der funktionalen Programmierung in Haskell
  • Unifikationsalgorithmus
  • Beweis von Programmeigenschaften mit struktureller Induktion
  • Lambda-Kalkül
  • Logikprogrammierung in Prolog
  • Abstrakte Maschinen AM0 und AM1 sowie deren Übersetzung von/nach C
  • Beweis von Programmeigenschaften mit dem Hoare-Kalkül
  • Abstrakte Maschinen mit Haskell

News

  • 09.08.2021: Es gibt inzwischen Musterlösungen zu den Wiederholungsaufgaben von Übung 14. Diese findet ihr unten verlinkt. Außerdem findet ihr unten die Hinweise zur Online-Klausur zusammengefasst. Wer die Probeklausur am 02.08.2021 verpasst hat, der findet im OPAL-Kurs die Aufgaben incl. Musterlösung unter dem Reiter "Übungsblätter".
  • 09.06.2021: Unten findet ihr die Materialien aus Übung 8 zur Logikprogrammierung. Beachtet bitte, dass die Zeilennummern in den SLD-Refutationen sich zwischen den Mitschriften und den Slides unterscheiden. Das liegt einfach an der automatischen Nummerierung in den Slides. In jedem Fall sollten die Angaben konsistent sein.
  • 02.06.2021: Die Materialien aus Übung 7 sind nun unten zu finden. Zur Klammer-Frage aus der Dienstag-Übung: um den rekursiven Aufruf in Aufgabe 1c müssen Klammern gesetzt werden. Außerdem findet vom 31.05. bis zum 20.06.2021 die Lehrveranstaltungsevaluation statt. Ich würde mich freuen, wenn ihr daran teilnehmt und Feedback zur Übung hinterlasst. Den Link findet ihr unten in den Materialien.
  • 19.05.2021: Das Material für Übung 6 ist online. Die Aufgabe 2 ist einem zusätzlichen kleinen Video ausgelagert. Ich habe gerade noch einmal alle Links zu Slides, Handouts und Notizen getestet - bei mir funktionierten alle. Sollte ich da etwas übersehen haben, dann schreibt mir gern eine Nachricht, welcher Link nicht funktioniert. :)
  • 28.04.2021: Das Material für Übung 3 ist jetzt verfügbar. Ich habe noch ein kurzes Video zur Aufgabe 3 gedreht, das kurz die Idee erklärt. Außerdem findet ihr eine Text-Erklärung zu den Funktionen höherer Ordnung in den Materialien. Kleiner Hinweis zum Inhalt: ich hatte in der Übung behauptet, dass in Aufgabe 2 beim Filtern der geraden Zahlen eine length Funktion fehle - das ist natürlich Quatsch, da habe ich mich von den evenNodes verwirren lassen :)
  • 21.04.2021: Die Materialien für Übung 2 sind nun online. Auf Nachfrage lade ich auch die annotierten Slides hoch (nachträglich auch noch für die erste Woche). Ich bearbeite diese Notizen nicht nochmal, d.h. es können Markierungen zu Fragen enthalten sein, die nicht mit der eigentlichen Aufgabe verbunden sind - lasst euch also nicht verwirren.
    Beachtet bitte die Operatorprioritäten, v.a. die in der Übung diskutierte f x:xs == (f x) : xs /= f (x:xs).
    Die Aufgabe 3 zu den algebraischen Datentypen werden wir in der nächsten Woche besprechen - ihr findet aber auch eine ausführliche Erläuterung in den Materialien unten.
  • 18.04.2021: Für Übung 2 findet ihr unten Templates zum Download (zip-Archiv), die euch mühsames Abtippen ersparen sollen. In den Übungen werde ich diese Templates als Startpunkt verwenden.
  • 10.04.2021: Am Montag beginnt das Semester - pünktlich gibt es auch von mir einige wichtige Infos auf dieser Seite. Auch in diesem Semester werden die Übungen online stattfinden müssen. Dafür werde ich weiter Zoom nutzen und freue mich euch in einer meiner Übungen am Dienstag oder Mittwoch, jeweils in der 2. DS, begrüßen zu dürfen.
  • 31.03.2021: Die Website befindet sich noch im Aufbau.

Ich bemühe mich stets euch das Lernen so angenehm, unterhaltsam und einfach wie möglich zu machen. Das ist mein eigener Anspruch und dafür opfere ich auch gern mal meine Freizeit. Ein Beispiel, wofür relativ viel Zeit drauf gegangen ist, seht ihr gerade vor euren Augen: diese Website. Sie ist sicher nicht perfekt und sicher auch nicht notwendig, um euch eine Übung zu bieten. Ebenso ensteht mein ganzes Material wie Slides und Mitschriften nicht mal eben so. Vielleicht hat der ein oder andere schon erkannt, worauf es hinaus laufen soll: wenn du Lust und das nötige Kleingeld dafür hast, würde ich mich sehr freuen, wenn du meine Arbeit unterstützt und mir vielleicht einen Kaffee oder ein Mensaessen spendierst. Aber versteht mich bitte nicht falsch: ich mache das alles wirklich super gerne und habe auch meinen Spaß daran - und Geld wird auf meine Arbeit nie einen Einfluss haben. Und ja, für meine Tutorentätigkeit werde ich auch als studentische Hilfskraft bezahlt - mit vier bzw. fünf Stunden für zwei Übungen deckt das aber gerade einmal die Übungszeit und ein wenig Vorbereitung ab.

Informationen

Bitte beachtet stets die Informationen auf der Website der Lehrveranstaltung sowie im zugehörigen OPAL-Kurs. Bei Fragen oder Problemen könnt ihr euch an mich oder an Thomas Ruprecht wenden. Mich erreicht ihr auch schnell und problemlos via Telegram @oakoneric.

Die in meinen Übungen verwendeten Materialien habe ich größtenteils in meiner Freizeit erstellt. Sie stammen insbesondere nicht vom Lehrstuhl und können damit trotz gründlicher Arbeit noch Fehler enthalten. Die Slides und den zugehörigen Latex-Code dazu findet ihr in meinem entsprechenden Github-Repository. Findet ihr einen Fehler in meinen Lösungen, dann fühlt euch eingeladen mir dies mitzuteilen oder direkt selbst mit einem Request zu beheben.

Ich werde versuchen stets die aktuellen Vorlesungen und Übungsblätter zu verlinken, um ein einheitliches System zu erhalten - mal sehen wie gut das funktioniert. Für die verlinkten Materialien vom Lehrstuhl gelten die entsprechenden Hinweise auf der Website der Lehrveranstaltung und im OPAL-Kurs.

Zur Klausurvorbereitung findet ihr auf dem FTP-Server vom iFSR einige Altklausuren. Ihr benötigt dafür eine VPN-Verbindung ins Uni-Netz.

Online-Übungen

Die Übungen werden in diesem Semester ausschließlich digital gehalten. Meine Online-Übungen finden wöchentlich zu folgenden Zeiten statt:

  • Dienstag, 2. Doppelstunde: 920 bis 1050 Uhr
  • Mittwoch, 2. Doppelstunde: 920 bis 1050 Uhr

Ich werde dafür die Plattform Zoom nutzen Der Zugangslink bleibt stets der gleiche - ihr findet ihn hier und im OPAL-Kurs.

zum Meeting

Nach jedem Meeting stelle ich die Notizen, verwendeten Folien und eine Aufzeichnung des Meetings (sofern niemand etwas dagegen hat) online. Ihr findet das gesamte Material unten in der Übungsübersicht. Die Zugangsdaten zu den Videos habt ihr per Mail erfahren (oder schreibt mich an, wenn ihr später dazu gestoßen seid).

Evaluation

Wie in jedem Semester gibt es auch diesmal eine Lehrveranstaltungsevaluation. Ich freue mich über eure Teilnahme und euer Feedback. Die Umfrage ist komplett anonym, also lasst gern auch kritische Worte da. :)

Lehrveranstaltungsevaluation

Praktische Aufgaben

Leider haben wir in den Übungen nicht die Zeit um allen einen funktionsfähigen Compiler und ein optimales Setup zu garantieren. Daher bitte ich euch die Informationen auf der Lehrveranstaltungswebsite zu beachten. Wie immer sind natürliche auch Google und YouTube sehr gute Quellen für weitere Hilfe. Im Zweifelsfall hilft euch sicher auch der iFSR. Außerdem habe ich euch einige Hinweise zusammengetragen:

Hinweise zu Haskell    Hinweise zu Prolog

Für das Selbststudium gibt es zwei sehr gute Bücher, die ich euch empfehlen möchte. Beide Bücher sind frei online verfügbar, sogar ohne VPN und ohne SLUB-Zugang.

  • Learn You a Haskell For Great Good! Ein sehr gut geschriebenes Buch, kann ich nur empfehlen einmal reinzusehen. Erklärt sehr ausführlich und kurzweilig. Damit sollte jeder Haskell verstehen können. Eine Online-Version des Buches findet ihr hier.
  • Real World Haskell Ebenso ein sehr gutes Buch, deckt aber wesentlich mehr Inhalte ab, als wir brauchen werden. Die Online-Version gibt's hier.

Übungsübersicht

Im Folgenden findet ihr das gesamte Material meiner Übungen und den Vorlesungsinhalten. Die Vorlesungsvideos sind urheberrechtlich seitens der Professur geschützt und keinsweg mein Eigentum. Es sind die Hinweise im OPAL-Kurs einzuhalten. Um die Vorlesungsvideos abzurufen benötigt ihr eine VPN-Verbindung ins Uni-Netz. Meine Übungsvideos sind ein wenig passwortgeschützt - die Zugangsdaten erfahrt ihr in den Übungen oder ihr schreibt mir.

Woche 1: Einführung in Haskell
12.04. bis 16.04.2021
  • Vorlesungsvideo
  • Übungsblatt 1
  • Videoaufzeichnung der Übung (Dienstag)
  • Lösungen
    • Aufgabe 1: siehe Slides
    • Aufgabe 2

      Wir berechnen die Fakultät \(n! = \prod_{i=1}^n i\).

      -- Aufgabe 2(a)
      fac :: Int -> Int
      fac 0 = 1
      fac n = n * fac (n-1)

      Wir summieren Fakultäten auf, d.h. berechnen \(\operatorname{sumFacs}(n,m) = \sum_{i=n}^m i!\). Dabei können wir wahlweise die obere Grenze oder die untere Grenze "rausziehen".

      -- Aufgabe 2(b)
      sumFacs :: Int -> Int -> Int
      sumFacs n m
      	| n > m = 0
      	| otherwise = fac n + sumFacs (n+1) m
      
      sumFacs' :: Int -> Int -> Int
      sumFacs' n m
      	| n > m = 0
      	| otherwise = fac m + sumFacs' n (m-1)
    • Aufgabe 3

      Wir berechnen die Fibonacci-Zahlen und nutzen dafür die bereits gegebene Rekursionsvorschrift \(f_n = f_{n-1} + f_{n-2}\) mit den Startwerten \(f_0 = 1\) und \(f_1 = 1\).

      fib :: Int -> Int
      fib 0 = 1
      fib 1 = 1
      fib n = fib (n-1) + fib (n-2)
      
      fib' :: Int -> Int
      fib' n = fib_help 1 1 n
      
      fib_help :: Int -> Int -> Int -> Int
      fib_help x _ 0 = x
      fib_help x y n = fib_help y (x+y) (n-1)

      Wenn man mittels :set +s die Laufzeitmessung in GHCi aktiviert und fib n für große n versucht zu berechnen, wird man feststellen, dass das sehr lange dauert. Daher kann man eine alternative Variante implementieren, die drei "Speicherplätze" nutzt und somit ein iteratives Verfahren nachahmt (vgl. Slides).

      fib' :: Int -> Int
      fib' n = fib_help 1 1 n
      
      fib_help :: Int -> Int -> Int -> Int
      fib_help x _ 0 = x
      fib_help x y n = fib_help y (x+y) (n-1)
Woche 2: Haskell - Datentypen
19.04. bis 23.04.2021
  • Vorlesungsvideo
  • Übungsblatt 2
  • Coding Templates
  • Videoaufzeichnung der Übung (Mittwoch)
  • Lösungen
    • Aufgabe 1: Listenoperationen
      1. eine Liste umkehren
        rev :: [Int] -> [Int]
        rev [] = []
        rev (x:xs) = rev xs ++ [x]
      2. Sortierung einer Liste prüfen
        isOrd' :: [Int] -> Bool
        isOrd' [] = True
        isOrd' [x] = True
        isOrd' (x:y:xs) = x <= y && isOrd' (y:xs)
      3. (sortierte) Listen zusammenfügen
        merge :: [Int] -> [Int] -> [Int]
        merge [] ys = ys
        merge xs [] = xs
        merge (x:xs) (y:ys)
        | x < y = x : merge xs (y:ys)
        | otherwise = y : merge (x:xs) ys
      4. (unendliche) Liste der Fibonacci-Zahlen
        fib :: Int -> Int
        fib 0 = 1
        fib 1 = 1
        fib n = fib (n-1) + fib (n-2)
        
        fib' :: Int -> Int
        fib' i = stack 1 1 i
        where stack f0 f1 0 = f0
        stack f0 f1 i = stack f1 (f0 + f1) (i-1)
        
        fibs :: [Int]
        fibs = fibAppend 0
        where fibAppend x = fib x : fibAppend (x+1)
        Testen kann man diese Funktion beispielsweise mittels take 7 fibs, was uns die ersten sieben Fibonacci-Zahlen zurückgibt. take ist dabei eine Funktion aus der Standard-Bibliothek Prelude vom Typ take :: Int -> [Int] -> [Int], d.h. man kann mit dieser Funktion nicht ein Intervall von gewünschten Zahlen angeben (wie eine Frage in der Übung war), siehe auch hier. Man kann nun zwischen den beiden Varianten fib und fib' umschalten und die Laufzeitunterschiede (vgl. auch Übung 1, Aufgabe 3) vergleichen.
    • Aufgabe 2: Zeichen & Zeichenketten
      1. Präfix-Test - Wir testen ob ein String Präfix eines weiteren Strings ist.
        isPrefix :: String -> String -> Bool
        isPrefix [] _ = True
        isPrefix _ [] = False
        isPrefix (p:ps) (c:cs) = p == c && isPrefix ps cs
      2. Wir testen das Vorkommen eines Patterns in einem gegebenen String.
        countPattern :: String -> String -> Int
        countPattern "" "" = 1
        countPattern _  "" = 0
        countPattern xs yys@(y:ys)
        | isPrefix xs yys = 1 + countPattern xs ys
        | otherwise       = countPattern xs ys 
    • Aufgabe 3: algebraische Datentypen
      1. Beispielbaum
        mytree :: BinTree
        mytree = Branch 0 
        ( Nil )
        ( Branch 3 
        ( Branch 1 Nil Nil )
        ( Branch 5 Nil Nil )
        )
      2. Test auf Baum-Gleichheit
        equal :: BinTree -> BinTree -> Bool
        equal Nil              Nil              = True
        equal Nil              (Branch y l2 r2) = False
        equal (Branch x l1 r1) Nil              = False
        equal (Branch x l1 r1) (Branch y l2 r2) = (x == y) && (equal l1 l2) && (equal r1 r2) 
      3. Einfügen in einen Suchbaum
        insert :: BinTree -> [Int] -> BinTree
        insert t     [] = t
        insert t (x:xs) = insert t' xs
        where t' = insertSingle t x
        insertSingle Nil            x = Branch x Nil Nil
        insertSingle (Branch y l r) x
        | x < y     = Branch y (insertSingle l x) r
        | otherwise = Branch y l                  (insertSingle r x)
Woche 3: Haskell - Funktionen höherer Ordnung
26.04. bis 30.04.2021
  • Vorlesungsvideo
  • Übungsblatt 3
  • Coding Templates
  • Videoaufzeichnung der Übung und Erklärung zu Aufgabe 3 (foldleft-Funktion)
  • Lösungen
    • Aufgabe 1: Bäume mit beliebig vielen Kindern - data RoseTree = Node Int [RoseTree]
      1. Anzahl der Blätter zählen:
        countLeaves :: RoseTree -> Int
        countLeaves (Node _ [] )    = 1
        countLeaves (Node _ [t])    = countLeaves t
        countLeaves (Node x (t:ts)) = countLeaves t + countLeaves (Node x ts)
      2. Prüfen, ob ein RoseTree immer eine gerade Anzahl an Kindern hat

        Variante 1: durch Abspalten von immer zwei Bäumen aus der Liste können wir am Ende feststellen, ob die Liste gerade Länge (es bleibt [] übrig) oder ungerade Länge (es bleibt eine einelementige Liste [t] übrig) hatte

        evenNodes :: RoseTree -> Bool
        evenNodes (Node _  []       ) = True
        evenNodes (Node x  [t]      ) = False
        evenNodes (Node x (t1:t2:ts)) = evenNodes (Node x ts) && evenNodes t1 && evenNodes t2

        Variante 2: Wir prüfen explizit, ob die Länge der Liste gerade ist (mittels length-Funktion) und testen das erste Listenelement mit evenNodes', die RoseTree verarbeiten kann, sowie die Restliste mit einer Funktion evenNodes'', die Listen [RoseTree] verarbeiten kann.

        evenNodes' :: RoseTree -> Bool
        evenNodes' (Node _ []) = True
        evenNodes' (Node _ ts) = mod (length ts) 2 == 0 && evenNodes'' ts
        where
        evenNodes'' :: [RoseTree] -> Bool
        evenNodes'' []     = True
        evenNodes'' (t:ts) = evenNodes' t && evenNodes'' ts
    • Aufgabe 2: Funktionen höherer Ordnung

      Für diese Aufgabe gibt es viele verschiedene Varianten, ich erwähne hier nur einige davon. Entgegen meiner Behauptung in den Übungen benötigt man natürlich beim Filtern der geraden Zahlen keine length-Funktion; da hab ich mich von den evenNodes von oben verwirren lassen ;)

      f :: [Int] -> Int
      f xs = foldr product 1 (map square (filter even' xs))
      where even' x = mod x 2 == 0
      square x = x * x
      product x y = x * y
      
      f' :: [Int] -> Int
      f' xs = foldr (*) 1 (map (^2) (filter even xs))
      
      f'' :: [Int] -> Int
      f'' = foldr (*) 1 . map (^2) . filter even
      
      f''' :: [Int] -> Int
      f''' = foldr (*) 1 . map (^2) . filter ((== 0) . (`mod` 2))
    • Aufgabe 3: Faltung einer Liste von links
      foldleft :: (Int -> Int -> Int) -> Int -> [Int] -> Int
      foldleft f x []     = x
      foldleft f x (y:ys) = foldleft f (f x y) ys
Woche 4: Haskell - Typpolymorphie und Unifikation
03.05. bis 07.05.2021
  • Beide Übungen finden ganz normal statt - auch die Mittwoch-Übung findet trotz des Dies Academicus wie geplant am Mittwoch, 05. Mai 2021 um 920 Uhr statt.

  • Vorlesungsvideo
  • Übungsblatt 4
  • Coding Templates
  • Videoaufzeichnung der Übung (Dienstag)
  • Lösungen - Aufgabe 1 Wir betrachten den polymorphen Datentyp data BinTree a = Branch a (BinTree a) (BinTree a) | Leaf a deriving Show.
    1. Beispielbaum
      testTree :: BinTree Int
      testTree = Branch 5
      (Leaf 1)
      (Branch 12
      (Branch 4
      (Leaf 0)
      (Leaf 0))
      (Branch 12
      (Leaf 0)
      (Leaf 1)))
    2. minimale Tiefe eines Baumes
      depth :: BinTree a -> Int
      depth (Leaf   _    ) = 1
      depth (Branch _ l r) = 1 + min (depth l) (depth r)
      -- Hinweis: Die Funktion min ist in der Haskell-Standardbibliothek vorhanden
    3. Beschriftungen eines Baumes durch Beschriftungsfolge ersetzen
      paths :: BinTree a -> BinTree [a]
      paths = go []
      where go :: [a] -> BinTree a -> BinTree [a]
      go prefix (Leaf   x    ) = Leaf   (prefix ++ [x])
      go prefix (Branch x l r) = Branch (prefix ++ [x]) (go (prefix ++ [x]) l) (go (prefix ++ [x]) r)
    4. map-Funktion für Bäume
      tmap :: (a -> b) -> BinTree a -> BinTree b
      tmap f (Leaf   x    ) = Leaf   (f x)
      tmap f (Branch x l r) = Branch (f x) (tmap f l) (tmap f r)
    Lösungen - Aufgabe 2 Das Folgende sind nur kurze Lösungen, die ausführlicheren Lösungen findet ihr in den Slides bzw. den Mitschriften der Übung.
    • Teil (a): \begin{align*} \definecolor{highlight}{rgb}{.96,.57,0} \newcommand{\col}[1]{\textcolor{highlight}{#1}} &\left\{\left(\begin{array}{lcrlcl} \col{\sigma(}\sigma(&x_1&,\alpha) \col{,} &\ \sigma(&\gamma(x_3) &, x_3)\col{)} \\ \col{\sigma(}\sigma( &\gamma(x_2)&,\alpha) \col{,} &\ \sigma(&x_2 &, x_3)\col{)} \end{array}\right)\right\}\\ % \overset{\text{Dek.}}{\Longrightarrow}\quad % &\left\{\left(\begin{array}{lcr} \col{\sigma(} & x_1 & \col{,} \alpha\col{)} \\ \col{\sigma(} & \gamma(x_2) & \col{,} \alpha\col{)} \end{array}\right), \left(\begin{array}{lcr} \col{\sigma(}& \gamma(x_3) & \col{,} x_3)\col{)} \\ \col{\sigma(}& x_2 & \col{,} x_3)\col{)} \end{array}\right)\right\} \\ \overset{\text{Dek.}}{\Longrightarrow^2} \quad % &\left\{ \begin{pmatrix} x_1 \\ \gamma(x_2) \end{pmatrix} , \begin{pmatrix} \alpha \\ \alpha \end{pmatrix} , \begin{pmatrix} \gamma(x_3) \\ x_2 \end{pmatrix} , \col{\begin{pmatrix} x_3 \\ x_3 \end{pmatrix}} \right\} \\ \overset{\text{El.}}{\Longrightarrow} \quad % &\left\{ \begin{pmatrix} x_1 \\ \gamma(x_2) \end{pmatrix} , \col{\begin{pmatrix} \alpha \\ \alpha \end{pmatrix}} , \begin{pmatrix} \gamma(x_3) \\ x_2 \end{pmatrix} \right\} \\ \overset{\text{Dek.}}{\Longrightarrow} \quad % &\left\{ \begin{pmatrix} x_1 \\ \gamma(x_2) \end{pmatrix} , \col{\begin{pmatrix} \gamma(x_3) \\ x_2 \end{pmatrix}} \right\} \\ \overset{\text{Vert.}}{\Longrightarrow} \quad % &\left\{ \begin{pmatrix} x_1 \\ \gamma(\col{x_2}) \end{pmatrix} , \begin{pmatrix} \col{x_2} \\ \gamma(x_3) \end{pmatrix} \right\} \quad ({\text{Occur check: } \textcolor{cdgray}{x_2 \text{ kommt nicht in } \gamma(x_3) \text{ vor}}})\\ % \overset{\text{Subst.}}{\Longrightarrow} \quad &\left\{ \begin{pmatrix} x_1 \\ \gamma(\gamma(x_3)) \end{pmatrix} , \begin{pmatrix} x_2 \\ \gamma(x_3) \end{pmatrix} \right\} \end{align*} allgemeinster Unifikator: \begin{align*} x_1 &\mapsto \gamma(\gamma(x_3)) \\ x_2 &\mapsto \gamma(x_3) \\ x_3 &\mapsto x_3 \end{align*}
    • Teil (b): Zwei weitere Unifikatoren finden wir durch die konkrete Belegung der "freien" Variable \(x_3\): \begin{align*} x_1 &\mapsto \gamma(\gamma(\alpha)) & x_1 &\mapsto \gamma(\gamma(\gamma(\alpha))) \\ x_2 &\mapsto \gamma(\alpha) & x_2 &\mapsto \gamma(\gamma(\alpha)) \\ x_3 &\mapsto \alpha & x_3 &\mapsto \gamma(\alpha) \end{align*}
    • Teil (c): Der Occur check schlägt für die Terme \( t_1 = x_1 \) und \( t_2 = \gamma(x_1) \) fehl, da \( x_1 \) in \( t_2 = \gamma(x_1) \) vorkommt. Würden wir hier substituieren, liefen wir in eine Endlosrekursion.
    • Teil (d): Gegeben seien folgende Typausdrücke: \begin{align*} t_1 &= \texttt{(a , [a])} \\ t_2 &= \texttt{(Int , [Double])} \\ t_3 &= \texttt{(b , c)} \end{align*}
      • \(t_1\) und \(t_2\) sind nicht unifizierbar
      • \(t_2\) und \(t_3\) sind unifizierbar mit \(\texttt{b} \mapsto \texttt{Int}\), \(\texttt{c} \mapsto \texttt{[Double]}\)
      • \(t_1\) und \(t_3\) sind unifizierbar mit \(\texttt{a} \mapsto \texttt{a}\), \(\texttt{b} \mapsto \texttt{a}\), \(\texttt{c} \mapsto \texttt{[a]}\)
Woche 5: Beweis von Programmeigenschaften
10.05. bis 14.05.2021
Woche 6: \(\lambda\)-Kalkül
17.05. bis 21.05.2021
Woche 7: \(\lambda\)-Kalkül
31.05. bis 04.06.2021
Woche 8: Logikprogrammierung
07.06. bis 11.06.2021
  • Im Zeitraum vom 31.05. bis zum 20.06.2021 finden die Lehrveranstaltungsevaluationen statt. Ich würde mich sehr freuen, wenn ihr daran teilnehmt und die Übungen bewertet - gern auch mit Freitextkommentaren zu positiven und verbesserungswürdigen Aspekten. Alle Antworten sind anonym.

  • Vorlesungsvideo
  • Übungsblatt 8
  • Videoaufzeichnung der Übung (Mittwoch)
  • Hinweis: Die Zeilenangaben in den SLD-Refutationen können sich zwischen den Mitschriften und Slides unterscheiden, sollten aber in jedem Fall konsistent sein. Grund dafür sind Leerzeilen in der Originaldatei. Die unten stehenden Lösungen orientieren sich an den Slides.

  • Lösungen - Aufgabe 1
    1. Abbildung der Kantenrelation des gegebenen Graphen durch ein Prädikat edge

      edge(1, 4).
      edge(1, 2).
      edge(3, 2).
      edge(4, 3).
      edge(1, 1).
    2. Pfade als zweistelliges Prädikt path

      path(U, U).
      path(U, W) :- edge(U, V), path(V, W).
    3. SLD-Refutationen für das Goal ?- path(4, X).

                 ?- path(4,X).
      { X = 4 }  ?- .                          % 7 
                 ?- path(4,X).
      ?- edge(4,W), path(W,X).     % 8
      { W = 3 }  ?- path(3,X).                % 5
      { X = 3 }  ?- .                         % 6 
                 ?- path(4,X).
      ?- edge(4,W), path(W,X).     % 8 
      { W = 3 }  ?- path(3,X).                % 5
      ?- edge(3,U), path(U,X).     % 8 
      { U = 2 }  ?- path(2,X).                % 4
      { X = 2 }  ?- .                         % 7 

      Damit ist also \( X \in \{ 2,3,4 \} \).

    Lösungen - Aufgabe 2
    1. Prädikat even, das alle geraden Zahlen enthält

      even(0).
      even(s(s(N))) :- even(N).
    2. Prädikt div2, dass alle Paare \( ( n, \lfloor \frac n 2 \rfloor ) \) enthält

      div2(0, 0).
      div2(s(0), 0).
      div2(s(s(N)), s(M)) :- div2(N, M).
    3. SLD-Refutation für das Goal ?- div2(<3>, <1>).

      ?- div2(<3>, <1>).
      ?- div2(<1>, 0)           % 12
      ?- .                      % 11 
    4. Zusatz: Prädikat div, dass alle Tripel \( (n, m, \lfloor \frac n m \rfloor ) \) enthält

      lt(0, s(M)) :- nat(M).
      lt(s(N), s(M)) :- lt(N, M).
      
      div(0, M, 0) :- lt(0, M).
      div(N, M, 0) :- lt(N, M).
      div(N, M, s(Q)) :- lt(0, M), sum(M, V, N), div(V, M, Q).
    5. Zusatz: SLD-Refutation für das Goal ?- div(<3>,<2>,<1>): siehe Slides

Woche 9: Logikprogrammierung
14.06. bis 18.06.2021
  • Im Zeitraum vom 31.05. bis zum 20.06.2021 finden die Lehrveranstaltungsevaluationen statt. Ich würde mich sehr freuen, wenn ihr daran teilnehmt und die Übungen bewertet - gern auch mit Freitextkommentaren zu positiven und verbesserungswürdigen Aspekten. Alle Antworten sind anonym.

  • Vorlesungsvideo
  • Übungsblatt 9
  • Videoaufzeichnung der Übung (Dienstag)
    • Mitschriften vom Dienstag und Mittwoch
    • In den Slides hatte ich nur Dinge unterstrichen, deswegen habe ich sie diesmal nicht mit hochgeladen.

    Hinweis: Die Zeilenangaben in den SLD-Refutationen können sich zwischen den Mitschriften und Slides unterscheiden, sollten aber in jedem Fall konsistent sein. Grund dafür sind Leerzeilen in der Originaldatei. Die unten stehenden Lösungen orientieren sich an den Slides.

  • Lösungen - Aufgabe 1
    1. Prüfen der Teillisteneigenschaft durch ein Prädikat sublist

      nat (0).
      nat(s(X)) :- nat(X).
      
      listnat ([]).
      listnat ([X|XS]) :- nat(X), listnat(XS).
      
      prefix([]    , Ys )    :- listnat(Ys).
      prefix([X|Xs], [X|Ys]) :- nat(X), prefix(Xs, Ys).
      
      sublist(Xs   , [Y|Ys]) :- nat(Y), sublist(Xs, Ys).
      sublist(Xs   , Ys )    :- prefix(Xs, Ys).
    2. SLD-Refutationen für das Goal ?- sublist([<4>|XS], [<5>, <4>, <3>]).

                 ?-  sublist ([<4>|Xs], [<5>, <4>, <3>]).
      ?-  nat(<5>), sublist ([<4>|Xs], [<4>, <3>]). % 6
      ?-* nat(0), sublist ([<4>|Xs], [<4>, <3>]).   % 2
      ?-  sublist ([<4>|Xs], [<4>, <3>]).           % 1
      ?-  prefix ([<4>|Xs], [<4>, <3>]).            % 7
      ?-  nat(<4>), prefix(Xs , [<3>]).             % 10
      ?-* nat(0), prefix(Xs , [<3>]).               % 2
      ?-  prefix(Xs , [<3>]).                       % 1
      {Xs = []}  ?-  listnat ([<3>]).                          % 9
      ?-  nat(<3>), listnat ([]).                   % 5
      ?-* nat(0), listnat ([]).                     % 2
      ?-  listnat ([]).                             % 1
      ?-  .                                         % 4
                      ?-  sublist ([<4>|Xs], [<5>, <4>, <3>]).
      ?-  nat(<5>), sublist ([<4>|Xs], [<4>, <3>]). 
      										% 6
      ?-* nat(0), sublist ([<4>|Xs], [<4>, <3>]).  
      										% 2
      ?-  sublist ([<4>|Xs], [<4>, <3>]).      % 1
      ?-  prefix ([<4>|Xs], [<4>, <3>]).       % 7
      ?-  nat(<4>), prefix(Xs , [<3>]).        % 10
      ?-* nat(0), prefix(Xs , [<3>]).          % 2
      ?-  prefix(Xs , [<3>]).                  % 1
      {Xs=[<3>|Xs1]}  ?-  nat(<3>), prefix(Xs1 , []).          % 10
      ?-* nat(0), prefix(Xs1 , []).            % 2
      ?-  prefix(Xs1 , []).                    % 1
      {Xs1 = []}      ?-  listnat ([]).                        % 9
      ?-  .                                    % 4
    Lösungen - Aufgabe 2
    1. Evaluierung eines binären Termbaums mit dem Prädikat eval

      sum(0, Y, Y) :- nat(Y).
      sum(s(X), Y, s(S)) :- sum(X, Y, S).
      
      eval( X         , X ) :-  nat(X).
      eval( plus (L,R), X ) :-  eval(L, LE), eval(R, RE), sum(LE, RE,  X).
      eval( minus(L,R), X ) :-  eval(L, LE), eval(R, RE), sum(RE,  X, LE).
    2. SLD-Refutation für das Goal ?- insert(<t1>, <t2>, X).

      Ausführlichere Hinweise zu Anschauung des Prädikats insert finden sich in den Slides.

      1.                            ?-  insert(<t1>, <t2>, X).
        {X = tree(a, LT1, RT1)}    ?-  insert(tree(b, nil, nil), <t2>, LT1), 
        			insert(tree(v, nil, nil), <t2>, RT1).   % 6
        {LT1 = tree(b, LT2, RT2)}  ?-  insert(nil , <t2>, LT2), 
        			insert(nil, <t2>, RT2), 
        			insert(tree(v, nil, nil), <t2>, RT1).   % 6
        {LT2 = nil, RT2 = nil}     ?-* insert(tree(v, nil, nil), <t2>, RT1).   % 4
        {RT1 = <t2>}               ?-  istree(<t2>).                           % 5
        		?-* istree(nil), istree(nil), istree(nil).  % 2
        		?-* .                                       % 4
      2.                            ?-  insert(<t1>, <t2>, X).
        {X = tree(a, LT1, RT1)}    ?-  insert(tree(b, nil, nil), <t2>, LT1), 
        			insert(tree(v, nil, nil), <t2>, RT1).   % 6
        {LT1 = tree(b, LT2, RT2)}  ?-  insert(nil , <t2>, LT2), 
        			insert(nil, <t2>, RT2), 
        			insert(tree(v, nil, nil), <t2>, RT1).   % 6
        {LT2 = nil, RT2 = nil}     ?-* insert(tree(v, nil, nil), <t2>, RT1).   % 4
        {RT1 = tree(v, LT3, RT3)}  ?-  insert(nil, <t2>, LT3),
        			insert(nil, <t2>, RT3).                 % 6
        {RT3 = nil, LT3 = nil}     ?-* .                                       % 4
Woche 10: Abstrakte Maschine AM0
21.06. bis 25.06.2021
Woche 11: Abstrakte Maschine AM1
28.06. bis 02.07.2021
Woche 12: Hoare-Kalkül
05.07. bis 09.07.2021
Woche 13: H0 - ein einfacher Kern von Haskell
12.07. bis 16.07.2021
Woche 14: Wiederholung
19.07. bis 23.07.2021
  • In dieser Woche gibt es (vo­r­aus­sicht­lich) kein Vorlesungsvideo mehr.
  • Übungsblatt 14
  • Da wir in Break-Out-Rooms gearbeitet haben, gibt es zu dieser Übung keine Aufzeichnung. Bei Fragen könnt ihr die Musterlösungen des Lehrstuhls oder natürlich mich konsultieren.

  • Musterlösungen vom Lehrstuhl
Klausur
16.08.2021 ab 900 Uhr
  • Die nachfolgenden Informationen sind dem Prüfungskurs auf OPALExam@TUD entnommen. Ich übernehme keinerlei Garantie für die Angaben - verbindlich sind die Informationen des verantwortlichen Prüfers.

  • Die Probeklausur fand am 02.08.2021 statt. Die Aufgaben und Musterlösungen dazu finden sich im OPAL-Kurs, auch wenn die Probeklausur eher als technischer Test gedacht war. Insbesondere findet am 09.08.2021 keine Probeklausur mehr statt - solltet ihr diese Fehlinformation erhalten haben, dann lasst euch gesagt sein, dass ihr nichts verpasst habt.

  • Die Klausur findet am 16.08.2021 von 920 Uhr bis 1030 Uhr statt; die Bearbeitungszeit beträgt also 70 min.

  • Auch diese Prüfung wird online über OpalExam@TUD durchgeführt, stellt sicher, dass ihr euch einmal inital dort eingeloggt habt.

    • Loggt euch bereits einige Zeit vor Beginn der Klausur in OpalExam@TUD ein, ich empfehle ab 900 Uhr bereit zum Arbeiten zu sein.

    • Im Prüfungskurs auf OpalExam@TUD findet ihr entsprechende Hinweise und einen Link zu eurem BigBlueButton-Raum. Dort werden wichtige Ansagen der Aufsichtspersonen zu finden sein und ihr könnt bei Fragen und Probleme an die Aufsicht herantreten. Wundert euch nicht, wenn ihr keine weiteren Personen in dem Raum seht - euch sind alle Rechte in der Konferenz genommen worden und ihr könnt somit nur noch eine Privatnachricht an die Aufsichtsperson schreiben.

    • Der Klausurbaustein sollte am Tag der Klausur sichtbar sein und ab 910 Uhr solltet ihr auch auf den Start-Button zugreifen können. Sollte dieser nach diesem Zeitpunkt nicht erscheinen, aktualisiert die Seite im Browser (Taste F5).

    • Drückt den Start-Button zwischen 910 Uhr und 920 Uhr. Damit gelangt ihr in einen virtuellen Warteraum bis zum Start der Klausur. Schließt diesen Warteraum bitte nicht! Der Zugang zu den Klausuren wird ab 920 Uhr (in Wellen) zentral durch die zuständigen Aufsichten freigegeben, dann beginnt die Bearbeitungszeit von 70 Minuten.

    • Seid ihr zu spät gekommen, dann meldet euch zunächst im BigBlueButton-Raum bei eurem Betreuer.

    • Bei Problemen, Absturz etc. kontaktiert sofort die Aufsicht im BigBlueButton-Raum (einzige sichtbare Person) via privater Textnachricht; wenn das nicht funktioniert (unterbrochene Internetverbindung o.Ä.), dann ruft unter der im Prüfungskurs auf OpalExam@TUD angegebenen Telefonnummer an. Wenn ihr schon Eingaben getätigt habt, dann wartet nach einem Abbruch mindestens 3 Minuten, bevor ihr den Browser neu startet, zurück zum Test navigiert und auf den Start-Knopf drückt. Damit wird sichergestellt, dass eure eingegebenen Antworten vollständig an das System übertragen wurden.