Library CoLoR.Term.WithArity.ATrsNorm

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2008-08-08
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

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.