17-Algebra des Programmierens previous clip next clip

Recording date 2019-01-29

Via

Passwort

Language

German

Faculty

Lehrstuhl für Informatik 8 (Theoretische Informatik)

Format

lecture

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.

Up next

Milius, Stefan
Prof. Dr. Stefan Milius
2019-02-05
Passwort

More clips in this category ' Computer Science'

2017-06-02
IdM-login
protected  
2019-04-20
Free
public  
2018-04-13
Free
public