RIS.transducer: definition and properties of the binding transducer.

Set Implicit Arguments.

Require Export stacks words.

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

Transducer

Definition

The predicate s ⊣ l1 | l2 ↦ s' encodes the transition function of the transducer. It holds when there exists a transition in the transducer from state s to state s' labelled with letters l1|l2.
Definition step (s : stack) (l1 l2 : letter) (s' : stack) :=
  match (l1,l2) with
  | (⟨a,⟨b) β‡’ s' = (a,b)::s
  | (a⟩,b⟩) β‡’ (s ⊨ a ↦ b) ∧ s' = s βŠ– (a,b)
  | (var x,var y) β‡’ s' = s ∧ βˆƒ p, y = pβˆ™x ∧ βˆ€ a, a ∈ ⌊xβŒ‹ β†’ s ⊨ a ↦ pβˆ™a
  | _ β‡’ False
  end.
Notation " s ⊣ l1 | l2 ↦ s' " := (step s l1 l2 s') (at level 80).

The predicate s ⊣ u | v β€… s' encodes paths in the transducer. It holds when there exists a path in the transducer from state s to state s' labelled with the words u|v.
Reserved Notation " s ⊣ u | v β€… s' " (at level 80).
Inductive path : word β†’ word β†’ stack β†’ stack β†’ Prop :=
| pathΟ΅ s : s ⊣ [] | [] β€… s
| pathl s2 u v l1 l2 s1 s3 :
    s1 ⊣ l1 | l2 ↦ s2 β†’ s2 ⊣ u | v β€… s3 β†’ s1 ⊣ l1::u | l2::v β€… s3
where " s ⊣ u | v β€… s' " := (path u v s s').
Hint Constructors path.

The function Ξ΄t: computing a path in the transducer

compatible s u v returns true if and only if there exists s' such that s⊣u|vβ€…s'.
Fixpoint compatible s u v :=
  match (u,v) with
  | ([],[]) β‡’ true
  | ([],_) | (_,[]) β‡’ false
  | (⟨a::u,⟨b::v)β‡’ compatible ((a,b)::s) u v
  | (a⟩::u,b⟩::v)β‡’
    if (pairedb s a b)
    then compatible (sβŠ–(a,b)) u v
    else false
  | (var x::u,var y::v)β‡’
    match var_perm' ⌊xβŒ‹ s with
    | None β‡’ false
    | Some p β‡’ (pβˆ™x =?= y)&&(compatible s u v)
    end
  | (_::_,_::_) β‡’ false
  end.

If s⊣u|vβ€…s', then Ξ΄t s u v returns s'. Otherwise, Ξ΄t s u v returns []. This implies that there is at most one path from s labelled with u|v.
Fixpoint Ξ΄t s u v :=
  match (u,v) with
  | ([],[]) β‡’ s
  | ([],_) | (_,[]) β‡’ []
  | (⟨a::u,⟨b::v)β‡’ Ξ΄t ((a,b)::s) u v
  | (a⟩::u,b⟩::v)β‡’
    if (pairedb s a b)
    then Ξ΄t (sβŠ–(a,b)) u v
    else []
  | (var x::u,var y::v)β‡’
    match var_perm' ⌊xβŒ‹ s with
    | None β‡’ []
    | Some p β‡’
      if (pβˆ™x =?= y)
      then Ξ΄t s u v
      else []
    end
  | (_::_,_::_) β‡’ []
  end.

Ltac case_var s x y :=
  let p := fresh "p" in
  let e := fresh "e" in
  case_eq (var_perm' ⌊xβŒ‹ s);
  [intros p e;destruct_eqX (pβˆ™x) y|intros e].

There is a path from s1 to s2 labelled with u|v if and only if u,v is compatible with s1 and s2 is Ξ΄t s1 u v.
Theorem Ξ΄t_compatible_spec s1 u v s2 :
  Ξ΄t s1 u v = s2 ∧ compatible s1 u v = true ↔ s1 ⊣ u|v β€… s2.

Corollary Ξ΄t_path s u v : compatible s u v = true ↔ s ⊣ u|v β€… Ξ΄t s u v.

When u,v is not compatible with s, we set Ξ΄t s u v to be the empty list. This choice of a default value is arbitrary.
Lemma compatible_false s u v : compatible s u v = false β†’ Ξ΄t s u v = [].

Elementary properties

It is straightforward that a path of length one is exactly a step.
Remark path_single_letter s1 l1 l2 s2 :
  s1 ⊣ [l1] | [l2] β€… s2 ↔ s1 ⊣ l1 | l2 ↦ s2.

The transition predicate commutes with permutation actions.
Fact nom_step p s1 s2 l1 l2 :
  s1 ⊣ l1 | l2 ↦ s2 β†’ p βˆ™ s1 ⊣ pβˆ™l1 | pβˆ™l2 ↦ pβˆ™s2.

Corollary nom_path p s1 s2 u v :
  s1 ⊣ u | v β€… s2 β†’ p βˆ™ s1 ⊣ pβˆ™u | pβˆ™v β€… pβˆ™s2.

Corollary nom_compatible p s u v :
  compatible s u v = compatible (pβˆ™s) (pβˆ™u) (pβˆ™v).

Corollary nom_Ξ΄t p s u v :
  pβˆ™(Ξ΄t s u v) = Ξ΄t (pβˆ™s) (pβˆ™u) (pβˆ™v).

If s is accepting, then for any word u there is an accepting stack s' such that s ⊣ u | u β€… s'.
Lemma path_id_Accepting u : βˆ€ s, s βœ“ β†’ (Ξ΄t s u u) βœ“.

Lemma path_id_compatible u : βˆ€ s, s βœ“ β†’ compatible s u u = true.

Corollary path_id s u : s βœ“ β†’ βˆƒ s', s'βœ“ ∧ s ⊣ u | u β€… s'.

If there is a path from labelled with u|v, then u and v have the same length.
Lemma path_length_word u v s1 s2 : s1 ⊣ u | v β€… s2 β†’ ⎒uβŽ₯ = ⎒vβŽ₯.

If u1 and v1 have the same length, then u1++u2,v1++v2 is compatible with s if and only if u1,v1 is compatible with s and u2,v2 is compatible with Ξ΄t s u1 v1.
Proposition compatible_app u1 u2 v1 v2 s :
  βŽ’u1βŽ₯ = ⎒v1βŽ₯ β†’
  compatible s (u1++u2) (v1++v2) = (compatible s u1 v1)
                                     && compatible (Ξ΄t s u1 v1) u2 v2.

If u1,v1 is compatible with s then Ξ΄t s (u1++u2) (v1++v2) may be computed as Ξ΄t (Ξ΄t s u1 v1) u2 v2.
Proposition Ξ΄t_app u1 u2 v1 v2 s :
  compatible s u1 v1 = true β†’ Ξ΄t s (u1++u2) (v1++v2) = Ξ΄t (Ξ΄t s u1 v1) u2 v2.

If there is a path labelled with u1++u2|v1++v2, and if u1 and v1 have the same length, then it can be factored as a path labelled with u1|v1 followed by one with label u2|v2.
Corollary path_decompose_app u1 u2 v1 v2 s1 s2 :
  (s1 ⊣ u1++u2 | v1++v2 β€… s2) β†’ ⎒u1βŽ₯ = ⎒v1βŽ₯ β†’
  βˆƒ s3, s1 ⊣ u1 | v1 β€… s3 ∧ s3 ⊣ u2 | v2 β€… s2.

Corollary path_letter u l v s1 s2 :
  (s1 ⊣ u++[l] | v β€… s2) β†’
  βˆƒ v' l' s3, v = v' ++ [l'] ∧ s1 ⊣ u | v' β€… s3 ∧ s3 ⊣ l | l' ↦ s2.

If we know s2 to be accepting, we may simplify image (s1++s2) a, var_perm x (s1++s2), pairedb (s1++s2) a b, compatible (s1++s2) u v. Also, Ξ΄t (s1++s2) u v is accepting if and only if Ξ΄t s1 u v is.
Proposition image_app_Accepting s1 s2 :
  s2 βœ“ β†’ βˆ€ a, image (s1++s2) a = image s1 a.

Corollary var_perm_app_Accepting s1 s2 x :
  s2 βœ“ β†’ var_perm x (s1++s2) = var_perm x s1 .

Lemma pairedb_app_Accepting s1 s2 :
  s2 βœ“ β†’ βˆ€ a b, pairedb (s1++s2) a b = pairedb s1 a b.

Proposition compatible_app_Accepting s1 s2 u v :
  s2 βœ“ β†’ compatible (s1++s2) u v = compatible s1 u v.

Proposition Ξ΄t_app_Accepting s1 s2 u v :
  s2 βœ“ β†’ Ξ΄t (s1++s2) u v βœ“ ↔ Ξ΄t s1 u v βœ“.

Corollary path_app_Accepting s1 s2 u v s3 :
  s2 βœ“ β†’ s1 ⊣ u | v β€… s3 β†’ βˆƒ s4, s1++s2 ⊣ u | v β€… s4 ∧ (s3 βœ“ β†’ s4 βœ“).

We can flip a path with label u|v into a path with label v|u.
Lemma step_sym a b s1 s2 : s1 ⊣ a | b ↦ s2 β†’ s1` ⊣ b | a ↦ s2`.

Corollary path_sym s u v s' : s ⊣ u | v β€… s' ↔ (s`) ⊣ v | u β€… (s'`).

Corollary compatible_flip s u v : compatible (s`) u v = compatible s v u.

Corollary Ξ΄t_flip s u v : Ξ΄t (s`) u v = (Ξ΄t s v u)`.

We can compose a path with label u|v with a path with label v|w to get a path with label u|w, if their starting points are compatible.
Lemma step_mix l1 l2 l3 s1 s2 s3 s4 :
  prj2 s1 = prj1 s3 β†’ s1 ⊣ l1 | l2 ↦ s2 β†’ s3 ⊣ l2 | l3 ↦ s4 β†’
  (s1 β‹ˆ s3) ⊣ l1 | l3 ↦ (s2 β‹ˆ s4) ∧ prj2 s2 = prj1 s4.

Corollary path_mix u v w s1 s2 s3 s4 :
  prj2 s1 = prj1 s3 β†’ (s1 ⊣ u | v β€… s2) β†’ (s3 ⊣ v | w β€… s4) β†’
  prj2 s2 = prj1 s4 ∧ (s1 β‹ˆ s3) ⊣ u | w β€… (s2 β‹ˆ s4).

Notice that paths are deterministic, in the sense that given a starting point s and a label u|v, there is at most one stack s' such that s⊣ u | v β€…s'.
Remark step_det a b s s1 s2 : s ⊣ a | b ↦ s1 β†’ s ⊣ a | b ↦ s2 β†’ s1 = s2.

Remark path_det u v s s1 s2 : s ⊣ u | v β€… s1 β†’ s ⊣ u | v β€… s2 β†’ s1 = s2.

We can compose a path from s1 to s2 and one from s2 to s3 to get a path from s1 to s3.
Lemma path_app u1 u2 v1 v2 s1 s2 s3 :
  s1 ⊣ u1 | v1 β€… s2 β†’ s2 ⊣ u2 | v2 β€… s3 β†’ s1 ⊣ u1++u2 | v1++v2 β€… s3.

Binding power

If s ⊣ u | v β€… s', we can relate the number of occurrences of atoms in s and s' with the binding power of u and v with respect to a.
Proposition stack_binding a u s s' :
  (s ⊣ u | u β€… s') β†’
  nb a (prj1 s') = (nb a (prj1 s) - d_binding (𝗙 a u)) + c_binding (𝗙 a u).

Corollary stack_binding_both u v s s' :
  (s ⊣ u | v β€… s') β†’
  βˆ€ a,
    nb a (prj1 s') = (nb a (prj1 s) - d_binding (𝗙 a u)) + c_binding (𝗙 a u)
    βˆ§
    nb a (prj2 s') = (nb a (prj2 s) - d_binding (𝗙 a v)) + c_binding (𝗙 a v).

Using these, we can compute the size of the target stack from the c-binding power of u.
Lemma size_stack u v s :
  [] ⊣ u | v β€… s β†’ ⎒sβŽ₯ = sum (fun a β‡’ c_binding (𝗙 a u)) {{⌊uβŒ‹}}.

Applying permutations on one component

We introduce a new operation. p ⧓ s is the stack obtained by replacing every pair (a,b) in s with (a,pβˆ™b).
Definition mixp p s : stack:= (prj1 s) βŠ— (pβˆ™prj2 s).
Infix "⧓" := mixp (at level 50).

Remark mixp_fst p l : prj1 (p ⧓ l) = prj1 l.

Remark mixp_snd p l : prj2 (p ⧓ l) = prj2 (pβˆ™l).

Remark mixp_snd_bis p l : prj2 (p ⧓ l) = pβˆ™prj2 l.

Remark mixp_cons p a b l : p ⧓ ((a,b)::l) = (a,pβˆ™b)::p ⧓ l.

Remark mixp_app p l m : p ⧓ (l++m) = p ⧓ l ++ p ⧓ m.

Remark mixp_absent p l a b : absent (p⧓l) a b ↔ absent l a (pβˆ—βˆ™b).

min_occ a u is equal to d_binding (𝗙 a u) if the boolean component of 𝗙 a u is false, and d_binding (𝗙 a u)+1 otherwise.
Definition min_occ a v :=
  match 𝗙 a v with (m,true,_) β‡’ S m | (m,_,_) β‡’ m end.

Remark min_occ_app a u v : min_occ a u ≀ min_occ a (u++v).

This is the technical lemma needed to prove that the law Ξ±Ξ± holds for stacks. More precisely, we want to show that if b #Ξ± u and a #Ξ± u then there is a path from the empty stack to some accepting stack labelled with u | [(a,b)]βˆ™u. We generalise the statement by changing a,b #Ξ± u with a permutation p such that βˆ€ a, Β¬ a #Ξ± u β†’ p βˆ™ a = a.
Intuitively, one might think that the following holds: s ⊣ u | v β€… s' β†’ p ⧓ s ⊣ u | pβˆ™v β€… p⧓s'. Unfortunately, this is not true in general, consider for instance [] ⊣ a⟩ | a⟩ β€… [].
For this reason we need to require that βˆ€ a, Β¬ a #Ξ± v β†’ p βˆ™ a = a. However, while the statement becomes true in this case, it is not suitable for induction. Thus we assume the stronger condition βˆ€ a, p βˆ™ a β‰  a β†’ min_occ a v ≀ nb a (prj2 s).
Lemma perm_path_mixp p u v s s' :
  (βˆ€ a, p βˆ™ a β‰  a β†’ min_occ a v ≀ nb a (prj2 s)) β†’ (s ⊣ u | v β€… s') β†’
  p ⧓ s ⊣ u | pβˆ™v β€… p⧓s'.

Corollary Ξ±fresh_perm_path p u v s s' :
  (βˆ€ a, Β¬ a #Ξ± v β†’ p βˆ™ a = a) β†’ s ⊣ u | v β€… s' β†’ p ⧓ s ⊣ u | pβˆ™v β€… p ⧓ s'.

Corollary Ξ±fresh_perm_path_nil p u :
  (βˆ€ a, Β¬ a #Ξ± u β†’ p βˆ™ a = a) β†’ βˆƒ s, [] ⊣ u | pβˆ™u β€… s ∧ s βœ“.

Main result

Completeness

It is now fairly routine to check that whenever u and v are alpha-equivalent, there is a path labelled with u|v from the empty stack to some accepting stack.
Theorem Ξ±equiv_path u v : u ≑ v β†’ βˆƒ s, [] ⊣ u | v β€… s ∧ s βœ“.

Soundness

To prove completeness, we will proceed by induction on the length of the path, focusing on the last step:
  • if []⊣[]|[]β€…[], then []≑[];
  • if [] ⊣ u|v β€… s ⊣ l|l' ↦ s' and s' is accepting, then the letters l,l' can be:
    • ⟨a,⟨b, but because s' is accepting we deduce that a=b and s' is accepting;
    • var x,var y, with s=s', and because s' is accepting we deduce that var x=var y;
    • a⟩,b⟩.
    In the first two case, we have l=l' and by induction u≑v, thus we deduce u++l≑v++l'.
The last case is more subtle: we need to show that if aβ‰ b and if there is path for the empty stack to s labelled with u++[a⟩] | v++[b⟩], then we can decompose u and v as follows:
  • u=u1++⟨a::u2 and v=v1++⟨b::v2, where u1 and v1 have the same length;
  • a β‹„ u2 and b β‹„ v2.
However, the statements a β‹„ u2 and b β‹„ v2 are not stable by prefixes, meaning that this statement is too weak to be provable by a direct induction. Therefore we start by proving the following technical lemma.
Lemma path_stack_decompose_aux u v a b t1 t2 :
  ([] ⊣ u | v β€… t1++(a,b)::t2) β†’
  βˆƒ u1 u2 v1 v2, u=u1++⟨a::u2
                 βˆ§ v=v1++⟨b::v2
                 βˆ§ ⎒u1βŽ₯ = ⎒v1βŽ₯
                 βˆ§ nb a (prj1 t1) = c_binding (𝗙 a u2)
                 βˆ§ nb b (prj2 t1) = c_binding (𝗙 b v2)
                 βˆ§ nb a (prj1 t2) = c_binding (𝗙 a u1)
                 βˆ§ nb b (prj2 t2) = c_binding (𝗙 b v1).

Corollary path_stack_decompose u v a b s :
  ([] ⊣ u | v β€… s) β†’
  aβ‰ b β†’
  (s ⊨ a ↦ b) β†’
  βˆƒ u1 u2 v1 v2, u=u1++⟨a::u2
                 βˆ§ v=v1++⟨b::v2
                 βˆ§ ⎒u1βŽ₯ = ⎒v1βŽ₯
                 βˆ§ a β‹„ u2
                 βˆ§ b β‹„ v2.

We may now prove the second direction of our main theorem: whenever we have an accepting path labelled with u|v, u and v are alpha-equivalent.
Note that this proof relies on the fact that Atom is infinite. This is in fact the only place in the proof where we use this fact. Indeed, to prove that ⟨a;⟨b;a⟩;b⟩ is equivalent to ⟨b;⟨a;b⟩;a⟩, the transducer only uses names a and b, but the derivation of ≑ will need to use a Ξ±-fresh name.
Theorem path_Ξ±equiv u v s : s βœ“ β†’ [] ⊣ u | v β€… s β†’ u ≑ v.

Theorem completeness u v : u ≑ v ↔ (βˆƒ s, [] ⊣ u | v β€… s ∧ s βœ“).

Using the equivalence between paths and alpha-equivalence, and lemma Ξ±fresh_perm_path_nil, we can prove that the following rule is admissible.
Proposition Ξ±equiv_Ξ±fresh_transpose p u : (βˆ€ a, Β¬ a #Ξ± u β†’ pβˆ™a = a) β†’ u ≑ pβˆ™u.

End s.