Termersetzung ist
Für Anwendungen wichtig sind die Eigenschaften
- Termination (SN) (keine unendlich langen Rechnungen)
- Konfluenz (CR,UNR) (eindeutige Ergebnisse)
- Ableitungskomplexität (Länge von Rechnungen
als Funktion der Startgröße)
das ist aber alles unentscheidbar (wg. Turing-Vollst.)