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 = Z | S N 
f :: N -> N -> N
f x y = case x 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)