Konstruktor-Systeme

Für TRS R über Signatur Σ: Symbol s∈Σ heißt

• definiert, wenn ∃(l, r)∈R : l[] = s
• sonst Konstruktor.

Das TRS R heißt Konstruktor-TRS, falls:

• die definierten Symbol kommen links nur in den Wurzeln vor (rechts egal)

Übung: diese Eigenschaft formal spezifizieren

Beispiele: R₁ = {a(b(x))→b(a(x))} über Σ₁ = {a/1, b/1},

R₂ = {f (f (x, y), z)→f (x, f (y, z)) über Σ₂ = {f /2}:

definierte Symbole? Konstruktoren? Konstruktor-System?

Funktionale Programme sind ähnlich zu Konstruktor-TRS.