# Library CoLoR.Term.WithArity.ATrsNorm

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
1) canonical representation of a rule l -> r:
WE ASSUME: incl (vars r) (vars l).
given the list of variables of l, xs = ATerm.vars l,
a variable of l or r is renamed as its position in xs
2) canonical representation of a list of rules R:
the rules of R are put in their unique representation
and R is sorted wrt the following ordering
(l1,r1) >rule (l2,r2) if (l1,r1) (>term)lex (l2,r2)
f(t1..tn) >term g(u1..up) if
(f,(t1..tn)) (>symb,(>term)lex)lex (g,(u1..up))
f(t1..tn) >term x
x >term y if x >nat y
assuming a total ordering >symb on symbols

- Frederic Blanqui, 2008-08-08

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation terms := (vector term).

canonical representation of a rule

Section norm.

Variable xs : variables.

Fixpoint norm (t : term) : term :=

match t with

| Var x =>

match position beq_nat x xs with

| Some y => Var y

| None => Var (length xs)

end

| Fun f ts => Fun f (Vmap norm ts)

end.

End norm.

Definition mkNormRule l r :=

let xs := ATerm.vars l in mkRule (norm xs l) (norm xs r).

canonical representation of a list of rules

Section term_ordering.

Variable symb_cmp : Sig -> Sig -> comparison.

Fixpoint cmp (t u : term) : comparison :=

match t, u with

| Var x, Var y => nat_compare x y

| Var x, _ => Lt

| _, Var x => Gt

| Fun f ts, Fun g us =>

match symb_cmp f g with

| Eq =>

let fix cmp_terms n (ts : terms n) p (us : terms p)

: comparison :=

match ts, us with

| Vnil, Vnil => Eq

| Vnil, _ => Lt

| _, Vnil => Gt

| Vcons t ts, Vcons u us =>

match cmp t u with

| Eq => cmp_terms _ ts _ us

| c => c

end

end

in cmp_terms (arity f) ts (arity g) us

| c => c

end

end.

Definition mkNormRules := sort cmp.

End term_ordering.

End S.