RIS.equiv_stacks: dynamic properties of the binding transducer.

Set Implicit Arguments.

Require Export transducer.

Section s.
Context {atom X: Set}{𝐀 : Atom atom} {𝐗 : Alphabet 𝐀 X}.

Static equivalence

We may define the following relation on stacks.

Fixpoint equiv_stacks s1 s2 :=
  match s1 with
  | [] ⇒ s2 ✓
  | (a,b)::s1 ⇒ (s2 ⊨ a ↦ b) ∧ equiv_stacks s1 (s2 ⊖ (a,b))
  end.
Infix " == " := equiv_stacks (at level 80).

This relation may easily be translated as a boolean relation.

Fixpoint equiv_stacksb s1 s2 :=
  match s1 with
  | [] ⇒ prj1 s2 =?= prj2 s2
  | (a,b)::s1 ⇒ pairedb s2 a b && equiv_stacksb s1 (s2 ⊖ (a,b))
  end.

equiv_stacksb reflects equiv_stacks.

Lemma equiv_stacksb_spec s1 s2: s1 == s2 ↔ equiv_stacksb s1 s2 = true.

We will now show that equiv_stacks is an equivalence relation. Reflexivity is straightforward.

Lemma equiv_stacks_Reflexive s : s == s.

Two equivalent stacks validate the same pairs.

Lemma equiv_stacks_paired s1 s2 a b : s1 == s2 → (s1 ⊨ a ↦ b ) ↔ (s2 ⊨ a ↦ b ).

If two stacks are equivalent, then either both are accepting or none of them are.

Lemma equiv_stacks_Accepting s1 s2 : s1 == s2 → s1 ✓ ↔ s2 ✓.

Two accepting stacks are always equivalent.

Lemma Accepting_equiv_stacks s1 s2 : s1 ✓ → s2 ✓ → s1 == s2.

We may therefore show that == is a symmetric relation.

Lemma equiv_stacks_Symmetric s1 s2 : s1 == s2 → s2 == s1.

The operation rmfst is monotonic with respect to ==.

Global Instance equiv_stacks_rmfst :
Proper (Logic.eq ==> equiv_stacks ==> equiv_stacks) rmfst.

We these facts established we can prove that == is transitive.

Lemma equiv_stacks_Transitive s1 s2 s3 : s1 == s2 → s2 == s3 → s1 == s3.

Having proved reflexivity, symmetricity and transitivity, we now know that == is indeed an equivalence relation.

Global Instance equiv_stacks_equivalence : Equivalence equiv_stacks.

cons is monotonic with respect to ==.

Global Instance equiv_stacks_cons :
Proper (Logic.eq ==> equiv_stacks ==> equiv_stacks) cons.

If two stacks are equivalent, then their associated image functions are extensionally equivalent.

Global Instance equiv_stacks_image :
Proper (equiv_stacks ==> Logic.eq ==> Logic.eq) image.

It follows that two equivalent stacks yield equivalent permutations for any list.

Global Instance equiv_stacks_var_perm :
Proper (Logic.eq ==> equiv_stacks ==> sequiv) var_perm.

Definitions

Notation " s1 -- α -->> s2 " := (path (fst α) (snd α) s1 s2) (at level 80).
Notation " s1 -- α ---> s2 " := (step s1 (fst α) (snd α) s2) (at level 80).

As will be shown later on, the pair of words w1 s,w2 s characterises the stack s.

Definition w1 (s : stack) : word := map close (prj1 s).
Definition w2 (s : stack) : word := map close (prj2 s).
Definition 𝐰 (s : stack) := (w1 s ,w2 s ).

We define bissimilarity of stacks by coinduction, saying that s1∼s2 holds if for every pair of letters l1,l2, if s1 can perform one transition labelled with l1|l2 to s3 then s2 can can follow a transition with the same label to reach s4 with s3∼s4, and conversely.

Reserved Notation " s1 ∼ s2 " (at level 80).
CoInductive bissimilar : relation stack :=
| prog s1 s2 :
    (∀ α, (∀ s3, s1 -- α ---> s3 → ∃ s4, s2 --α ---> s4 ∧ s3 ∼ s4 )
          ∧ (∀ s4, s2 --α ---> s4 → ∃ s3, s1 --α ---> s3 ∧ s3 ∼ s4 ))
    → s1 ∼ s2
