Elaboration und Elimination in Typentheorie

Typkonzepte dienen dem Programmierer als konzeptionelle Hilfe, indem sie die Menge der Programme auf eine Teilmenge `sinnvoller' Programme einschränken. Es stellt sich die Frage, bis zu welchem Grad Typannotationen in Programmtexten ausgelassen werden können (Elimination), ohne die durch die Typisierung zugesicherten Eigenschaften zu verlieren. Dies ist zumindest dann möglich, wenn durch geeignete Inferenzprozesse die Typannotationen wieder hergestellt werden können (Elaboration).

Moderne Typentheorien wie der Konstruktionskalkül erlauben mit ihrem starken Typkonzept eine wesentlich allgemeinere Spezifikation von Programmeigenschaften als die Typsysteme heute üblicher Programmiersprachen. In dem Vortrag werden verschiedene Elaborationsmechanismen für Sprachen mit solch starken Typkonzepten vorgestellt und sinnvolle Kombinationsmöglichkeiten untersucht. Im Gegensatz zu den bekannten entscheidbaren Mechanismen für relativ schwache Typsysteme, wie etwa die Typrekonstruktion in ML, entstehen bei der Elaboration in dieser allgemeinen Form nichttriviale Entscheidbarkeitsprobleme.

Es wird eine Softwarearchitektur für interaktive Spezifikationssysteme vorgeschlagen, die sich aus der Kombination von (partieller) Elaboration und dem inversen Prozess der (partiellen) Elimination ergibt. Erfüllen die beiden Abbildungen gewisse Anforderungen, so ist eine korrekte logische Interpretation der Spezifikationssprache auf Basis der zugrundeliegenden Typentheorie sichergestellt.

Das Spezifikations- und Verifikationswerkzeug Typelab wurde gemäß dieser modularen Architektur realisiert. Dabei hat sich gezeigt, dass durch die Trennung von Systemkern und Spezifikationssprache konzeptionelle Fehler vergleichbarer Systeme vermieden werden konnten.