Verfeinerung (Informatik)

Grundidee und Zweck

Verfeinerung ist in der Informatik ein Verfahren, bei dem aus einer abstrakten Beschreibung eine konkretere Beschreibung abgeleitet wird. Abstrakte Beschreibungen können beispielsweise eine Registermaschine oder eine formale Spezifikation mittels Z-Notation sein. Die konkrete Beschreibung erhält dabei bestimmte Eigenschaften der abstrakten Beschreibung.

In der theoretischen Informatik dient Verfeinerung insbesondere dazu, aus verallgemeinerten Registermaschinen korrekte, einfache Registermaschinen zu konstruieren. Dadurch lassen sich Programme für Registermaschinen zunächst mit verständlichen, leistungsfähigeren Operationen beschreiben und anschließend auf die wenigen erlaubten Grundbefehle zurückführen.

Grundbefehle der einfachen Registermaschine

Eine einfache Registermaschine besitzt nur drei grundlegende Möglichkeiten:

• Erhöhung eines Registers um 1: Register_k := Register_k + 1.
• Verminderung eines Registers um 1: Register_k := Register_k ∸ 1.
• Prüfung, ob ein Register den Wert 0 hat: Register_k = 0?

Dabei bezeichnet ∸ die arithmetische Differenz. Sie ist definiert durch

x ∸ 1 = x − 1, wenn x > 0, und x ∸ 1 = 0 sonst.

Ein Register mit dem Wert 0 wird durch die Verminderung also nicht negativ. Diese besondere Definition der Subtraktion stellt sicher, dass alle Registerwerte innerhalb der natürlichen Zahlen bleiben.

Ersetzen verallgemeinerter Befehle

Wurde bereits eine Registermaschine entwickelt, die eine bestimmte Funktion ausführt, kann diese Funktion später wie ein unmittelbarer Befehl verwendet werden. Beherrscht eine Maschine beispielsweise die Addition zweier Zahlen a und b, darf man bei der Beschreibung einer weiteren Registermaschine direkt die Addition zweier Register angeben.

Eine solche unmittelbare Addition gehört zwar nicht zu den elementaren Befehlen der einfachen Registermaschine. Sie kann jedoch durch die schon vorhandene Registermaschine zur Addition von a und b ersetzt werden. Genau dieses Ersetzen eines verallgemeinerten Befehls durch eine entsprechende Folge einfacher Befehle heißt Verfeinerung.

Eine Registermaschine, die solche noch zu ersetzenden Operationen enthält und deshalb weiter verfeinert werden muss, heißt verallgemeinerte Registermaschine.

Bedeutung für Konstruktion und Beweise

Verfeinerung erleichtert es, für eine Funktion eine übersichtliche, lesbare und kurze Registermaschine anzugeben. Komplexere Teilfunktionen können zunächst als bereits verfügbare Operationen behandelt werden. Danach werden sie durch passende einfache Registermaschinen ersetzt, sodass am Ende eine korrekte Maschine entsteht, die nur die erlaubten Grundbefehle verwendet.

Als Beispiel nennt der Artikel den Beweis der Berechenbarkeit der Cantorschen Paarungsfunktion. Dort hilft die Verfeinerung dabei, die Registermaschine verständlich zu beschreiben, ohne von Anfang an jeden einzelnen elementaren Schritt ausschreiben zu müssen.