(zum Beispiel eine Ersetzungsrelation →R
auf
Term(Σ)
)
- ρ
ist terminierend (stark normalisierend),
falls es keine unendliche lange ρ
-Folge gibt
d. h.
ρ(x0, x1), ρ(x1, x2), ρ(x2, x3),…
- ρ
is schwach normalisierend,
falls zu jedem x0∈M
eine ρ
-Folge zu einer ρ
-Normalform führt
Beachte:
es gibt ρ
, die schwach, aber nicht stark normalisieren.
Johannes Waldmann
2015-12-11