Library LangAlg.terms_w_terms

In this module we describe the reductions between terms (type 𝐓), primed weak terms (𝐖') and series-parallel terms (𝐒𝐏).

Set Implicit Arguments.

Require Export terms w_terms.
Open Scope term_scope.
Section s.
Variable X : Set.
Variable dec_X : decidable_set X.

We start by defining a conversion function from series parallel terms over a duplicated alphabet into terms over the original alphabet.

  Fixpoint 𝐒𝐏 _to_𝐓 (e : 𝐒𝐏 (@X' X)) : 𝐓 X :=
    match e with
    | 𝐒𝐏 _var (a,true ) ⇒ 𝐓 _var a
    | 𝐒𝐏 _var (a,false ) ⇒ 𝐓 _cvar a
    | e ⨾ f ⇒ 𝐒𝐏 _to_𝐓 e ⋅ 𝐒𝐏 _to_𝐓 f
    | e ∥ f ⇒ 𝐒𝐏 _to_𝐓 e ∩ 𝐒𝐏 _to_𝐓 f
    end.

Using this function, we build a translation from primed weak terms into terms.

  Definition 𝐖'_to_𝐓 (e : 𝐖') : 𝐓 X:=
    match e with
    | (exist _ (None ,A) _) ⇒ ⟨map fst A⟩
    | (exist _ (Some u,A) _ ) ⇒
      ⟨map fst A⟩ ⋅ 𝐒𝐏 _to_𝐓 u
    end.

For the converse direction, we directly translate terms into primed weak terms.

  Fixpoint 𝐓 _to_𝐖' (e : 𝐓 X) : 𝐖' :=
    match e with
    | 1 ⇒ 𝟭'
    | 𝐓 _var a ⇒ (exist _ (Some (𝐒𝐏 _var (a,true )),[]) (@balanced_nil X))
    | 𝐓 _cvar a ⇒
      (exist _ (Some (𝐒𝐏 _var (a,false )),[]) (@balanced_nil X))
    | e ⋅ f ⇒ (𝐓 _to_𝐖' e ) ⊗' (𝐓 _to_𝐖' f)
    | e ∩ f ⇒ (𝐓 _to_𝐖' e ) ⊕' (𝐓 _to_𝐖' f)
    end.

The translation from terms to primed weak terms is monotone with respect to the ordering of 𝐖'.

The translation from series-parallel terms into terms is size preserving.

The translation from terms to primed weak terms reduces the size.

From weak terms to terms the size may increase, but is bounded as follows:

We may recover the variables of a term by map the first projection to the set of variables of its translation in 𝐖'.

Going from primed weak terms to terms and back yields an equivalent 𝐖'-term.

We can relate the variables of a series parallel term (over the duplicated alphabet) with the variables of its corresponding term.

The translation from primed weak terms to terms is monotone.

Going from terms to primed weak terms and back yields an equivalent term.

The translation from primed weak terms into terms is a reduction, in the sense that two 𝐖' terms are ordered if and only if their images are ordered.

Similarly, the translation from terms to primed weak terms is a reduction.

Theorem 𝐓 _to_𝐖'_inf_iff e f : e ≤ f ↔ 𝐓 _to_𝐖' e ≤ 𝐓 _to_𝐖' f.
End s.
Close Scope term_scope.

Languages

𝐒𝐏_to_𝐓 is language preserving, for interpretations of assignments of the shape Ξ σ.

𝐖'_to_𝐓 is language preserving, for interpretations of assignments of the shape Ξ σ.

So is 𝐓_to_𝐖', under similar hypotheses.