Herleitungen als Programme: Ihre Kompilation und Interpretation

Zusammenfassung

Die Einsicht, daß Herleitungen, also formalisierte Beweise, als Programme verwendet werden können, ist nicht neu: Erste Hinweise darauf sind bereits 1945 in einem Artikel von Kleene [3] zu finden. Die grundlegende Idee des Programmierens mit Herleitungen beruht auf der Tatsache, daß aus einer konstruktiven Herleitung D einer Existenzaussage ∃y B in effektiver Weise ein Term t extrahiert werden kann, der als „Zeuge“ die Richtigkeit dieser Existenzaussage belegt:

$$D: \vdash \exists yB(y) \Rightarrow {\exists _{{\text{eff(}}D{\text{)}}}}{\text{Term }}t \vdash B(t).$$

(1)

Um diesen Sachverhalt für die Programmierung nutzbar zu machen, ist es zweckmäßig, die Formel B in (1) als Beschreibung der Beziehung zwischen Eingabe x und Ausgabe y eines gewünschten Programmes zu interpretieren. Der Vorgang des Programmierens besteht dann darin, eine Herleitung D der Formel ∀x∃yB(x, y) zu konstruieren. Diese Herleitung kann nun als Programm für beliebige Eingabewerte e ausgewertet werden. Dazu wird D zunächst in naheliegender Weise auf eine Herleitung D _e der Formel ∃y B(r, y) spezialisiert. Anschließend wird aus D _e mit dem Verfahren von (1) ein Term t_e extrahiert, so daß auch die Formel B(e, t _e ) herleitbar ist. Der Wert von t _e ist dann der gesuchte Ausgabewert.