Synthese von Gewichtsfunktionen (für SRS)

• Gewicht ist Abbildung g : Σ→$\mathbb {N}$

  forgesetzt zu g^* : Σ^*→$\mathbb {N}$ : w $\mapsto$ $\sum_{i}^{}$g(w_i)

  Bsp: g = {a $\mapsto$ 2, b $\mapsto$ 5}, g(bab) = 12

• das ist wfmA ($\mathbb {N}$, > ,[⋅]) mit [ε] = 0, [c](x) = g(c) + x
• ist kompatibel mit R, falls ∀(l, r)∈R : g^*(l ) > g^*(r)

  Bsp (Verifikation) R = {bab→aaba, a³→b}

• Synthese: gegeben R, kompatible g durch lin. Ungls.

  (1 - 3)g_a + (2 - 1)g_b > 0∧(3 - 0)g_a + (0 - 1)g_b > 0

  Lösbarkeit ist effizient entscheidbar

• als Terminations-Verfahren erscheint das sehr einfach, kann aber nach einer Transformation, welche die Signatur vergrößert, sehr wirksam sein.