Algebra des Programmierens

Ziel: solide und flexible mathematische Grundlagen für effektive Programmierung und System-SemantikMethode: die kategorielle Sichtweise
  • Funktoren zur Beschreibung induktiver Datentypen (Listen, Stacks, Bäume usw.);
    Strukturelle Induktion und Rekursion mittels Initialer-Algebra-Semantik
  • Funktoren zur Beschreibung von Automaten und Transitionssystemen als Koalgebren;
    Bisimulation und System-Verhalten mittels Finaler-Koalgebra-Semantik

Inhalt

  • Induktive Datentypen wie z.B. Listen, Stacks und Bäume werden abstrakt beschrieben.
  • Strukturelle Induktion für solche Datentypen (z.B. fold-Operation auf Listen) wird als Spezialfall von Initialer Algebra Semantik verstanden.
    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.

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.
    Freie Online-Version
  • S. Awodey: Category Theory, 2nd edition, Oxford University Press, 2010.