WS 2003/04: Theorie der Programmierung I + II

Termine

Vorlesung	Di 12:15 - 13:45	H-C 3310
	Mi 14:15 - 15:45	H-F 104/5
Erste Vorlesung	Di 14. 10. 2003
Übung	Mi 12:15 - 13:45	H-F 104/5
		H-C 6336/37 (nur TP I)
Erste Übung	Mi 22. 10. 2003

Aufteilung

Teil I der Vorlesung endet kurz vor Weihnachten, Teil II schließt sich unmittelbar an.

Prüfungen

Hier finden Sie einen Leitfaden zur Prüfungsvorbereitung (für TP I): pdf ps ps.gz

Zur Vereinbarung eines Prüfungstermins können Sie mir eine e-mail schicken und/oder persönlich vorbeikommen.

Übungsblätter

Übung 1	dvi	pdf	ps	ps.gz
Übung 2	dvi	pdf	ps	ps.gz
Übung 3	dvi	pdf	ps	ps.gz
Übung 4	dvi	pdf	ps	ps.gz
Übung 5	dvi	pdf	ps	ps.gz
Übung 6	dvi	pdf	ps	ps.gz
Übung 7	dvi	pdf	ps	ps.gz
Übung 8	dvi	pdf	ps	ps.gz
Übung 9	dvi	pdf	ps	ps.gz
Übung 10 (korrigierte Version)	dvi	pdf	ps	ps.gz
Übung 11	dvi	pdf	ps	ps.gz
Übung 12	dvi	pdf	ps	ps.gz

Materialien zur Vorlesung

Allgemeines:

KFG und Typregeln	dvi	pdf	ps	ps.gz
Small step Regeln	dvi	pdf	ps	ps.gz
Abgeleitete small step Regeln	dvi	pdf	ps	ps.gz
Big step Regeln	dvi	pdf	ps	ps.gz
Abgeleitete big step Regeln	dvi	pdf	ps	ps.gz
Rekursion und Listen	dvi	pdf	ps	ps.gz
Kalkül	dvi	pdf	ps	ps.gz

Beispiele zur Typüberprüfung:

Absolutbetrag	dvi	pdf	ps	ps.gz
sum_of_squares (mit Paaren)	dvi	pdf	ps	ps.gz
sum_of_squares (curryfiziert)	dvi	pdf	ps	ps.gz
twice	dvi	pdf	ps	ps.gz
Übung 2, Aufgabe 2	dvi	pdf	ps	ps.gz
Übung 3, Aufgabe 1 a	dvi	pdf	ps	ps.gz
Übung 3, Aufgabe 1 b	dvi	pdf	ps	ps.gz
Übung 3, Aufgabe 1 d	dvi	pdf	ps	ps.gz
Übung 3, Aufgabe 1 e	dvi	pdf	ps	ps.gz
Übung 3, Aufgabe 1 f	dvi	pdf	ps	ps.gz
Übung 3, Aufgabe 2	dvi	pdf	ps	ps.gz
Übung 3, Aufgabe 3	dvi	pdf	ps	ps.gz
Fakultätsfunktion	dvi	pdf	ps	ps.gz
ggT (mit Paaren)	dvi	pdf	ps	ps.gz
ggT (curryfiziert)	dvi	pdf	ps	ps.gz
even und odd	dvi	pdf	ps	ps.gz
Übung 12, Aufgabe 1	dvi	pdf	ps	ps.gz
Übung 12, Aufgaben 2 und 3	dvi	pdf	ps	ps.gz

Beispiele zur small step Semantik:

Absolutbetrag	dvi	pdf	ps	ps.gz
square	dvi	pdf	ps	ps.gz
sum_of_squares (mit Paaren)	dvi	pdf	ps	ps.gz
sum_of_squares (curryfiziert)	dvi	pdf	ps	ps.gz
twice	dvi	pdf	ps	ps.gz
twice (besser lesbar)	dvi	pdf	ps	ps.gz
Übung 4, Aufgabe 3	dvi	pdf	ps	ps.gz
Fakultätsfunktion	dvi	pdf	ps	ps.gz
ggT	dvi	pdf	ps	ps.gz
even und odd	dvi	pdf	ps	ps.gz

Beispiele zur big step Semantik:

Absolutbetrag	dvi	pdf	ps	ps.gz
square	dvi	pdf	ps	ps.gz
sum_of_squares (mit Paaren)	dvi	pdf	ps	ps.gz
sum_of_squares (curryfiziert)	dvi	pdf	ps	ps.gz
twice	dvi	pdf	ps	ps.gz
twice (besser lesbar)	dvi	pdf	ps	ps.gz
Übung 6, Aufgabe 1	dvi	pdf	ps	ps.gz
Fakultätsfunktion	dvi	pdf	ps	ps.gz
even und odd	dvi	pdf	ps	ps.gz

Praxis

Wer die "Theorie der Programmierung" durch etwas "Praxis der Programmierung" ergänzen möchte, kann sich SML/NJ (= "Standard ML of New Jersey") besorgen. Das ist die real existierende Programmiersprache, an die sich die in der Vorlesung definierte Sprache anlehnt. Alle nötigen Informationen dazu gibt's auf der SML/NJ-Homepage

Literatur

1. Benjamin Pierce: Types and Programming Languages, MIT Press, 2002

In diesem Buch werden (nur) small-step Semantik und Typsysteme behandelt. Dabei wird in Teil II (Kapitel 8-14) etwa die gleiche Programmiersprache abgedeckt, die wir auch in der Vorlesung betrachten, und es werden ähnliche Resultate (z.B. Typsicherheit) für diese Sprache bewiesen. Insgesamt ist das Buch sehr als Vorlesungsbegleitung zu empfehlen.

2. Glynn Winskel: The Formal Semantics of Programming Languages, MIT Press, 1993

In Kapitel 2,5 und 6 des Buches werden operationelle, denotationelle und axiomatische Semantik für eine einfache imperative Sprache behandelt, in Kapitel 9, 10 und 11 werden Typsysteme, operationelle und denotationelle Semantik für funktionale Sprachen betrachtet. Der Schwerpunkt bei der operationellen Semantik liegt auf big-step, small-step kommt nur am Rande vor (Absatz 2.6).

3. Robin Milner, Mads Tofte and Robert Harper: The Definition of Standard ML, MIT Press 1990

In diesem Buch wird die funktionale Programmiersprache "Standard ML" (an die sich die in der Vorlesung definierte Sprache anlehnt) formal definiert, d.h.
- die Syntax (= kontextfreie Syntax) in Kapitel 1 und 2
- die statische Semantik (= Typregeln) in Kapitel 3 und 4
- die dynamische Semantik (= big step Semantik) in Kapitel 5 und 6
Man kann hier einmal sehen, wie die Techniken, die wir in der Vorlesung erlernen, auf eine echte Programmiersprache angewendet werden. Das ist natürlich sehr aufwendig.

4. Robin Milner and Mads Tofte: Commentary on Standard ML, MIT Press, 1991

Hier werden Erläuterungen zu 3. gegeben und es werden einige Sätze über die Semantik bewiesen.

5. Larry C. Paulson: ML for the working programmer

Sehr zu empfehlen für jeden, der in ML programmieren oder auch nur etwas mehr Gefühl für's funktionale Programmieren bekommen möchte (was ja für die Vorlesung nicht schaden kann!). Natürlich gibt's noch viele andere Bücher zum gleichen Thema.

Kurt Sieber