Regelsysteme

• R eine Menge von Regeln (TRS, term rewriting system)

  definiert Relation →_R auf Term(Σ)

  (einmalige Anwendung irgendeiner Regel irgendwo):

  →_R : = {(t, s) | ∃(l, r)∈R, p∈Pos(t) : t→_{(l, r), p}s}

• jedes solche →_R definiert ein ARS
• ist nichtdeterministisches Berechnungsmodell

  Resultat = (→_R)-Normalform (kürzer: R-Normalform)

• Ausdrucksstärke stimmt mit Turing-Maschinen überein
  • Simulation einer TM M durch →_R⁺ für TRS R
  • Simulation von →_R durch TM