Verfeinerung (Informatik)
# Verfeinerung (Informatik)

Unter Verfeinerung versteht man in der Informatik ein Verfahren, bei dem aus einer abstrakten Beschreibung (z. B. Registermaschine, formale Spezifikation mittels Z-Notation) eine konkretere Beschreibung abgeleitet wird. Eine Verfeinerung erhält dabei in der konkreten Beschreibung (bestimmte) Eigenschaften der abstrakten Beschreibung.

## Verfeinerung bei Registermaschinen

Unter der Verfeinerung versteht man in der theoretischen Informatik ein Verfahren, aus verallgemeinerten Registermaschinen korrekte, einfache Registermaschinen zu konstruieren.

### Einfache Registermaschine

Die einfache Registermaschine kennt nur die Befehle

    ${\mbox{Register}}_{k}:={\mbox{Register}}_{k}+1$,
    ${\mbox{Register}}_{k}:={\mbox{Register}}_{k}{\dot {-}}1$

und den Test

    ${\mbox{Register}}_{k}=0?$,

wobei

    $x{\dot {-}}1={\begin{cases}x-1,&{\mbox{wenn}}\,x>0\ \\0,&{\mbox{sonst}}\end{cases}}$

die arithmetische Differenz ist.

Durch diese Definition der Subtraktion erreicht man, dass man innerhalb der natürlichen Zahlen bleibt.

### Registermaschinen für weitere Funktionen

Hat man nun eine Registermaschine geschrieben, die in der Lage ist, beispielsweise zwei Zahlen a und b zu addieren, dann kann man künftig in jeder Registermaschine unmittelbar zwei Register addieren: Man könnte an stelle dieser unmittelbaren Addition auch die Registermaschine für die Addition zweier Zahlen a und b einsetzen.

Diesen Schritt nennt man Verfeinerung.

Eine Registermaschine, die noch verfeinert werden muss, nennt man verallgemeinerte Registermaschine.

### Bedeutung

Durch die Verfeinerung wird es einfacher, zu einer Funktion eine übersichtliche, lesbare und kurze Registermaschine anzugeben. Ein Beispiel zeigt der Beweis der Berechenbarkeit der Cantorschen Paarungsfunktion.

