Previous Up Next

Module Red

module AS = Absynt

module B = Basic

Rewrite system on Q

The type qterm stands for Q, the type of states of T, a list of indices. The “terms” here are just lists of indices, i.e., a state qαQ is represented by the integer sequence α alone. For substitution, we take the strategy of first-match (from left to right). The function qmatch finds this first match of l inside t. The algorithm is linear in the size of the terms (i.e., the lengths of the lists). The last two arguments are the prefix at the left-hand side of the match and the definitely non-matching part on the left-end of t (accumulated in reverse order). The invariants of the algorithm, as can readily be verified on the branches of the code, are:

   torig =  reverse(l_off) @ pref @ t
   lorig =  pref @ l

The invariants are trivially true when calling the function with empty lists for pref and l_off. Upon proper termination, l is empty, so the first invariant guarantees that the function gives back some match. Since it scans the list from left-to-right, it is the first match.

tested: ok

type qterm = int list

let rec qmatch ((t:qterm), (l:qterm),pref,l_off) : (∗ “t = t[l]” ∗)
     (qterm × qterm × qterm × qterm ) =
   match l with
     [ ] → (tlprefl_off)
   ∣ i::l → 
       match t with 
         [ ] → raise (Failure "qmatch")
       ∣ j::t →
           if (i=j)
           then qmatch (tlpref@[i], l_off)
             match pref with
               [ ] → qmatch (tl, [ ], j::l_off)
             ∣ _ → qmatch (tList.rev(pref)@l , [ ], pref@l_off) (∗ it’s t, not t′∗)

The function works similar to the qmatch, but collecting all matches. Since it gives back the list of matches, it doesn’t raise an error.

tested: ok

let rec qmatch_all ((t:qterm), (l:qterm), prefl_off) :
     (qterm × qterm × qterm × qterm ) list =
   match l with
     [ ] → 
       (match pref with
         [ ] → [(tlprefl_off)]
       ∣ x::pref → 
           (tlprefl_off) :: (∗ that’s the 1st match ∗)
           (qmatch_all ((pref @ t), pref, [ ], (x::l_off))))
   ∣ i::l → 
       match t with 
         [ ] → [ ]
       ∣ j::t →
           if (i=j)
           then qmatch_all (tlpref@[i], l_off)
             match pref with
               [ ] → qmatch_all (tl, [ ], j::l_off)
             ∣ _ → qmatch_all (tList.rev(pref)@l , [ ], pref@l_off) (∗ it’s t, not t′∗)

Using the match-function, qsubst, simply replaces a matching sequence by another one. The substitution is an element of Q× Q; it thus can be seen as a ground rewrite rule on Q. In case the rule cannot be applied, the matching error is raised.

tested: ok

