Previous Up Next

Module Mtt

The module contains the implementation of the transducers. In this document, we’ll leave out various functions for diagnosis present in the actual code.
type qequations = (qstarindex × qstarindexlist (∗ rename to qstarequations ∗)
type qstarrelation = qequations

type α twopartition = (α list) × (α list)
type d_partition = ((qstarindex × qstarindextwopartition) × qstarindex list

The following function converts a number of state-pairs into an ground rewrite system on Q. With the current representation, it’s just the identity relation.


let eqns_of_qstarindexpairs (ql : (qstarindex × qstarindexlist) : qequations = ql

Next some predicates for checking, whether terms are acceptable as part of a new rule, for instance. The result depends on whether we calculate the composition or the iteration of transducers. The predicate is_pureterm checks for containment in TΣ, i.e., no q’s appear, the function is_rhs_term_comp for TΣ(Q2(X)), is_rhs_term_star for TΣ(Q(X)), is_constructorterm for Σ(X), is_variableterm for X, and finally is_lhs_term_star for Q(Σ(X)). The functions are parametric in the choice of the type for the states.
let is_variableterm (t:α term): bool = (∗ tX. (x(q) is not allowed) ∗)
   match t with 
     AS.V(_,_) → true
   ∣ _ → false

let is_constructorterm (t: α term) : bool = (∗ t ∈ Σ(X) ∗)
   match t with 
     AS.V(_,_) → false
   ∣ AS.P(_,_) → false
   ∣ AS.T(_,subterms) → (List.for_all is_variableterm subterms)
   ∣ AS.QT (___) → false

let rec is_pureterm (t: α term) : bool = (∗ tTΣ(X)

unclear

∗) 
   match t with 
     AS.V(_,_) → true
   ∣ AS.P(_,_) → true
   ∣ AS.T(_,subterms) → (List.for_all is_pureterm subterms)
   ∣ AS.QT (AS.Q _ttl) → false

let rec is_lhs_term_star (t: α term) : bool = (∗ tQ(Q(..(Σ(X))

tested: ok

∗)
   match t with 
     AS.V(_,_) → false
   ∣ AS.P(_,_) → false 
   ∣ AS.T(_,subterms) → (∗ Q can be Q0 ∗)
       is_constructorterm t
   ∣ AS.QT (AS.Q jttl) → 
       (match t with
         AS.QT (AS.Q ___) → is_lhs_term_star t (∗ PARMS ∗)
       ∣ _ → is_constructorterm t)

let rec is_rhs_term_star (t: α term) : bool = (∗ TΣ(Q(…(Q(X)) ∗)
   match t with 
     AS.V(_,_) → true
   ∣ AS.P(_,_) → true
   ∣ AS.T(_,subterms) → (List.for_all is_rhs_term_star subterms)
   ∣ AS.QT (AS.Q jttl) → 
       match t with
         AS.QT (AS.Q ___) → is_rhs_term_star t (∗ PARMS ∗)
       ∣ AS.V(_,_) → true
       ∣ AS.P(_,_) → false
       ∣ AS.T(_,_) → false

Transduction

With the help of the rewrite-module, the implementation of reduction is trivial: reduce the term until it qualifies as a closed term from TΣ.

tested, linear examples


let transduce ((_,_,ql,iqlist,rl): α mtt) (t: α term) : (α termlist =
   B.list_flatten_map (∗ for all inital states: collect the reduction results ∗)
     (fun qinit → Red.reduce_until rl is_pureterm (AS.QT(qinit,t,[ ])))
     iqlist

Simulation and equivalence


Given a sequence of indices from Q and a symbol f (equipped with an arity), the function build_starstate builds a term from Q(f(x1,…,xn)), more precisely in the exploded from Q(Q(… (Q(f(x1,…,xn))… ))), to make it a term with states from Q1. The fact that the term is “exploded” is important, otherwise we can’t use the rules of T1.
let rec build_qstarterm (ilqstarindexs : qindex term =
   match il with 
     [ ] → AS.build_constructorterm s
   ∣ i:: il → AS.QT(AS.Q(i), (build_qstarterm il s), [ ])

The bisimulation-algorithm later will work in an “on-the-fly”-manner. This means that after exploring the state-space/reducing the terms, one has to find out, whether the terms reached will contain new states from Q. The function extract_output_and_qstars recurs through a given term and collects all the states from Q occurring inside it. At the same time, it extract the “pure” terms, erasing all the qα’s. This is needed to compare the output according to the definition of bisimulation (the term —without mentioning the states— is the output of a transition). The two functions extract_qstars and extract_output are the corresponding projections to the components.

The function extract_linear_term_and_n works simularly. Given a term tTΣ(Q(X)), it replaces all states from Q by variables.7 More precisely, it takes a term tTΣ(Q(TΣ)) and does the replacement, since the nature of the terms “inside” Q is not checked. The variables used from left to right are x0 to xn−1, if there are n occurrences of states in the term.

Unchecked

8


let rec extract_leading_qstar (tqindex term) : qstarindex =
   match t with 
   ∣ AS.V(_,_) → [ ] (∗ index of qє ∗)
   ∣ AS.P(_,_) → [ ]
   ∣ AS.T(symbtl) → [ ]
   ∣ AS.QT(AS.Q(i:qindex), ttl) → (∗ NO PARMS !∗)
       let ql = extract_leading_qstar t
       in i::ql

       NO PARMS !

Unchecked


let rec extract_output_and_qstars (tqindex term) : ((qindex term) × (qstarindex list)) =
   match t with
   ∣ AS.V(_,_) → (t,[[ ]]) (∗ list of an empty list! ∗)
   ∣ AS.P(_,_) → (t,[[ ]])
   ∣ AS.T(symbtl) → 
       let (tlql) = List.split (List.map extract_output_and_qstars tl)
       in (AS.T(symbtl), List.flatten ql)
   ∣ AS.QT(AS.Q(i:qindex), ttl) → (∗ NO PARMS !∗)
       let (tql) = extract_output_and_qstars t
       in (t
             List.map 
               (fun q → i::q) (∗ prepend the outer index ∗)
               ql)

       NO PARMS !
let extract_output (tqindex term) : qindex term = fst (extract_output_and_qstars t)

let extract_qstars (tqindex term) : (qstarindex list) = snd (extract_output_and_qstars t)

The following function assumes, that tTΣ(Qx(TΣ(X))), i.e., the states are all together
let rec extract_indices (t: α term) : α list = 
   match t with 
     AS.V(_,_) → [ ] 
   ∣ AS.P(_,_) → [ ]
   ∣ AS.T(symbtl) → 
       Basic.list_flatten_map extract_indices tl
   ∣ AS.QT(AS.Q(i:α), ttl) → [i]

let extract_linear_term_and_n (tqindex term) : (qindex term × int) =
   let rec extract t (i:int) = (∗ start counting at i

tested: ok

∗)
     match t with
     ∣ AS.V(_,_) → (AS.V((Symbol.symbol_of_string "x"),i),i+1) (∗ direct ∗)
     ∣ AS.P(_,_) → raise (Failure "no parameters yet")
     ∣ AS.T(symbtl) → 
         let (tlj) =
           List.fold_left (∗ counting from left to right ∗)
             (fun ((rl,x): (qindex termlist × int) → 
               fun (sqindex term)→ 
                 let (s,k) = (extract s x)
                 in (rl@[s], k))
             ([ ],i)
             tl
         in
         (AS.T(symbtl),j
     ∣ AS.QT(AS.Q(_), ttl) → (∗ as soon as there is a q, we are through ∗)
         (AS.V((Symbol.symbol_of_string "x"),i),i+1)
   in extract t 0

Now the code for simulation. The function terms_and_qs_notin_rel is basically the lifting function. It takes a finite relation on states and lifts it to the term level. On term level, the function is represented as predicate on term pairs, as it is no longer a finite relation. In first approximation one can consider it as the lifting function of [DLS02]. The difference is that, when using the lifting-operation in doing one iteration step (one_fbisimstep resp. one_pbisimstep) to obtain the bisimulation relation, the lifting operator does not take the current relation Ri as argument but it’s “complement” Ri (the variable nonq). The reason why to use the complement is that the algorithm for bisimulation works in a “on-the-fly” manner.

In the forward case, one has to take care how to treat the inductive case the terms starting with a state from Q. In this case we have to keep on comparing the rest of the term, since the state are taken from Q. The function assumes that t1 and t2 are right-hand sides, i.e. from TΣ((Q)(X)). In the definition of bisimulation, where the function is used, this is guaranteed by the function post_on_symbol.
let rec terms_and_qs_notin_rel (rqstarrelation) (t1,t2) : bool =
   assert ((is_rhs_term_star t1) ∧ (is_rhs_term_star t2));
  
   match (t1,t2with
     (AS.V(s1,i1), AS.V(s2,i2)) → (s1=s2) ∧ (i1=i2)
   ∣ (AS.P(s1,i1), AS.P(s2,i2)) → (s1=s2) ∧ (i1=i2)
   ∣ (AS.T(s1,subterms1), AS.T(s2,subterms2)) →
       if (s1 ≠ s2) (∗ different term structure ∗)
       then false 
       else (List.for_all (terms_and_qs_notin_rel r) (List.combine subterms1 subterms2))
   ∣ (AS.QT (AS.Q i1__), AS.QT (AS.Q i2__)) → 
       let ((q1qstarindex),(q2qstarindex)) = (extract_leading_qstar t1,
                                                   extract_leading_qstar t2)
       in
             ¬ (List.mem (q1,q2r) (∗

?

complement of R! ∗)
   ∣ _ → false

In the backward case we have to compare terms of a more restricted form, because we reduce backwards until we encounter a left-hand side. Left-hand side terms are somewhat simpler than terms on the right-hand side of a rule. They are of the form tQ(TΣ(X)), i.e., a state followed by a single symbol. Since the identity of the variable does not play a role, we have to “lift” the relation (or rather its complement as before) to pairs of a state and a single symbol. This is done in the function q_and_symbol_notin_rel. The function gives answers negatively, if the structure (the symbols) are different or if the pair of states can be distinguished by the argument relation.

The following function qs_notin_rel is the analogue on just states, not complete terms; therefore the function is rather trivial. It is included to make the parallel between the forward and the backward case more clear.
let qstar_and_symbol_notin_rel (rqstarrelation) (∗ ∗)
     (((q1s1),(q2s2)) : (qstarindex × symbol) × (qstarindex × symbol)) 
     = 
   ((s1 = s2) (∗ if s1s2, then the pairs can be distinguished ∗)
       ∧ 
     (¬ (List.mem (q1,q2r))) (∗ complement of R! R contains the distinguishing pairs. ∗)
  

   The function post_on_symbol simply computes all reachable correct right-handsides, reachable by applying a given state from Q to a given symbol.

tested, ok


let post_on_symbol rl s (qlqstarindex) : (qindex termlist = 
   Red.reduce_until rl is_rhs_term_star (build_qstarterm ql s)

The function pre_on_rhs will be used to calculate all the predecessor terms of a given right-hand side of a rule. Since rules are just pairs of terms, we can simply reverse the rules of the transducer and use the generic reduction function reduce_until.

untested again


let pre_on_rhs (rl: ( qindex rulelist) (tqindex term) : (qindex termlist =
   assert ((is_rhs_term_star t)
             ∧ 
           (¬ (is_pureterm t))); (∗ otherwise the function diverges! ∗)

   Red.reduce_until 
     (List.map (fun (r,l) → (l,r)) rl) (∗ reduce backwards

tested: ok

∗)
     is_lhs_term_star (∗ ∗)
     t

For the past-bisimulation, the comparison can be done between the left-hand sides. Since the identity of the variable does not play a role, we extract a pair of the leading state and the following single symbol from a term of Q(Σ(X)), i.e., a legal left-hand side.
let extract_symbol (tqindex term) : symbol = (∗ t ∈ Σ(X) ∗)
   match t with
     AS.V(_,_) → raise (Failure "cannot happen (extract_symbol)")
   ∣ AS.P(_,_) → raise (Failure "cannot happen (extract_symbol)")
   ∣ AS.QT (AS.Q jttl) → raise (Failure "cannot happen (extract_symbol)")
   ∣ AS.T(s,varlist) → s

let rec extract_qstar_and_symbol_of_lhs (tqindex term) : (qstarindex × symbol) =
   assert (is_lhs_term_star t); (∗ ∈ Q(Σ(X)). ∗)
   match t with 
     AS.V(_,_) → raise (Failure "cannot happen")
   ∣ AS.P(_,_) → raise (Failure "cannot happen")
   ∣ AS.T(_,_) → ([ ], extract_symbol t)
   ∣ AS.QT (AS.Q jttl) → 
       let (qs) = (extract_qstar_and_symbol_of_lhs t)
       in (j :: qs)

let extract_qstar_of_lhs (tqindex term) : qstarindex = fst (extract_qstar_and_symbol_of_lhs t)

Forward bisimulation

The function one_fbisimstep is the basic step of the partition refinement algorithm for calulating the largest forward bisimulation. Its arguments can be divided in static and dynamic ones. The static ones are the rules of the transducer, i.e., the rules according to which the bisimulation step is evaluated. Then the signature Σ, here ssig which constitutes the input to be checked. Finally the ground rewrite-system to simplify the states.9

The dynamic components of the functions are the partition of the currently known set of states and the set of states itself. One bisimulation step refines the partions and, at the same time, gives back newly detected states.

About the partitioning: the variable unknown corresponds to Ri, the ith iteration of the bisimulation relation. The function terms_and_qs_notin_rel is applied to nonq = Ri, i.e., the pairs of states, which are already known to be non-bisimular (and will stay so). This is to avoid, that a pair is to be falsely considered to be non-congruent, just because the states in the terms after one step have not been visited before and thus had not had the chance of being listed in Ri.


let one_fbisimstep (rl: (qindex rulelist) (ssigssignature) (rewrite_eqsqequations)
     (((unknownnonq), visitedq) : d_partition) : d_partition
     (∗ The last component of the returned d-partition are the newly detected states. The second component of the returned partition are likewise the newly detected non-congruent pairs (since the step partitions the input unknown.

tested (few): ok

∗)
     =
     let (still_unknownnew_nonq) = (∗ partition unknown ∗)
     List.partition (fun (i,j) → 
             List.for_all (fun (s: (symbol × int)) → (∗ ∀ s ∈ Σ ∗)
         let (post_ipost_j) = (post_on_symbol rl s ipost_on_symbol rl s j)
         in 
                 (List.for_all (fun (t1′qindex term) → (∗ ∀ t1′ ∗)
           List.exists (fun (t2′qindex term) → (∗ ∃ t2′ ∗)
             (terms_and_qs_notin_rel nonq (t1′t2′))) (∗ t1′Rt2′∗)
             post_j)
             post_i)
           ∧
         (List.for_all (fun (t2′qindex term) →
           List.exists (fun (t1′qindex term) →
             (terms_and_qs_notin_rel nonq (t1′t2′)))
             post_i)
             post_j))
         ssig)
       unknown;
   in 
     let states_reaped : qstarindex list = (∗ scan for unseen states (inefficient) ∗)
     B.list_remove_doublettes 
       (B.list_flatten_map
           (fun (i,j) → (∗ for all (i,j) ∈ R ∗)
             (B.list_flatten_map
               (fun s → (∗ for all s ∈ Σ ∗)
                 (B.list_flatten_map extract_qstars (post_on_symbol rl s i) @
                   B.list_flatten_map extract_qstars (post_on_symbol rl s j)))
               ssig))
           unknown)
   in let newly_detected = List.find_all (fun x→ (¬ (List.mem x visitedq))) states_reaped 
   in ((still_unknownnew_nonq), newly_detected)

The function fbisimulation_states builds the fixpoint of the previous function. In a first approximation, it refines the partitioning until it has stabilized, i.e. here, that no more new non-equivalent state are found (nonq is empty). The fixpoint-iteration is done by an inner function fbisim. Since the calculation of the bismulation is done on-the-fly, the exit-condition for the fixpoint is slightly more complicated than just testing for emptyness of nonq. Each single iteration step explores the “state-space” consisting of terms from TΣ(Q(X)). In doing so, it might encounter new states from Q not seen before (given back in new_visitedq). Only if no new states are found, the iterations ends. If new states are found, the relations must be extended by building pairs from the new states, whose status wrt. bisimulation is unknown for a start.
let fbisimulation_states (rl: (qindex rulelist) (ssigssignature) (rewrite_eqsqequations)
     (((unknownnonq), visitedq) : d_partition)
     : d_partition
     =
   let rec fbisim (∗ the inner bisimulation loop ∗)
       (rewrite_eqsqequations)
       (((unknownnonq), visitedq) : d_partition)
       : d_partition
       =
         let ((still_unknownnew_nonq), new_visitedq) = (∗ partition unknown ∗)
       one_fbisimstep rl ssig rewrite_eqs ((unknown,nonq), visitedq)
     in 
         match (new_nonq,new_visitedqwith 
       ([ ],[ ]) → ((still_unknownnonq),visitedq) (∗ end of iteration ∗)
     ∣ (_,[ ]) → (∗ at least no new states ∗)
         fbisim rewrite_eqs ((still_unknown,nonq@new_nonq),visitedq)
     ∣ (_x::v) → (∗ new states => new unexplored pairs of states ∗)
         let further_unknown = 
           (B.list_cross_product new_visitedq new_visitedq) @
           (B.list_cross_product new_visitedq visitedq) @
           (B.list_cross_product visitedq new_visitedq)
         in fbisim rewrite_eqs ((still_unknown@further_unknown,new_nonq@nonq),
                                 new_visitedq@visitedq)

   in fbisim rewrite_eqs ((unknown,nonq), visitedq)

Given a list of states from Q, the function builds, in the obvious way, an initial partition: the unknown pairs is the full relation, the non-congruent part of the relation is initially empty.

Tested: ?


let rec build_startpartition (qlqstarindex list) : d_partition 
     = (((B.list_cross_product ql ql),[ ]),ql)

The next function just wraps up the previous one. The reason, we the previous one might independantly be useful is the by reusing information in the additional arguments, one can save time.

untested


let fbisimulation_states_fromscratch (rl: (qindex rulelist) (ssigssignature) (rewrite_eqsqequations)
     (visitedqqstarindex list)
     : d_partition
     = fbisimulation_states rl ssig rewrite_eqs (build_startpartition visitedq)

Past bisimulation

Past bisimulation will be handled similar to the forward case.

stubs only

The situation is slightly more complex, though. The definition of past bisimulation from [DLS02] is dual to the forward case. The crucial problem is, that if we just take the naive approach, past bisimulations are not closed under union, but the union closed under reflexive, transitive, and symmetric closure is.


The iterative step in the calculation of the past bisimulation is given by:

(q1,q2) ∈ Ri+1 iff. q1″( f(x))—→t[q1′,…,q1…,qn′]} for some t, q1,… qn, q1″, then ∃ q2″ such that q2″(f(x)) —→ t[q1′,…,q2…,qn′] and q1Ri q2″.

So, as first step we have to calculate all pairs of right-hand sides for a given transducer, for which the precondition of the above implication holds.


Next we need a lifting function, which just exchanges one pair of states in a given term and leaves the rest untouched. It will be used only for pairs of states but we define it here also for whole relations, i.e., sets/lists of pairs of states.

Again we have to take into account that the bisimulation algorithm will work on-the-fly. This means the set of states is not statically known before. Therefore, the sign of being undistinguishable in the i+1th iteration is not, that all the pre-states are indistinguishable according to the bisimulation definition, but rather that it is not the case that the pre-states are already known to distiguisable in the ith iteration.

One problem is, to find all relevant right-hand sides. Of course we don’t want to deal with infinitely many, only those we expect to contribute to the property. The rules that we are working with, are from T and not T, so we can’t just take the right-hand sides of the rules of T as pattern!


The following function builds the starting terms for the backward exploration. We start building all possible combinations for a given pair (qi,qj) of states and a list of states. The natural number n ≥ 0 gives the length of the resulting lists (i.e., the length after inserting either qi or qj). In the degenerated case, that the list of states is empty and a length of n>1 is required, the result is empty, as well. In case n = 0, the result is likewise (and unconditionally) a pair of empty lists. The case is treated separately since the function list_combinations expects non-negative arguments.

tested: ok


let build_statecombinations 
     ((qiqj): qstarindex × qstarindex)
     (qlqstarindex list) (∗ set (not list) of states QvQ ∗)
     (nint) (∗ n ≥ 0 ∗)
     : ((qstarindex listlist) × ((qstarindex listlist)
     = (∗ {(q1′,…,qi,…,qn−1′) ∣ qk′∈ Qv} × {(q1′,…,qj,…,qn−1′) ∣ qk′∈ Qv} ∗)
   if (n = 0)
   then 
     ([ ], [ ])
   else
     let (q_to_n : qstarindex list list) = B.list_combinations ql (n−1) (∗ =Qn ∗)
     in 
     ( (B.list_flatten_map (B.list_insert_after_allpos qiq_to_n),
       (B.list_flatten_map (B.list_insert_after_allpos qjq_to_n))

Next we have to construct all terms which can possibly contribute to a backward step. The function build_relevant_rhs takes a term, which must be a right-hand side, and turns it into a set/list of pairs of terms which may contribute to a backward step. In the past bisimulation step, those pairs are generated by taking all currently known states (visitedq), permuting them in all possible ways into the available right-hand sides.

Special care must be taken dealing with right-hand sides for closed terms and terminal symbols, which in the current representation take the role of final states. Those terms cannot be used to distinguish a pair of states in the partition-refinement step. Therefore, those terms do not count as relevant and filtered out.10

We start with generating the relevant terms for one given input term (build_relevant_rhs), before we generalize the function to lists of terms (build_relevant_rhss).

It’s different now!
untested again: ok?


let rec qstarindex_as_qstarterm (q : qstarindex) (tqindex term) : qindex term 
     = (∗ wrap q around the term ∗) 
   match q with 
     [ ] → t
   ∣ i::q → AS.QT((AS.Q i),
                       qstarindex_as_qstarterm q t,
                       [ ])

let build_relevant_rhs
     ((qi,qj): qstarindex × qstarindex) (∗ pair of states from Q to separate ∗)
     (visitedqqstarindex list)
     (tqindex term)
     : (qindex term × qindex termlist
     = 
   assert (is_rhs_term_star t);
   let ((t_naked,n): qindex term × int) = extract_linear_term_and_n t
   in 
   let ((ql_iql_j): (qstarindex listlist × (qstarindex listlist) = 
     (∗ A pair of sets of vectors (= same-length lists) of elements from Q ∗)
     build_statecombinations (qi,qjvisitedq n (∗ find all combinations of states ∗)
     (∗ Each set of vectors must be turned into a set of substitutions ∗)
   in 
   if ((ql_iql_j)) = ([ ],[ ]) 
   then
     [ ]
   else
     let build_varlist (nint) : (qindex termlist = (∗ [x0,…,xn−1] ∗)
       let rec build m = (∗ 0 ≤ mn ∗)
         if (m=n
         then [ ]
         else AS.V(Symbol.symbol_of_string "x"m) :: build (m+1)
       in
       build 0
     in let xtl : (qindex termlist = build_varlist n
     in let ((x_tx_i,x_tx_j) : (qindex term × qindex termlist list × (qindex term × qindex termlist list) =
       ((List.map (fun (qv_iqstarindex list) → (∗ ∀ (q1′,…,qi,…,qn−1′) ∗)
         List.map2 (fun q → fun tx → (txqstarindex_as_qstarterm q tx)) (∗ ∀ x0,… xn−1,q′ ∗)
           qv_i xtl)
           ql_i),
         (List.map (fun (qv_jqstarindex list) → (∗ ∀ (q1′,…,qj,…,qn−1′) ∗)
           List.map2 (∗ ∀ x0,… xn−1, q′ ∗)
             (fun q → fun tx → (tx,qstarindex_as_qstarterm q tx))
             qv_j xtl)
           ql_j))
     in let ((vsl_ivsl_j) : (qindex Red.vsubstlist × (qindex Red.vsubstlist) = 
     (∗ extract the substitutions ∗)
       (List.map Red.terms_match x_tx_i,
         List.map Red.terms_match x_tx_j)
     in let ((rhs_irhs_j): ((qindex termlist × (qindex termlist)) = 
     (∗ finally build all right-hand sides, applying the substitutions ∗)
       (List.map (fun s → (Red.v_app s t_naked)) vsl_i, (∗ must not be flat!! ∗)
         List.map (fun s → (Red.v_app s t_naked)) vsl_j
     in (∗ zip the two result lists together ∗)
     List.combine rhs_i rhs_j

let build_relevant_rhss (∗ Loop around the previous function ∗)
     ((i,j): qstarindex × qstarindex)
     (visitedqqstarindex list)
     (rhsl : (qindex termlist)
     : (qindex term × qindex termlist
     = B.list_flatten_map (build_relevant_rhs (i,jvisitedqrhsl

The function one_pbisimstep is the basic iteration step for past bisimulation, refining a given partition dynamically.

tested: ok (few testcases only)


let one_pbisimstep (rl: (qindex rulelist) (ssigssignature) (rewrite_eqsqequations)
     (((unknownnonq), visitedq) : d_partition) : d_partition
     =
   let (still_unknownnew_nonq) = 
     List.partition (∗ partition unknown = Ri ∗) 
       (fun ((i,j): (qstarindex × qstarindex)) → 
         (List.for_all (∗ for all relevant pairs of right-hand sides ∗)
             (fun ((r_i,r_j) : (qindex term × qindex term)) → 
               let ((pre_s_ipre_s_j) : 
                     (qstarindex × symbollist × (qstarindex × symbollist) = 
                 (List.map extract_qstar_and_symbol_of_lhs (pre_on_rhs rl r_i), 
                 List.map extract_qstar_and_symbol_of_lhs (pre_on_rhs rl r_j))
               in
                       (
               (List.for_all 
                   (fun ((q_is_i): (qstarindex × symbol)) → (∗ ∀ qiQ ∗)
                     (List.exists 
                       (fun ((q_js_j): (qstarindex × symbol)) → (∗ ∃ qjQ ∗)
                         (qstar_and_symbol_notin_rel nonq ((q_is_i),(q_js_j))))
                       pre_s_j))
                   pre_s_i)
                 ∧
               (List.for_all 
                   (fun ((q_js_j): (qstarindex × symbol)) → 
                     (List.exists 
                       (fun ((q_is_i): (qstarindex × symbol)) → 
                         qstar_and_symbol_notin_rel nonq ((q_i,s_i), (q_j,s_j)))
                       pre_s_i))
                   pre_s_j)))
             (build_relevant_rhss (i,jvisitedq (snd (List.split rl)))))
       unknown
   in
   let states_reaped : qstarindex list = (∗ scan for unseen states (inefficient) ∗)
     B.list_remove_doublettes
       (B.list_flatten_map 
           (fun ((i,j) : qstarindex × qstarindex) → (∗ for all pairs of the relation ∗)
             (B.list_flatten_map
               (fun ((r_ir_j) : qindex term × qindex term) →
                 ( List.map extract_qstar_of_lhs (pre_on_rhs rl r_i)
                     @ List.map extract_qstar_of_lhs (pre_on_rhs rl r_j)))
               (build_relevant_rhss (ijvisitedq (snd (List.split rl)))))
           unknown)
   in let newly_detected = List.find_all (fun x → (¬ (List.mem x visitedq))) states_reaped
   in ((still_unknownnew_nonq), newly_detected)

As for one_fbisimstep and fbisimulation_states in the forward case, the function pbisimulation_states computes cum grano salis the fixpoint of one_pbisimstep.

tested: ok


let pbisimulation_states
     (rl: (qindex rulelist)
     (ssigssignature)
     (rewrite_eqsqequations)
     (((unknownnonq), visitedq) : d_partition)
     : d_partition
     = 
   let rec pbisim (∗ the inner bisimulation ∗)
       (rewrite_eqsqequations)
       (((unknownnonq), visitedq) : d_partition)
       : d_partition
       =
     let ((still_unknownnew_nonq), new_visitedq) = (∗ partition unknown ∗)
       one_pbisimstep rl ssig rewrite_eqs ((unknown,nonq), visitedq)
     in 
         match (new_nonq,new_visitedqwith 
       ([ ],[ ]) → ((still_unknownnonq),visitedq) (∗ end of iteration ∗)
     ∣ (_,[ ]) → (∗ at least no new states ∗)
         pbisim rewrite_eqs ((still_unknown,nonq@new_nonq),visitedq)
     ∣ (_x::v) → (∗ new states => new unexplored pairs of states ∗)
         let further_unknown = 
           (B.list_cross_product new_visitedq new_visitedq) @
           (B.list_cross_product new_visitedq visitedq) @
           (B.list_cross_product visitedq new_visitedq)
         in pbisim rewrite_eqs ((still_unknown@further_unknown,new_nonq@nonq),
                                 new_visitedq@visitedq)
   in pbisim rewrite_eqs ((unknown,nonq), visitedq)

Swapping relations

Next we need to take care of transforming bisimulations ∼p and ∼f into a relation usable for quotienting.


The function merge_p_f takes two relations as subsets of Qn× Qn (represented “flattenend”).11 So the input relations will be unordered, just pairs of states from Q. It is assumed that the two relations are swapping. The two relations are merged into a common relation such that result is a

  1. terminating and
  2. confluent

ground rewrite-system. Using lexicographical ordering, the termination condition is always guaranteed.12

unfinished!


We use integers representing states of Q. In order to use the lexicographic ordering of the base module, we need to adapt the ≤ on integers to the representation required there.


let int_order x y = if x<y then B.LESS else if x = y then B.EQ else B.NLESS

let order_qequations (eqnsqequations) : qequations =
   (List.find_all 
       (fun (l,r) → 
         match (B.lex_order int_order l rwith 
           B.NLESS → true
         ∣ _ → false)
       eqns)

let merge_p_f ((bisim_pbisim_f): qequations × qequations) : qequations =
       (∗ not the final version!! ∗)
       order_qequations (bisim_p @ bisim_f)

Acceleration

Next the implementation of the quotienting of the transducer. In the following, we start to work on terms that may contain “real” states from Q and not just sequences of qi(qj(…)) (in exploded form). I.e., we are working now with type qstarindex the type parameter of terms, rules, etc. Therefore, a number of conversion functions are needed. The function starterm_of_term performs one direction of the conversion, where the result is kept is in “imploded” form.

tested: ok


let rec starterm_of_term (tqindex term) : qstarindex term =
   let rec starterm_of_purerterm t =
     match t with 
       AS.V(s,i) → AS.V(s,i) (∗ since we convert the type, we must spell it out ∗)
     ∣ AS.P(s,i) → AS.P(s,i)
     ∣ AS.T(s,subterms) → AS.T(s,List.map starterm_of_purerterm subterms)
     ∣ AS.QT (AS.Q(i:qindex), ttl) → 
         raise (Failure "must not happen (starterm of term)")
   in
   let rec implode_leading_qs (alpha:qstarindex) (t:qindex term) : qstarindex term =
     match t with 
       AS.V(s,i) → AS.QT(AS.Q(alpha), AS.V(s,i), [ ])
     ∣ AS.P(s,i) → AS.QT(AS.Q(alpha), AS.P(s,i), [ ])
     ∣ AS.T(s,subterms) → 
         AS.QT(AS.Q(alpha), AS.T(sList.map starterm_of_purerterm subterms), [ ])
     ∣ AS.QT (AS.Q(i:qindex), ttl) → (∗ deeper, NO PARMS! ∗)
         implode_leading_qs (alpha@[i]) t
   in 
   match t with 
     AS.V(s,i) → AS.V(s,i) (∗ since we convert the type, we must spell it out ∗)
   ∣ AS.P(s,i) → AS.P(s,i)
   ∣ AS.T(s,subterms) → AS.T(s,List.map starterm_of_term subterms
   ∣ AS.QT (AS.Q(i:qindex), ttl) → implode_leading_qs [it

As the name implies, the following function, given an index α and a term t, produces the term qα(t).

not used


let rec wrap_qstar (qlqstarindex) (tqstarindex term) : qstarindex term =
   match ql with (∗ α × tqα(t) ∗)
     [ ] → t (∗ qє(t) = t ∗)
   ∣ _ → (AS.QT(AS.Q(ql), t, [ ]))

The normalising function normalizes the qα-states occuring within a term according to the given equations, i.e., it replaces qi(qj(…) by qnorm(ij). The term is assumed to satisfy the predicate is_rhs_term_star or that it is a left-hand side. Especially it is assumed that the states q form Q are found in t “imploded” form.

tested: ok


let rec normalise_qstarterm (rewrite_eqsqequations) (tqstarindex term
     : qstarindex term =
   match t with
   ∣ AS.V(symb,i) → t
   ∣ AS.P(symb,i) → t (∗ No parameters ∗)
   ∣ AS.T(symbtl) → 
       AS.T(symbList.map (normalise_qstarterm rewrite_eqstl)
   ∣ AS.QT(AS.Q(alpha), ttl) → 
       AS.QT(AS.Q(Red.qnorm rewrite_eqs alpha), 
             (normalise_qstarterm rewrite_eqst
             List.map (normalise_qstarterm rewrite_eqstl)

   Normalizing a transducer’s rewrite rules means, normalizing both left-hand side and right-hand side for each single rule.

Untested


let norm_transitions (rewrite_eqsqequations)
   : ( qstarindex rule list → qstarindex rule list) = 
   List.map
     (fun (l,r) → 
       (normalise_qstarterm rewrite_eqs l
         normalise_qstarterm rewrite_eqs r))

Given Q0 for T1 as list initial states, the following 2 function gives back Q0n, resp. Qn .

tested: ok
tested: ok

.
let rec build_fstart_qstars_eq (qlqindex list) (n:int) : qstarindex list = B.list_to_n ql n

let rec build_fstart_qstars_leq (qlqindex list) (n:int) : qstarindex list = 
   assert (n ≥ 1);
   if (n = 1) 
   then (build_fstart_qstars_eq ql n)
   else (build_fstart_qstars_eq ql n) @ (build_fstart_qstars_leq ql (n−1))

The next glean_transitions is an auxiliary function used in glean_T. It takes one qQ, builds terms q(f(x1,…,xn)) and finds the corresponding right-hand sides according to the given rules. This is done for a given signature Σ.

tested: ok


let glean_transitions
     (sarssignature)
     (alpha : qstarindex)
     (rl : (qindex rulelist)
     : ((qstarindex rulelist) (∗ transitions from T ∗)
     = let startterms: (qindex termlist = (∗ explode the α ∗)
       List.map (build_qstarterm alphasar
     in 
     List.map
       (fun (l,r) → (∗ we have to lift it to rules of T again ∗) 
                 (starterm_of_term l,
           starterm_of_term r))
       (Basic.list_flatten_map
           (fun x →
             List.map (fun r →
               (x,r)) (∗ build a new pair ∗)
               (Red.reduce_until rl (is_rhs_term_starx))
           startterms)

In a depth-first manner, the function glean_T takes the given “transducer” and

  1. find all new reachable q-states (starting from the initial states), and
  2. gives back all transitions it encounters. The real work is done in the inner search-procedure, basically a depth-first search.
tested: not ok for qv not empty


let glean_T 
     (sarssignature)
     (rl: (qindex rulelist) (∗ rules of T1 ∗)
     (rewrite_eqsqequations) (∗ not usesd ∗)
     (visitedqqstarindex list)
     (tlqstarindex list) (∗ list of start “terms” (q’s) ∗)
     : (((qstarindex rulelist) × (qstarindex list))
     =
     let rec search (∗ the forward exploration procedure proper ∗)
       (visitedqqstarindex list
       (tlqstarindex list) (∗ the ones to explore in forward manner ∗)
       : ((qstarindex rulelist) × (qstarindex list) =
             match tl with
       [ ] → ([ ],[ ]) (∗ Done with that, no more states to start from ∗)
     ∣ alpha::tl → (∗ check the next state from Q ∗)
         if (List.mem alpha visitedq) (∗ Have we seen it already? ∗)
         then (∗ If so, tackle the rest. ∗)
           let (rules,visitedq) = search visitedq tl
               (∗ Recur. Later, when normalizing, call search(t @ visitedq) (tl) ∗)
           in 
           (if (List.mem alpha visitedq
           then (rulesvisitedq) (∗ without normalizing: this branch ∗)
                                       (∗ is always taken. ∗)
           else (rulesalpha::visitedq))
         else 
           let ruletrans: (qstarindex rulelist = glean_transitions sar alpha rl
           in
           let qstates_to_explore : qstarindex list =
             (∗ extract the qα’s from the right-hand sides ∗)
             Basic.list_flatten_map extract_indices (snd (List.split ruletrans))
           in 
                   let (rules,visitedq) = (∗ search deeper ∗)
             search 
               (alpha::visitedq) (∗ one more visited ∗)
               (qstates_to_explore @ tl) (∗ dfs: new ones first ∗)
           in
           (ruletrans @ rulesalpha::visitedq)
     in
     let ((transitionsvisitedq): (qstarindex rulelist × qstarindex list) =
       search [ ] tl (∗ we must start internal search with the empty set of visited states ∗)
     in let new_visitedq = (∗ split out newly visited states ∗)
       snd (List.partition (fun x → List.mem x visitedqvisitedq)
     in (transitionsnew_visitedq)

Static acceleration

We start with a static version of the iterate_T-function. Static means, that set of equations used to collapse transducers is fixed as opposed to calculated on-the-fly while calculating the approximants Tn.

Basically, the function calls the function glean_T of the with Q0n which performs the forward state exploration. When returning the resulting rules are normalized and remembered. In case one layer does not give any new normalized rules, iterate_T_static stops.

As static arguments (i.e. those unchanged in the recursive call) the function takes the signature, the set Q0 of initial states of T and its rules.


let rec iterate_T_static
       (sarssignature) (∗ Σ ∗)
       (q0lqindex list) (∗ Q0 ∗)
       (rl : (qindex rulelist) (∗ rules of T1 ∗)
       (star_transitions: (qstarindex rulelist) (∗ collected transitions for Tn ∗) 
       (rewrite_eqns : qequations) (∗ equations on Q, static ∗)
       (((unknownnonq), visitedq): d_partition)
       (depthint)
       : (qstarindex rulelist
     =
   (assert (depth < 14)); (∗ Just a stopper ∗)
   let (fstart_qsqstarindex list) = build_fstart_qstars_eq q0l depth (∗ inefficient ∗)
   in let ((transitionsnew_visitedq) : (qstarindex rulelist × qstarindex list) =
       glean_T sar rl rewrite_eqns visitedq fstart_qs
   in let ntransitions = norm_transitions rewrite_eqns transitions
     in let (star_transitionsnew_transitions) = (∗ find the new transitions ∗)
       B.list_merge star_transitions ntransitions
     in
         match new_transitions with
     [ ] → star_transitions
   ∣ _ → (∗ one level deeper ∗)
       iterate_T_static sar q0l rl
         star_transitions
         rewrite_eqns (∗ static! ∗)
         ((unknown,nonq), visitedq) (∗ unchanged yet ∗)
         (depth + 1)

Dynamic acceleration

Next the dynamic variant to calculating T, a generalization of the static version iterate_T_static. This time, the equivalences used for quotienting are calculated on-the-fly.

To calculate T, iterate_T loops trying to find new transitions during the exploration of the approximations Tn. If no new transitions are found, the iteration stops.13

For each depth n, it starts with the initial states of Tn. Starting from this list, all transitions and all reachable states are calculated with the help of glean_T.

Under change.

The first 3 arguments doesn’t change in the iterations, the latter 4 change in the loop. The star_transitions are the currently collected transitions of Tn, where n is the depth of the loop (the last parameter). Initially the list of transitions is empty. As an invariant —of less importance— is that there are no duplicated rules.

The parameter rewrite_eqns keeps the rewrite system on Q. Initially, the rewrite-system is empty. As invariant we maintain that rewrite_eqns is strongly-normalizing and terminating, and additionally that it is “spanned” by a pair of future and past bisimulation (cf. [DLS02]). A combined invariant of the list of transitions for Tn and the rewrite-equations is, that the rewrite-equations are in (unique) normal form wrt. the equations. The next parameter is currently not (yet) really used.14

The depth denotes the iteration of T which is about to be explored in the current call of the function. Therefore, the initial depth will be 1.

stub

In the current (transient) state of affairs, we don’t calculate Tn, at least not explicitely, we concentrate on the bisimulation.

Unlike in the previous static version we don’t “glean” any transitions, we just look at the bisimulations as described in the paper.

The depth is the exponentiation currently explored.


let rec iterate_T
     (sarssignature) (∗ Σ ∗)
     (q0lqindex list) (∗ Q01 ∗)
     (rl : qindex rule list) (∗ rules of T1 ∗)
     (((unknownnonq), visitedq): d_partition)
     (depthint)
     ((rewrite_eqnsqequations), (rules_starqstarindex rule list))
     =
   print_string ("iterate_T: exploring T^"^(string_of_int depth));
   print_newline();
   if (depth < 5) (∗ just a stopper ∗)
   then
     (
       let depth_string = string_of_int depth
       in let (fstart_qsqstarindex list) = (∗ Q0n ∗)
       build_fstart_qstars_leq q0l depth 
     in 
           let (((unknown,nonq),visitedq) : d_partition) = 
         fbisimulation_states_fromscratch 
           rl sar (∗ rules + signature of T1 ∗)
           rewrite_eqns (∗ currently static ∗)
           fstart_qs
       in
           iterate_T sar q0l rl
         ((unknown,nonq), visitedq) (∗ unchanged yet ∗)
         (depth + 1) 
         (rewrite_eqnsrules_star)) (∗ unchanged ∗)
   else 
     (rewrite_eqnsrules_star)

Dynamic: comparing rules

The following calculates T by collecting the rules.


let rec iterate_T_rules
     (sarssignature) (∗ Σ ∗)
     (q0lqindex list) (∗ Q01 ∗)
     (rl : qindex rule list) (∗ rules of T1 ∗)
     (((unknownnonq), visitedq): d_partition)
     (depthint)
     ((rewrite_eqnsqequations), (rules_starqstarindex rule list))
     =
   print_string ("iterate_T_rules: exploring T^"^(string_of_int depth));
   print_newline();
   if (depth < 5) (∗ stopper ∗)
   then
     (
       let depth_string = string_of_int depth
       in let (fstart_qsqstarindex list) = (∗ Q0n ∗)
       build_fstart_qstars_eq q0l depth 
     in 
     print_string "Q^n = ";
     print_qstarindexlist fstart_qs;
       let ((rules_nnew_visitedq) : (qstarindex rulelist × qstarindex list) =
         glean_T sar rl rewrite_eqns visitedq fstart_qs
       in 
       print_endline ("\nrules found in T^" ^ depth_string ^ "  (rules_n)");
       Io.print_startransitions rules_n;
       print_endline("\nnew alphas found in T^" ^ depth_string ^ "  (new_visitedq)");
       Io.print_intlistlist new_visitedq;
       let normed_rules_n = norm_transitions rewrite_eqns rules_n
       in 
       print_endline("\nnormed rules found in T^" ^ depth_string);
       Io.print_startransitions normed_rules_n;
       let (rules_starrules_new) = (∗ find the new transitions ∗)
         B.list_merge rules_star normed_rules_n
       in
       match rules_new with
         [ ] → (rewrite_eqnsrules_new)
       ∣ _ → (∗ one level deeper ∗)
           iterate_T_rules sar q0l rl
             ((unknown,nonq), visitedq) (∗ unchanged yet ∗)
             (depth + 1) 
             (rewrite_eqns,rules_star))
   else 
     (rewrite_eqnsrules_star)

let star (transdqindex mtt) = transd

  

stub



Previous Up Next