Algebra des Programmierens (AlgProg)7.5 ECTS
(englische Bezeichnung: Algebra of Programming)

Lehrveranstaltungen:

• • Algebra des Programmierens
    (Vorlesung mit Übung, 4 SWS, Stefan Milius, Di, 12:15 - 13:45, 01.150-128; Mi, 10:15 - 11:45, 00.131-128)

Inhalt:

Induktive Datentypen wie z.B. Listen, Stacks und Bäume werden abstrakt beschrieben.

Strukturelle Induktion und Rekursion für solche Datentypen (z.B. die fold-Operation auf Listen) werden auf Grundlage der Initiale-Algebra-Semantik entwickelt. Dadurch werden verschiedene effektive Programmiertricks auf eine solide mathematische Grundlage gestellt.

Grundlagen und Methoden der Kategorientheorie werden eingeführt und erklärt, insbesondere initiale Algebren und ihre Konstruktion.

Evtl. werden Koalgebren behandelt, die es ermöglichen, verschiedene zustandsbasierte Systeme und ihre Semantik in einer einheitlichen Theorie zu studieren.

Lernziele und Kompetenzen:

Die Studierenden erklären induktive Datentypen und die entsprechenden strukturellen Induktionsprinzipien (Defitions- und Beweisprinzip) und wenden diese in Programmierbeispielen an. Sie leiten ferner solche Prinzipien für neue induktive Datentypen her und stellen sie als Spezialfall der Initiale-Algebra-Semantik dar.

Die Studierenden erläutern grundlegende Begriffe der Kategorientheorie und wenden die behandelten Begriffe und Methoden auf verschiedene Spezialfälle in der Informatik an (abstrakte Datentypen, zustandsbasierte Systeme). Sie formulieren die Semantik von induktiven Programmen und zustandsbasierten Systemen mit Hilfe von (Ko)Algebren formulieren.

Die Studierenden erlangen die Fähigkeit kategorientheoretische Beweise zu führen und die entsprechenden Argumente klar schriftlich niederzulegen.

Literatur:

• R. Bird and O. de Moor: Algebra of Programming, Prentice Hall, 1996.

• J. Adamek, H. Herrlich and G.E. Strecker: Abstract and Concrete Categories: The Joy of Cats, 2nd edition, Dover Publishers, 2009.

Weitere Informationen:

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:

1. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2010 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Vertiefung Informatik I und II | Vertiefungsmodul Theoretische Informatik)
2. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2013 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Vertiefung Informatik I und II | Vertiefungsmodul Theoretische Informatik)
3. Informatik (Bachelor of Science)
   (Po-Vers. 2009s | TechFak | Informatik (Bachelor of Science) | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsrichtung Theoretische Informatik)
4. Informatik (Bachelor of Science)
   (Po-Vers. 2009w | TechFak | Informatik (Bachelor of Science) | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsrichtung Theoretische Informatik)
5. Informatik (Master of Science)
   (Po-Vers. 2010 | TechFak | Informatik (Master of Science) | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsrichtung Theoretische Informatik)
6. Mathematik (Bachelor of Science)
   (Po-Vers. 2015w | NatFak | Mathematik (Bachelor of Science) | Module des Nebenfachs | Nebenfach Informatik | Vertiefungsmodule | Vertiefungsrichtung Theoretische Informatik)

Studien-/Prüfungsleistungen:

Algebra des Programmierens (Vorlesung mit Übung) (Prüfungsnummer: 861501)

Prüfungsleistung, mündliche Prüfung, Dauer (in Minuten): 30, benotet

Anteil an der Berechnung der Modulnote: 100.0 %

weitere Erläuterungen:
In die Note der mündliche Prüfung gehen auch die Übungsleistungen ein.

Erstablegung: WS 2018/2019, 1. Wdh.: SS 2019 (nur für Wiederholer)

1. Prüfer:

Lutz Schröder