let qsubst (sigmaqterm × qterm) (tqterm
     = (∗ substitute according to (only the) first match ∗)
   match sigma with 
     (l,r) → 
       let (rightcontext,_,_,l_off) = qmatch (tl, [ ], [ ]) 
       in (List.rev l_off) @ r @ rightcontext

Just as the previous qsubst substitued the first match by extracting the relevant information from qmatch, this function substitutes all matches using qmatch_all.
let rec qsubst_all (sigmaqterm × qterm) (tqterm)
     : qterm list 
     = match sigma with
       (l,r) → 
         ( (∗ Just extract the results ∗)
             (fun (rightcontext,_,_,l_off) →
               ((List.rev l_off) @ r @ rightcontext))
             (qmatch_all (tl, [ ], [ ])))

The next function is a simple generalization to a set of rules: it calculates the one-step successors of a term wrt. a given set of equations.

tested: ok

let qonestep (eqs: (qterm × qtermlistt = 
     (fun sigma → qsubst_all sigma t)

The function tests, whether the one step reduction relation specified by ground rewriting system possesses the diamond property. The ground rewrite system possesses the diamond property, if for all critical pairs, the cleave can be closed in one step again. Since we are dealing with a ground rewriting system on words from Q, the situation is a little simpler than for general term rewriting.

One has to take a care, though, not to oversimplify. At first sight, the simplification of the general definition to our setting of strings would be: given two rules (l1,r1) and (l2,r2), a critical pair for the two rules means the pair of terms consisting of (r1) and the result of applying the second rule to the l1. That’s not correct, we must consider the strings as specific terms over symbols with arity 1 and an end symbol. Therefore, for instance, the critical pair of 2 rules (ab, d1) and (bc, d2) is (d1,d2) since bc appears (after unification/substitution of x with c) within the term a(b(x)).

In our setting, a critical pair for two rules (l1,r1) and (l2,r2) (in this order) is computed by finding a non-empty overlap of the left-hand sides of the form l = l1lo l2′ such that l1 = l1lo and l2 = lol2′ and where lo, the common overlap, is non-empty. Note that the definition is asymmetric, since l1 precedes l2.

The function qoverlap is auxiliary. As invariant we maintain

       t1=t1pre @ to @ t1post 
       t2=to @ t2post

until t1post is empty. The initialization is with t1pre = to = [], t1post = t1, and t2post = t2.

let rec qoverlap (t1_pret1_postt_ot2_post
     : (qterm × qterm × qterm × qterm ) = 
   match t1_post with
     [ ] → (t1_pret1_postt_ot2_post)
   ∣ e1::t1_post →
       (match t2_post with
         [ ] → 
           (match t_o with
             [ ] → (t1_pre@t1_post,[ ],[ ],[ ])
           ∣ e3::t_o →
               qoverlap (t1_pre@[e3], t_o@t1_post, [ ], t_o)) 
       ∣ e2::t2_post →
           if e1 = e2 
           then qoverlap (t1_pre,t1_post,t_o@[e1],t2_post)
               match t_o with 
                 [ ] → qoverlap (t1_pre@[e1],t1_post,[ ],t2_post)
               ∣ e3::t_o
                   qoverlap (t1_pre@[e3], t_o@t1_post, [ ], t_o @t2_post))

Being able to find an end-overlap, we can build the critocal pairs finally.
let qcover (l1l2) =
   let (l1_prel1_postl_ol2_post) = qoverlap ([ ],l1,[ ],l2)
   match l_o with
     [ ] → l1_pre
   ∣ _ → (∗ non-trivial overlap! ∗)
       l1_pre @ l_o @ l2_post

let qcrit_pairs ((l1,r1), (l2,r2)) = (∗ crit. pairs

tested: ok

   let (l1_prel1_postl_ol2_post) = qoverlap ([ ],l1,[ ],l2)
   in match l_o with
     [ ] → [ ] (∗ no critical pairs ∗)
   ∣ _ →
       (let tl = qsubst_all (l2,r2) (l1_pre @ l_o @ l2_post)
         (fun r1′ → (r1@l2_postr1′)) (∗ forming the pairs ∗)

let qpair_is_joinable_or_equal eqs (t1,t2) = 
   if (t1=t2
   then true
     let (t1_postt2_post) = (qonestep eqs t1qonestep eqs t2)
     in (∗ the post-states must have at least one element in common ∗)
     List.exists (fun t1′ → List.mem t1′ t2_postt1_post

let qpair_is_joinable_or_equal2 (eqs1,eqs2) (t1,t2) =
   if t1 = t2
   then true
     let (t1_post_with_eqs1t2_post_with_eqs2) = (qonestep eqs1 t1qonestep eqs2 t2)
     List.exists (fun t1′ → List.mem t1′ t2_post_with_eqs2t1_post_with_eqs1

let qhas_diamondprop (eqs: (qterm × qtermlist) = 
   let ruleccombinations = Basic.list_cross_product eqs eqs
     (fun (rule1rule2) → 
         (qpair_is_joinable_or_equal eqs)
         (qcrit_pairs (rule1,rule2)))

let qhas_swappingdiamondprop (eqs1eqs2) = (∗ ∗)
   let ruleccombinations = Basic.list_cross_product eqs1 eqs2
     (fun (rule1rule2) → 
         (qpair_is_joinable_or_equal2 (eqs2eqs1)) (∗ reverse ∗)
         (qcrit_pairs (rule1,rule2)))

The next functions are about (ground) rewriting and normalizing. The function qrewrite is just auxiliary for normalizing.
exception NormalForm

let rec qrewrite eqs t = (∗ rewrites t according to the equations ∗)
   match eqs with 
     [ ] → raise (NormalForm)
   ∣ (l,r):: rest → 
         qsubst (l,rt
       with _ → (qrewrite rest t)

let rec qnorm (eqs: (qterm × qtermlistt = 
   match t with
     [ ] → t
   ∣ i::t → 
       let u = i::(qnorm eqs t)
       try (qnorm eqs (qrewrite eqs u))
       with NormalForm → u

let qnorm_starstate eqs (tint list list) = (fun x → [x]) (qnorm eqs (List.flatten t))

In the next function the set of equations are already assumed to be ordered and terminating! It finds rules that can be inferred already using the others, in this way also removing doublettes.6

let normalize_rewrite_eqns eqns =
   let rec purge eqns_orig eqns_purged =
             match eqns_orig with
       [ ] → eqns_purged
     ∣ (l,r)::eqns_orig → 
         if (List.mem (l,reqns_purged) (∗ an immediate doublette ∗)
         then purge eqns_orig eqns_purged
           (let l_norm = qnorm eqns_purged l
           in let r_norm = qnorm eqns_purged r
                   if (l_norm = r_norm)
           then purge eqns_orig eqns_purged
           else purge eqns_orig ((l,r)::eqns_purged))
   in List.rev (purge eqns [ ])


Substitutions (here kept separate for variables and for parameters) are finite maps from variables (or parameters) to terms. As implementation, the corresponding data-type from the library is used. For comparison of the entries in the map, i.e., the pairs for the variables/parameters and their index, the generic comparison function can be used. Since variables and parameters are largely handled the same, many of the following definitions come in pairs.

module VKey =
     type t = AS.vname
     let compare (s,i) (s,j) =
       compare (s,i) (s,j) (∗ generic comparison function ∗)

module PKey =
     type t = AS.pname
     let compare (s,i) (s,j) =
       compare (s,i) (s,j) (∗ generic comparison function ∗)

module VSubst = Map.Make(VKey)
module PSubst = Map.Make(PKey)

From the library’s modules, we get the types for the 2 kinds of substitutions, the definition of the domain of the substitution and the definition for the effect of a substition to a variable.

type α vsubst = α term VSubst.t
type α psubst = α term PSubst.t

let v_indom v vs = VSubst.mem v vs
let p_indom p ps = PSubst.mem p ps

let v_app_atomic vs v = 
     VSubst.find v vs
     Not_found → raise (Failure "variable substitution undefined")

let p_app_atomic ps p = 
     PSubst.find p ps
     Not_found → raise (Failure "parameter substitution undefined")

Applying a substitution to a term is the homomorphic lifting of the atomic substitution function through the term structure.


let rec v_app vs t =
     match t with
       AS.V v → v_app_atomic vs v
     ∣ AS.P _ → t
     ∣ AS.T(stl) →
         AS.T( (v_app vstl)
     ∣ AS.QT(qttl) →
         AS.QT(qv_app vs (v_app vstl)
   with (Failure s) → t

let rec p_app ps t =
     match t with
       AS.V _ → t
     ∣ AS.P p → p_app_atomic ps p
     ∣ AS.T(stl) →
         AS.T( (p_app pstl)
     ∣ AS.QT(qttl) →
         AS.QT(qp_app ps (p_app pstl)
   with (Failure s) → t

The next two functions check for occurrence of variable or parameter in a term.

let rec v_occurs (v:vname) (t: α term) : bool =
   match t with
     AS.V v → (v = v)
   ∣ AS.P _ → false
   ∣ AS.T(stl) → List.exists (v_occurs vtl
   ∣ AS.QT(qttl) → List.exists (v_occurs vtl

let rec p_occurs (p:pname) (t: α term) =
   match t with
     AS.V _ → false
   ∣ AS.P p → p = p
   ∣ AS.T(stl) → List.exists (p_occurs ptl
   ∣ AS.QT(qttl) → List.exists (p_occurs ptl


A match σ of two terms t1 and t2 is a substitution such that t1σ = t2. This is calculated by term_match. The function is termmatches is auxiliary, incrementally collecting the substitution for a list of term-pairs; The same for terms_match, which is exported.

exception No_Match

let rec termmatches ((tpairsvs): (α term × α termlist × α vsubst) =
   match tpairs with
     [ ] → vs
   ∣ (AS.V vt2)::tpairs →
       if v_indom v vs
         if (v_app_atomic vs v = t2)
         then termmatches (tpairsvs)
         else raise No_Match
       else termmatches (tpairs, (VSubst.add v t2 vs))
   ∣ (_AS.V _)::tpairs → raise No_Match
   ∣ (AS.P p1AS.P p2)::tpairs →
       if p1 = p2 
       then vs
       else raise No_Match
   ∣ (AS.T(s1tl1), AS.T(s2tl2))::tpairs →
       if s1 = s2
       then termmatches (((List.combine tl1 tl2) @ tpairs), vs)
       else raise No_Match
   ∣ (AS.QT(s1t1tl1), AS.QT(s2t2tl2))::tpairs →
       if s1 = s2
       then termmatches (((t1,t2):: ((List.combine tl1 tl2) @ tpairs)), vs)
       else raise No_Match
   ∣ _ → raise No_Match

let termmatch ((t1,t2) : (α term × α term)) = termmatches ([(t1,t2)], VSubst.empty)

let terms_match (tpairs: (α term × α termlist) : α vsubst = 
   termmatches (tpairsVSubst.empty)

Term reduction

The function rule_o_term applies a rule, i.e., a pair of terms (of specific form), to another term. In case the left-hand side of the rule does not match, the term is not reduced (but no error is raised).

tested, ok

The function one_or_0_step is the generalization to a list of rules. This gives the set of reachable states starting from a given term and applying the set of rules 0 or one 1 step.

Tested: ok?

let rec rule_o_term ((lhs,rhs): α rule) (t: α term) : (α termlist =
   match t with
     AS.V v → [t] (∗ variables cannot be reduced ∗)
   ∣ AS.P p → [t] (∗ parameters cannot be reduced ∗)
   ∣ AS.T(stl) →
       let post_tl = (rule_o_term (lhs,rhs)) tl
       let reduced_inside = 
           (fun tl → AS.T(stl))
           (B.list_product_2 post_tl)
       in let reduced_outside =
           [(v_app (termmatch (lhst)) rhs)]
         with No_Match → [ ]
       reduced_outside @ reduced_inside
   ∣ (AS.QT(sttl)) →
       let post_tl : (α termlist list = (rule_o_term (lhs,rhs)) tl
       in let post_t : (α termlist = rule_o_term (lhs,rhst
       in let reduced_inparameters : (α termlist list = B.list_product_2 post_tl
       in let reduced_inside =
           (fun (ttl) → AS.QT(s,t,tl))
           (B.list_cross_product post_t reduced_inparameters)
       in let reduced_outside =
           [(v_app (termmatch (lhst)) rhs)]
           No_Match → [ ]
       in reduced_outside @ reduced_inside

let one_or_0_step (rl: (α rulelist) (t: α term) = 
       (fun (l: (α termlist) → 
         fun (r: α rule) → (rule_o_term r t) @ l))
     [ ] rl

The function reduce_until finally iterates the one-step reduction function in a depth-first search manner, to all terms until the given predicate holds.
let reduce_until (rl: (α rulelist) (p: α term → bool) (t: α term) = 
   let g = B.Graph (one_or_0_step rlin B.dfs_collect g p t

Previous Up Next