Funktionale Programme

...sind spezielle Term-Ersetzungssysteme. Beispiel:

Signatur: S einstellig, Z nullstellig, f zweistellig.

Ersetzungssystem {f (Z, y)→y, f (S(x), y)→S(f (x, y))}.

Startterm f (S(S(Z)), S(Z)).

entsprechendes funktionales Programm:

data N = S N | Z
f :: N -> N -> N
f a y = case a of
    Z   -> y
    S x -> S (f x y)

Aufruf: f (S (S Z)) (S Z)

Auswertung = Folge von Ersetzungsschritten →_R^*
Resultat = Normalform (hat keine →_R-Nachfolger)