left

Semantic Labelling

right
AProVE Help SystemTechniquesTechniques working on TRSsSemantic Labelling

Description

The basic idea of Semantic Labelling [Zan '95] is to introduce a labeling for function symbols of a given term rewriting system R over the signature Σ depending on the semantics of their arguments.

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.

Application and Configuration

You can select whether you want to return the labeled or the unlabeled TRS. Note that returning an unlabeled TRS does make sense, as some rules will have been deleted in the process. Normally Semantic labeling is restricted to string rewriting for efficiency reasons. This can be changed by selecting work on TRSs in addition to SRSs. The user can also define the size of the carrier set M (Model Size) and the range of the polynomials used for RRR in evaluating models (RRR Range).

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.