Previous Up Next

Module Sanalysis

open Absynt

A few auxiliary functions. Left-hand sides of rules are terms from Q(Σ(X)), which unique variables. Right-hand sides, on the other hand, are terms from TΣ(Q(X)).

both checked: ok

Note that closed terms are correct right-hand sides, but a term in which a variabe occurs not preceded by a state form Q is not a correct right-hand side.5
let is_lhs (t: α term) : bool = 
   match t with 
     V(_,_) → false
   ∣ P(_,_) → false 
   ∣ T(_,subterms) → false 
   ∣ QT (Q iT(s,tl),_) → (∗ NO PARMS ∗)
       (List.for_all (∗ immediate subterms must be variables ∗)
           (fun t → 
             match t with 
               V(_) → true
             ∣ _ → false)
           tl)
   ∣ _ → false

let rec is_rhs (t: α term) = 
   match t with
     V(_,_) → false (∗ no variables except preceded by a state ∗)
   ∣ P(_,_) → false 
   ∣ T(_,subterms) → 
       List.for_all is_rhs subterms
   ∣ QT (Q iV(_,_), _) → true 
   ∣ QT (Q i_ , _) → false

A pair of terms is a rule, if the first term is a correct left-hand side and the second a right-hand side. Besides that, the variables mentioned in the left-hand term must be unique, and all variables mentioned in the term on the right-hand side must appear in the left-hand side. It is not required that the variables on the right-hand side are unique; this is necessary only for linear transducers and will be checked separately.
let rec extract_vars (t: α term) : vname list = 
   match t with
     V(s,i) → [(s,i)]
   ∣ P(_,_) → [ ]
   ∣ T(_,subterms) → 
       Basic.list_flatten_map extract_vars subterms
   ∣ QT (_t,_) → extract_vars t

let is_rule (t1,t2) = (∗

tested: ok

∗)
   if (¬ ((is_lhs t1) ∧ (is_rhs t2)))
   then false
   else 
     let (vl1,vl2) = (extract_vars t1extract_vars t2)
     in 
     if (¬ (Basic.list_has_unique_entries vl1))
     then false
     else List.for_all (fun v → (List.mem v vl1)) vl2

A term is well-typed with respect to the declaration of arities of symbols and of the states, if each symbols uses the correct number of subterms and the same for states. Currectly, states must have arity of exactly 1.


A transducer is well-typed, if the symbols’s arities are used according to their declaration, if the initial states are a subset of the states, and if the rules as pairs of terms adhere to the syntactic restrictions for left-hand and right-hand sides. For uniqueness, we check only the two declaration lists, the list of states and initial states may contain doublettes. Currently no macro-tree transducer are supported, so well-typed means, that the arities of the states from Q is 1 and that no parameters are used. For sake of efficiency, both are checked by the same procedure.

tested: ok

. If a term uses a symbol which is not declared, an error is raised by the association lists
let rec is_welltyped ((qsigssig) : α signature) (t: α term) : bool = 
   match t with
     V(s,i) → true 
   ∣ P(_,_) → true 
   ∣ T(s,subterms) → 
       (((List.assoc s ssig) = List.length subterms)
           ∧
         List.for_all (is_welltyped (qsigssig)) subterms)
   ∣ QT (_t,_) → (is_welltyped (qsigssigt)

let is_wellformed ((_,(qsig,ssig), slislrl): α mtt) = 
   (∗ uniqueness of the symbols ∗)
   let ql = (fst (List.split qsig)) (∗ declared state indices ∗)
   in let syms = (fst (List.split ssig)) (∗ declared symbols ∗)
   in 
   if (¬ (Basic.list_has_unique_entries (ql)))
   then raise (Failure "state list in declaration not unique")
   else if (¬ (Basic.list_has_unique_entries syms))
   then raise (Failure "symbols in declaration not  unique")
   else if (¬ (List.for_all 
                   (fun is → (List.mem is sl))
                   isl))
   then raise (Failure ("illegal initial state"))
   else (∗ next we test the rules for well-formedness ∗)
   if (¬ (List.for_all is_rule rl))
   then false (∗ Now: “typechecking” ∗)
   else 
     let (terms_l,terms_r) = List.split rl
     in
     ((List.for_all (is_welltyped (qsigssig)) terms_l)
         ∧
       ((List.for_all (is_welltyped (qsigssig)) terms_r)))

To test, whether T is a word-transducer, we simply check the arities of the symbols together with well-typedness (I.e., a word transducers is guaranteed to be well-formed.

tested: ok


let is_wordtransducer (t: α mtt) = 
   if (¬ (is_wellformed t)) 
   then false
   else 
     let (_,(_,ssig),_,_,_) = t
     in List.for_all (fun (_,a) → ((a = 0) ∨ (a = 1))) ssig 

A well-formed transducer is called linear, if for each rule, no variable occurs more than once on the rule’s right-hand side.

Tested: ok


let is_linear (t : α mtt) = 
   if (¬ (is_wellformed t))
   then false
   else 
     let (_,_,_,_,rl) = t
     in 
     List.for_all 
       (fun t → (Basic.list_has_unique_entries (extract_vars t)))
       (snd (List.split rl))

   the right-hand sides


Previous Up Next