Funktionale Programmiersprachen

Zusammenfassung

Im vorherigen Kapitel diente der λ-Kalkül, angereichert um einige Basisfunktionen und -prädikate, als Metasprache zur Formalisierung der Semantik imperativer Programmiersprachen. Der gleiche Kalkül, sogar mit weniger Basisfunktionen, eignet sich auch sehr gut, ein gewünschtes Ein-/Ausgabeverhalten direkt als Funktion zu beschreiben. Daher liegt es nahe, Programmiersprachen zu betrachten, deren Sprachelemente die des λ-Kalküls oder der verwandten kombinatorischen Logik sind. Bei solchen Sprachen ist die Metasprache der imperativen Sprachen zur Objektsprache geworden, und damit besteht die Spezifikation der Semantik nur noch aus der Angabe der semantischen Bereiche und der Interpretation der Funktions- und Prädikatssymbole. Ein funktionales Programm besteht dann aus einem Ausdruck A, der selbst das von ihm definierte Objekt bezeichnet, d.h. die Semantikfunktion wird durch die Gleichung

$$[\kern-0.15em[ A ]\kern-0.15em] \,{\text{ = }}\,A$$

bestimmt. Damit lassen sich Aussagen über Programmeigenschaften wesentlich kürzer beweisen.