where " s1 ∼ s2 " := (bissimilar s1 s2).

Similarity is defined analogously.

Reserved Notation " s1 ≺ s2 " (at level 80).
CoInductive similar : relation stack :=
| prog2 s1 s2 :
(∀ α, (∀ s3, s1 --α ---> s3 → ∃ s4, s2 --α ---> s4 ∧ s3 ≺ s4))
→ s1 ≺ s2
where " s1 ≺ s2 " := (similar s1 s2).

We consider here languages to be sets of pairs of words, i.e. predicates over words×words.

Definition lang := (word × word)%type → Prop.

Two languages are equivalent if they contain the same words.

Global Instance eq_sem : SemEquiv lang := fun L M ⇒ ∀ σ, L σ ↔ M σ.

The language L is smaller that the language M if every word in L belongs to M.

Global Instance inf_sem : SemSmaller lang := fun L M ⇒ ∀ σ, L σ → M σ.

The semantics of a stack s is the set of pairs u,v such that there is a path from s to some accepting stack labelled with u,v.

Definition semantics s : lang := fun σ ⇒ (∃ s', s' ✓ ∧ s --σ -->> s').
Notation " ⟦ s ⟧ " := (semantics s).

Lemmas

equiv_stacks

fun s ⇒ δt s u v preserves the relation ==.

Global Instance equiv_stacks_δt :
Proper (equiv_stacks ==> Logic.eq ==> Logic.eq ==> equiv_stacks) δt.

If s==s', then u,v is compatible with s if and only if s' is.

Global Instance equiv_stacks_compatible :
Proper (equiv_stacks ==> Logic.eq ==> Logic.eq ==> Logic.eq) compatible.

Characteristic words

The pair w1 s,w2 s belongs to the semantics of s.

Lemma w_path s : ⟦s ⟧ (𝐰 s).

If w1 s1,w2 s1 is in the semantics of s2, then s1==s2.

Lemma w_equiv_stacks s1 s2 :
⟦s2 ⟧ (𝐰 s1) → s1 == s2.

Bissimilarity

Bissimilarity is an equivalence relation.

Global Instance bissimilar_equivalence : Equivalence bissimilar.

Although we have defined bissimilarity in terms of transitions, it may be naturally extended to paths.

Lemma bissimilar_path s1 s2 σ s3 :
s1 ∼ s2 → s1 --σ -->> s3 → ∃ s4, s2 --σ -->> s4 ∧ s3 ∼ s4.

In fact s1 is bissimilar to s2 exactly when for every pair of words u,v, there is a path labelled with u|v from s1 if and only if there is one from s2.

Lemma bissimilar_alt s1 s2 :
s1 ∼ s2 ↔ ∀ σ, (∃ s, s1 --σ -->> s ) ↔ (∃ s, s2 --σ -->> s ).

Bissimilar stacks are equivalent with respect to acceptance.

Lemma bissimilar_accepting s1 s2 : s1 ∼ s2 → s1 ✓ → s2 ✓.

Static equivalence implies bissimilarity.

Lemma equiv_stacks_bissimilar s1 s2 : s1 == s2 → s1 ∼ s2.

If s1 and s2 are bissimilar, then the semantics of s2 contains w1 s1,w2 s2.

Lemma bissimilar_w s1 s2 :
s1 ∼ s2 → ⟦s2 ⟧ (𝐰 s1).

Similarity

Bissimilarity implies similarity.

Lemma bissimilar_similar s1 s2 : s1 ∼ s2 → s1 ≺ s2.

Similarity implies static equivalence.

Lemma similar_equiv_stacks s1 s2 : s1 ≺ s2 → s1 == s2.

Semantics

Bissimilarity implies semantic equivalence.

Lemma bissimilar_eq_sem s1 s2 : s1 ∼ s2 → ⟦s1 ⟧ ≃ ⟦s2 ⟧.

Semantic equivalence implies semantic inclusion.

Lemma eq_lang_incl_sem s1 s2 : ⟦s1 ⟧ ≃ ⟦s2 ⟧ → ⟦s1 ⟧ ≲ ⟦s2 ⟧.

Semantic inclusion of s1 in s2 implies that w1 s1,w2 s1 is in the semantics of s2.

Lemma incl_sem_w s1 s2 : ⟦s1 ⟧ ≲ ⟦s2 ⟧ → ⟦s2 ⟧ (𝐰 s1).

End s.