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

Lehrveranstaltungen:

• • Algebra des Programmierens
    (Vorlesung mit Übung, 4 SWS, Henning Urbat et al., Mi, 16:15 - 17:45, 01.255-128; Do, 14:15 - 15:45, 01.255-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:

Fachkompetenz

Wissen

Die Studierenden geben elementare Definitionen und Fakten zu induktiven Datentypen, zustandsbasierten Systemen und grundlegenden kategoriellen Begriffen wieder

Verstehen

Die Studierenden

• erklären grundlegende Begriffe und Konzepte der Kategorientheorie

• beschreiben Beispiele dieser Begriffe und Konzepte

• erläutern grundlegende kategorielle Ergebnisse und deren Beweise

Anwenden

Die Studierenden

• wenden strukturelle Induktionsprinzipien (Definitions- und Beweisprinzip) auf Programmierbeispiele an

• wenden strukturelle Koinduktionsprinzipien (Definitions- und Beweisprinzip) auf festgelegte Typen von zustandbasierten Systemen (Koalgebren) an

• übertragen kategorielle Begriffe auf verschiedene Spezialfälle der Informatik (abstrakte Datentypen und verschiedene Arten von Automaten)

Analysieren

Die Studierenden analysieren kategorielle Beweise, diskutieren die entsprechenden Argumentationen und legen diese schriftlich klar nieder.

Erschaffen

Die Studierenden

• arbeiten strukturelle Induktions- und Koinduktionsprinzipien für neue Datentypen und zustandsbasierte Systeme als Spezialfall der Initiale-Algebra-Semantik und Terminale-Koalgebra-Semantik aus

• kreieren kategorielle Begriffe, die Konzepte von konkreten Datentypen und Systemen abstrahieren

Lern- bzw. Methodenkompetenz

Die Studierenden

• beherrschen das grundsätzliche Konzept des Beweises als hauptsächliche Methode des Erkenntnisgewinns in der theoretischen Informatik. Sie überblicken abstrakte Begriffsarchitekturen.

• vollziehen mathematische Argumentationen nach, erklären diese, führen diese selbst und legen sie schriftlich nieder

Sozialkompetenz

Die Studierenden lösen Probleme in kollaborativer Gruppenarbeit und präsentieren erarbeitete Lösungen.

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:

1. Informatik (Master of Science)
   (Po-Vers. 2010 | TechFak | Informatik (Master of Science) | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsrichtung Theoretische Informatik | Algebra des Programmierens)

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 %

Prüfungssprache: Deutsch und Englisch

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

1. Prüfer:

Stefan Milius