RIS.traces: extracting stacks directly from words.

Set Implicit Arguments.

Require Export transducer.

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

Simple trace

We introduce here the notion of trace of a word. Intuitively, the trace of a word u is a list of names, corresponding to the unmatched ⟨a appearing in u. They appear in reverse order, for instance the trace of [⟨a;⟨b] will be [b;a].

The trace of a word u after a trace l is computed by the following reverse inductive definition:

Tr l [] = l;
Tr l (u++[⟨a])=a::Tr l u;
Tr l (u++[var x])=Tr l u;
Tr l (u++[a⟩])=(Tr l u) ⊖ a.

Definition updTr acc l :=
  match l with
  | var _ ⇒ acc
  | ⟨a ⇒ a::acc
  | a⟩ ⇒ acc ⊖ a
  end.
Definition Tr l u := fold_left updTr u l.

The following identities hold.

Lemma Tr_app l u v : Tr l (u ++v) = Tr (Tr l u) v.
Lemma Tr_add l u a : Tr l (u ++[a ]) = updTr (Tr l u) a.

This technical lemma will be used for the next proposition.

Lemma updTr_length l u x :
⎢updTr (Tr l u) x ⎥
≤ ⎢Tr l u ⎥ + sum (fun b ⇒ c_binding (𝗳 b x) - d_binding (𝗳 b x)) ⌊x ⌋.

The number of occurrences of a in Tr l u can be obtained from the number of as in l by first subtracting d_binding (𝗙 a u), and then adding c_binding (𝗙 a u).

Proposition Tr_length_binding_atom a l u :
nb a (Tr l u) = (nb a l - d_binding (𝗙 a u)) + c_binding (𝗙 a u).

The atoms in the trace Tr l u all appear either in the support of u or in l.

Lemma Tr_support l u : Tr l u ⊆ ⌊u ⌋++l.

If a does not appear in Tr l u (for any l), then a is close-balanced in u.

Lemma Tr_close_balanced a u l : ¬ a ∈ Tr l u → a ▷ u.

If a is close-balanced in u, then it cannot appear in Tr [] u. Note however that it could appear in Tr l u for some l: take for instance l=[a] and u=[].

Lemma In_Tr_not_open_balanced a u : a ▷ u → ¬ a ∈ Tr [] u.

Tr commutes with the action of permutations.

Lemma Tr_perm p u l : p ∙(Tr l u ) = Tr (p ∙l) (p ∙u).

Indexed traces

For Theorem path_αequiv, we will need a stronger notion of traces. Simple traces, as defined in the previous section, list the occurrences of unmatched ⟨a. In the definition to come we strengthen this by adding a natural number corresponding to the index of the letter in u where the unmatched ⟨a was found.

Technical definition

We start by defining a variant of rmfst, intended to work on lists of pairs built out of a number an an atom. Its effect will be made clear by the following lemmas.

Fixpoint rmfstn (a : atom) (l : list (nat ×atom)) :=
  match l with
  | [] ⇒ []
  | (n,b)::l ⇒ if a =?=b then l else (n,b)::(rmfstn a l )
  end.

Given a name a and a list l, if there is no pair of the shape (n,a) in l then rmfstn a l = l.

Lemma rmfstn_notin a l : ¬ a ∈ prj2 l → rmfstn a l = l.

If on the other hand there are such pairs in l, then rmfstn a l will remove from l the first of them.

Lemma rmfstn_in a n l1 l2 :
¬ a ∈ prj2 l1 → rmfstn a (l1 ++ (n ,a ) :: l2) = l1 ++l2.

rmfst and rmfstn are related by the following identity.

Lemma rmfstn_rmfst a l : (prj2 l ) ⊖ a = prj2 (rmfstn a l).

rmfstn a l is contained in the list l.

Lemma rmfstn_decr a l : rmfstn a l ⊆ l.

Main definitions

We define Trn as follows. Its meaning will become clearer with the following lemmas.

Definition updTrn (accn : nat × list (nat × atom)) l :=
  let n := fst accn in
  let acc := snd accn in
  match l with
  | var _ ⇒ (S n ,acc )
  | ⟨a ⇒ (S n ,(n ,a)::acc )
  | a⟩ ⇒ (S n ,rmfstn a acc )
  end.
Definition Trn_aux l u := fold_left updTrn u l.
Definition Trn u := snd (Trn_aux (0,[]) u).

Properties of indexed traces

The second projection of Trn u is Tr [] u.

Remark updTrn_updTr acc l :
prj2 (snd (updTrn acc l)) = updTr (prj2 (snd acc)) l.

Corollary Trn_Tr u : prj2 (Trn u) = Tr [] u.

Any number appearing in the first projection of Trn u is strictly smaller than the length of u.

Lemma Trn_In_length u : ∀ n, n ∈ prj1 (Trn u) → n < ⎢u ⎥.

If the pair (n,a) appears in Trn u, then the letter at index n in u is ⟨a.

Lemma Trn_open a x u v : (⎢u ⎥,a ) ∈ Trn (u ++x ::v) → x = ⟨a.

If the number n1 appears before n2 in Trn u, then n2<n1.

Lemma Trn_incr u n1 a1 n2 a2 u1 u2 u3 :
Trn u = u1 ++(n1 ,a1 )::u2 ++(n2 ,a2 )::u3 → n2 < n1.

To state results about the binding power, we define the boolean predicate select n a. It holds for pairs (m,b) where n≤m and a=b.

Definition select n (a : atom) p := Nat.leb n (fst p) && a =?= (snd p ).
Lemma select_spec n a m b : select n a (m ,b ) = true ↔ n ≤ m ∧ a = b.

The number of pairs (n,a), such that n is smaller than or equal to the length of u, appearing in Trn (u++v) is equal to c_binding (𝗙 a v).

Lemma Trn_c_binding a u v :
⎢ select ⎢u ⎥ a :> Trn (u ++v)⎥ = c_binding (𝗙 a v).

If the pair (⎢u⎥,a) appears in Trn (u++⟨a::v), then a is close-balanced in v.

Lemma Trn_d_binding a u v : (⎢u ⎥,a ) ∈ Trn (u ++⟨a ::v) → a ◁ v.

Correspondence with stacks

If there is a path labelled with u|v from s1 to s2, then the first component of s2 is the trace of u after the first component of s1.

Lemma Tr_step a b s1 s2 : s1 ⊣ a | b ↦ s2 → prj1 s2 = updTr (prj1 s1) a.
Corollary Tr_path u v s1 s2 : s1 ⊣ u | v ⤅ s2 → prj1 s2 = Tr (prj1 s1) u.
Corollary Trn_path_snd u v s2 :
[] ⊣ u | v ⤅ s2 → prj1 s2 = prj2 (Trn u).

One can also understand that property as stating that if there is a path labelled with u|v from the empty stack to s, then s must be the combination of the trace of u with the trace of v.

Corollary path_Tr s u v : [] ⊣ u | v ⤅ s → s = (Tr [] u ) ⊗ (Tr [] v ).
Remark Accepting_path_Tr s u v : [] ⊣ u | v ⤅ s → s ✓ ↔ Tr [] u = Tr [] v.

If there is a path labelled with u|v from the empty stack to s, then the first projections of the indexed traces of u and v coincide.

Proposition Trn_path_fst u v s :
[] ⊣ u | v ⤅ s → prj1 (Trn u) = prj1 (Trn v).

End s.