Termination und Normalisierung

Für eine zweistellige Relation $\rho$ auf M

(zum Beispiel eine Ersetzungsrelation $\to_{R}^{}$ auf Term($\Sigma$))

• $\rho$ ist terminierend (stark normalisierend), falls es keine unendliche lange $\rho$-Folge gibt

  d. h. $\rho$(x₀, x₁),$\rho$(x₁, x₂),$\rho$(x₂, x₃),...

• $\rho$ is schwach normalisierend, falls zu jedem x₀ $\in$ M eine $\rho$-Folge zu einer $\rho$-Normalform führt

Beachte: es gibt $\rho$, die schwach, aber nicht stark normalisieren.

Beispiel (Wortersetzung): fgfg$\to$gfgffg (Alfons Geser, 2000)