Termersetzungssysteme als Programme

• to_R beschreibt einen Schritt der Rechnung von R,
• transitive Hülle →_R^* beschreibt Folge von Schritten.
• Resultat einer Rechnung ist Term in R-Normalform (= ohne →_R-Nachfolger)

dieses Berechnungsmodell ist im allgemeinen

• nichtdeterministisch R₁ = {C(x, y)→x, C(x, y)→y}

  (ein Term kann mehrere →_R-Nachfolger haben, ein Term kann mehrere Normalformen erreichen)

• nicht terminierend R₂ = {p(x, y)→p(y, x)}

  (es gibt eine unendliche Folge von →_R-Schritten, es kann Terme ohne Normalform geben)