![]() |
Semantic Labelling |
![]() |
AProVE Help System → Techniques → Techniques working on TRSs → | Semantic Labelling |
More specifically, we are looking for a Σ-Algebra (M, φ) as a (quasi-)model of our term rewrite system R. In order to find such an algebra automatically we restrict ourselves to finite carrier sets M, typically the 2-element set {0, 1}. Then we find a φ which assigns to each f ∈ Σ a function Mf over M. Due to the finiteness of M there are only finitely many of those functions.
A variable assignment α is a function which assigns to each variable x a value v ∈ M. We can extend α to a function αφ on terms by defining αφ(x) = α(x) for a variable x and αφ(f(t1, ..., tn)) = φ(f)(αφ(t1), ..., αφ(tn)) for a function symbol f of arity n.
Labelling of a term t given a variable assignment α is done by labeling each function symbol by the value of its arguments, i.e. α(x) for a variable x and the concatenation of all values of the arguments for a function symbol f. We denote the labeled term by lab(t). The labeling of a term rewrite system is the straightforward application of this labeling to all left-hand sides and all right-hand sides for all possible variable assignments over M.
(M, φ) is a quasi-model for R for a given well-founded order > on M if and only if for all l → r ∈ R and all variable assignments α we have αφ(l) ≥ αφ(r) and all Mf are weakly monotone functions. The term rewrite system Decr(Σ,M,>) is the set of all rules fx(v1, ..., vn) → fy(w1, ..., wn) with f ∈ Σ and x > y.
If (M, φ) is a quasi-model of R for >, then lab(R) ∪ Decr(Σ,M,>) terminates if and only if R terminates.
The Semantic Labelling in AProVE is used in conjunction with removal of redundant rules (RRR), i.e. the quality of a model is assessed by the number of rules that could be deleted by labeling R using the model, applying RRR and unlabeling the resulting system.
Semantic labeling increases the number of function symbols and rules significantly. As thus, it should only be applied when termination of the original term rewrite system R could not be shown using other techniques. As the search space explodes with the arities of functions symbols in R and the number of variables occurring in a rule, Semantic Labelling should normally only be applied to string rewrite systems or systems which are almost string rewrite systems.