Übung Terme, TRS

• Geben Sie die Signatur des Terms $\sqrt{{a\cdot a + b\cdot b}}$ an.
• Geben Sie ein Element t∈Term({f /1, g/3, c/0}) an mit t[1] = c().

mit ghci:

• data T = F T | G T T T | C deriving Show

  erzeugen Sie o.g. Terme (durch Konstruktoraufrufe)

Die Größe eines Terms t ist definiert durch

| f (t₁,…, t_k)| = 1 + $\sum_{{i=1}}^{k}$| t_i|.

• Bestimmen Sie |$\sqrt{{a\cdot a + b\cdot b}}$|.
• Beweisen Sie ∀Σ : ∀t∈Term(Σ) : | t| = | Pos(t)|.

Vervollständigen Sie die Definition der Tiefe von Termen:

k > 0 ⇒ depth(f (t₁,…, t_k)) = ...

• Bestimmen Sie depth($\sqrt{{a\cdot a + b\cdot b}}$)
• Beweisen Sie ∀Σ : ∀t∈Term(Σ) : depth(t) < | t|.

Für die Signatur Σ = {Z/0, S/1, f /2}:

• für welche Substitution σ gilt f (x, Z)σ = f (S(Z), Z)?
• für dieses σ: bestimmen Sie f (x, S(x))σ.

Notation für Termersetzungsregeln: anstatt (l, r) schreibe l→r.

Abkürzung für Anwendung von 0-stelligen Symbolen: anstatt Z() schreibe Z.

• Für R = {f (S(x), y)→f (x, S(y)), f (Z, y)→y}

  bestimme alle R-Normalformen von f (S(Z), S(Z)).

• für R_d = R∪{d (x)→f (x, x)}

  bestimme alle R_d-Normalformen von d (d (S(Z))).

• Bestimme die Signatur Σ_d von R_d.

  Bestimme die Menge der Terme aus Term(Σ_d), die R_d-Normalformen sind.

• für die Signatur {A/2, D/0}:

  definiere Terme t₀ = D, t_i+1 = A(t_i, D).

  Zeichne t₃. Bestimme | t_i| .

• für S = {A(A(D, x), y)→A(x, A(x, y))}

  bestimme S-Normalform(en), soweit existieren, der Terme t₂, t₃, t₄. Zusatz: von t_i allgemein.

Abkürzung für mehrfache Anwendung eines einstelligen Symbols: A(A(A(A(x)))) = A⁴(x)

• für {A(B(x))→B(A(x))}

  über Signatur {A/1, B/1, E/0}:

  bestimme Normalform von A^k(B^k(E))

  für k = 1, 2, 3, allgemein.

• für {A(B(x))→B(B(A(x)))}

  über Signatur {A/1, B/1, E/0}:

  bestimme Normalform von A^k(B(E))

  für k = 1, 2, 3, allgemein.