Library LangAlg.sp_terms_graphs

This module is devoted to the translation from series-parallel terms to graphs.

Set Implicit Arguments.

Require Export graph sp_terms.

Section s.

Definitions and basic facts

We fix a decidable alphabet X.
  Variable X : Set.
  Variable ฮ› : decidable_set X.

  Notation grph := (graph nat X).
  Notation edg := (@edge nat X).

The length of a term is defined inductively as follows.
  Fixpoint ln (u : ๐’๐ X) :=
    match u with
    | ๐’๐_var _ โ‡’ S O
    | u โจพ v | u โˆฅ v โ‡’ ln u + ln v
    end.

In fact, it coincides with the length of the list of variables.
  Lemma size_ln u : ln u = length โŒˆuโŒ‰.

As such, it is smaller that the size of the term.
  Lemma ln_smaller_size u : ln u โ‰ค โฆƒuโฆ„.

A term always has strictly positive length.
  Lemma ln_non_zero u : 0 < ln u.

We associate to every term a graph as follows:
  Fixpoint ๐•ฒ (u : ๐’๐ X) : grph :=
    match u with
    | ๐’๐_var a โ‡’ (0,[(0,a,S 0)],S 0)
    | uโจพv โ‡’ ๐•ฒ u โ‹„ graph_map (โจฅ (ln u)) (๐•ฒ v)
    | uโˆฅv โ‡’
      (graph_map {|ln u\ln u+ln v|} (๐•ฒ u))
        โ‹„ graph_map ({|ln u \ 0|} โˆ˜ โจฅ (ln u)) (๐•ฒ v)
    end.

The list of labels of the graph of a term is exactly its list of variables.
  Lemma graph_variables u : โŒˆ u โŒ‰ = โŒˆ๐•ฒ uโŒ‰.

The input of the graph of a term is always 0, and its output is equal to the length of the term.
  Lemma graph_input u : input (๐•ฒ u) = 0.

  Lemma graph_output u : output (๐•ฒ u) = ln u .

If the edge (i,ฮฑ,j) appears in the graph of u, then we can infer the following inequalities.
  Lemma ๐•ฒ_bounded u i ฮฑ j : (i,ฮฑ,j) โˆˆ (edges (๐•ฒ u)) โ†’ i < j โ‰ค ln u.

The length of a term is also its greatest vertex.
  Lemma vertices_bounded u i : i โˆˆ โŒŠ๐•ฒ uโŒ‹ โ†’ i โ‰ค ln u.

We give an inductive definition of the set of vertices of the graph of a term, which will we show to be equivalent to the real thing.
  Fixpoint vertices u :=
    match u with
    | ๐’๐_var _ โ‡’ (S O)::O::[]
    | uโจพv โ‡’ vertices u++(List.map (โจฅ (ln u)) (vertices v))
    | uโˆฅv โ‡’ rm (ln u) (vertices u++(List.map (โจฅ (ln u)) (vertices v)))
    end.

The graph of uโจพv is the sequential product of the graphs of u and v (modulo a translation of the graph of v to avoid vertex capture).
  Lemma good_for_seq_๐•ฒ u v:
    good_for_seq (๐•ฒ u) (graph_map (โจฅ (ln u)) (๐•ฒ v)).

The graph of uโˆฅv is the parallel product of the graphs of u and v (modulo two translations to avoid vertex capture).
  Lemma good_for_par_๐•ฒ u v:
    good_for_par (graph_map {|ln u\ln u+ln v|} (๐•ฒ u))
                 (graph_map ({|ln u\0|}โˆ˜โจฅ(ln u)) (๐•ฒ v)).

The path relation in term-graphs is contained in the smaller-or-equal relation of natural numbers.
  Lemma path_๐•ฒ u i j : i -[๐•ฒ u]โ†’ j โ†’ i โ‰ค j.

Hence we get that the path relation is a partial order, thus proving that the graph of a term is always acyclic.
  Lemma ๐•ฒ_acyclic u : acyclic (๐•ฒ u).

Is it not hard to show that it is also connected, thus making it a good graph.
  Lemma ๐•ฒ_good u : good (๐•ฒ u).

  Lemma ๐•ฒ_connected u : connected (๐•ฒ u).

The length of a term and 0 are vertices.
  Lemma vertex_ln u : ln u โˆˆ vertices u.

  Lemma vertex_0 u : 0 โˆˆ (vertices u).

As promised, the set of vertices of the graph of u is vertices u.
  Lemma vertices_graph_vertices u :
    vertices u โ‰ˆ โŒŠ๐•ฒ uโŒ‹.

The extremities of every edge in ๐•ฒ u are vertices.
  Lemma In_vertices u i ฮฑ j :
    (i,ฮฑ,j) โˆˆ (edges (๐•ฒ u)) โ†’ i โˆˆ (vertices u) โˆง j โˆˆ (vertices u).

If there is a path from i to j in ๐•ฒ u, then either both of them are vertices of u or none of them are.
  Lemma path_vertices u i j :
    i-[๐•ฒ u]โ†’ j โ†’ i โˆˆ (vertices u) โ†” j โˆˆ (vertices u).

If ฯ† is a morphism from the graph of u to that of v, and if i is a vertex of u, then its image is a vertex of v.
  Lemma is_morphism_vertices ฯ† u v:
    [] โŠจ ๐•ฒ u -{ฯ†}โ†’ ๐•ฒ v โ†’ โˆ€ i, i โˆˆ (vertices u) โ†’ (ฯ† i) โˆˆ (vertices v).

The next few lemma extract from a path in either ๐•ฒ (u1 โจพ u2) or ๐•ฒ (u1 โˆฅ u2) paths in either ๐•ฒ u1 or ๐•ฒ u2.
  Lemma path_seq_left u1 u2 i k :
    k โˆˆ (vertices u1) โ†’ i -[๐•ฒ (u1 โจพ u2)]โ†’ k โ†’ i -[๐•ฒ u1]โ†’ k.

  Lemma path_seq_right u1 u2 i k :
    ln u1 โ‰ค i โ†’ i -[๐•ฒ (u1 โจพ u2)]โ†’ k โ†’ i - ln u1 -[๐•ฒ u2]โ†’ k - ln u1.

  Lemma path_par u1 u2 i k :
    i -[๐•ฒ (u1 โˆฅ u2)]โ†’ k โ†’
    {|ln u1 + ln u2\ln u1|} i -[ ๐•ฒ u1]โ†’ {|ln u1 + ln u2\ln u1|} k
    โˆจ (โจช (ln u1)โˆ˜{|0\ln u1|}) i -[๐•ฒ u2 ]โ†’ (โจช (ln u1)โˆ˜{|0\ln u1|}) k.

  Lemma path_par_cross u1 u2 i k :
    i < ln u1 < k โ†’ i -[๐•ฒ (u1โˆฅu2)]โ†’ k โ†’ i = 0 โˆจ k = ln (u1โˆฅu2).

  Lemma path_par_left u1 u2 i k :
    k < ln u1 โ†’ i -[๐•ฒ (u1โˆฅu2)]โ†’ k โ†’ i -[๐•ฒ u1]โ†’ k.

  Lemma path_par_right u1 u2 i k :
    ln u1 < i โ†’ i -[๐•ฒ (u1โˆฅu2)]โ†’ k โ†’ i - ln u1 -[๐•ฒ u2]โ†’ k - ln u1.

From axiomatic containment to graph ordering

If u and v are related by the equality axioms of series-parallel terms, then their graphs are equivalent.
  Lemma is_morph_๐’๐_ax u v : ๐’๐_ax u v โ†’ ๐•ฒ u โ‹ˆ ๐•ฒ v.

The graph of a term e is greater than the point graph (0,[],0) if and only if all of its variables are tests.
  Lemma supid_hom_order A e : โŒˆeโŒ‰ โŠ† A โ†” A โŠจ (0, [], 0) โŠฒ ๐•ฒ e.

The parametric ordering of series-parallel terms is contained in the graph ordering with the same parameter.
  Lemma is_morph_๐’๐_inf A u v : A โŠจ u << v โ†’ A โŠจ ๐•ฒ u โŠฒ ๐•ฒ v.

From graph ordering to axiomatic containment

Variables

If the graph of u is smaller than the graph of a variable, then u is provably smaller than this variable.
  Lemma morph_var A u a ฯ† :
    A โŠจ (๐•ฒ (๐’๐_var a))-{ฯ†}โ†’ (๐•ฒ u) โ†’ [] โŠจ u << ๐’๐_var a.

Sequential product

  Section seq.
We fix a term u, and an integer k, such that k is an interior vertex of ๐•ฒ u (that is a vertex different from both 0 and ln u.
    Context { u : ๐’๐ X } { k : nat }.
    Context {Rk: 0 < k < ln u } {Vk: k โˆˆ (vertices u)}.

We'll split u according to k:
  • pref u k is a term whose graph is the part of the ๐•ฒ u that can reach k;
  • suf u k is a term whose graph is the part of the ๐•ฒ u that is reachable from k;
  • moustache u k is a term whose graph is the part of ๐•ฒ u that is visible from k.
    Fixpoint pref u k :=
      match u with
      | u โจพ v โ‡’
        if eqX k (ln u)
        then u
        else
          if Nat.ltb k (ln u)
          then pref u k
          else u โจพ (pref v (k - ln u))
      | u โˆฅ v โ‡’
        if Nat.ltb k (ln u)
        then pref u k
        else (pref v (k - ln u))
      | _ โ‡’ u
      end.

    Fixpoint suf u k :=
      match u with
      | u โจพ v โ‡’
        if eqX k (ln u)
        then v
        else
          if Nat.ltb k (ln u)
          then (suf u k) โจพ v
          else suf v (k - ln u)
      | u โˆฅ v โ‡’
        if Nat.ltb k (ln u)
        then suf u k
        else (suf v (k - ln u))
      | _ โ‡’ u
      end.
    Fixpoint moustache u k :=
      match u with
      | u โจพ v โ‡’
        if eqX k (ln u)
        then u โจพ v
        else
          if Nat.ltb k (ln u)
          then moustache u k โจพ v
          else u โจพ (moustache v (k - ln u))
      | u โˆฅ v โ‡’
        if Nat.ltb k (ln u)
        then moustache u k
        else moustache v (k - ln u)
      | _ โ‡’ u
      end.

split_point u k is the vertex in the graph of moustache u k that corresponds to k.
    Fixpoint split_point u k :=
      match u with
      | u โจพ v โ‡’
        if eqX k (ln u)
        then k
        else
          if Nat.ltb k (ln u)
          then split_point u k
          else ln u + split_point v (k - ln u)
      | u โˆฅ v โ‡’
        if Nat.ltb k (ln u)
        then split_point u k
        else split_point v (k - ln u)
      | _ โ‡’ k
      end.

We can relate u with pref u k โจพ suf u k using axiomatic containment.
    Lemma ๐’๐_inf_pref_suf : [] โŠจ u << pref u k โจพ suf u k.

split_point u k is the length of pref u k.
    Lemma ln_pref_split_point : ln (pref u k) = split_point u k.

The graphs of moustache u k and of pref u k โจพ suf u k are equal.
    Lemma split_moustache : ๐•ฒ (moustache u k) = ๐•ฒ (pref u k โจพ suf u k).

moustache u k is provably smaller than pref u k โจพ suf u k.
    Lemma split_moustache_inf: [] โŠจ moustache u k << pref u k โจพ suf u k.

u is provably smaller than its moustache.
    Lemma ๐’๐_inf_moustache : [] โŠจ u << moustache u k.

split_point u k is a vertex of moustache u k.
    Lemma split_point_in_moustache :
      split_point u k โˆˆ vertices (moustache u k).

If ฯ† is a morphism from u1โจพu2 to v1โจพv2, and if the image of the output of u1 is the output of v1, then the graph of u1 is greater than that of v1 and the graph of u2 is greater than the graph of v2.
    Lemma morphism_seq_split u1 u2 v1 v2 ฯ† A :
      A โŠจ ๐•ฒ (u1โจพu2) -{ฯ†}โ†’ ๐•ฒ (v1โจพv2) โ†’ ฯ† (ln u1) = ln v1 โ†’
      A โŠจ ๐•ฒ v1 โŠฒ ๐•ฒ u1 โˆง A โŠจ ๐•ฒ v2 โŠฒ ๐•ฒ u2.

ฮผ u k is a function mapping the vertices of u that are visible from k to vertices in moustache u k.
    Fixpoint ฮผ u k i :=
      match u with
      | ๐’๐_var _ โ‡’ 0
      | u โจพ v โ‡’
        if eqX k (ln u)
        then i
        else
          if Nat.ltb k (ln u)
          then
            if Nat.leb i (ln u)
            then ฮผ u k i
            else ln (moustache u k) + i - ln u
          else
            if Nat.leb i (ln u)
            then i
            else ln u + ฮผ v (k - ln u)
                          (i - ln u)
      | u โˆฅ v โ‡’
        if Nat.ltb k (ln u)
        then (ฮผ u k ({|ln (uโˆฅv)\ln u|} i))
        else (ฮผ v (k - ln u) (i - ln u))
      end.

The image of 0 by ยต is 0.
    Lemma ฮผ_0 : ฮผ u k 0 = 0.

The image of the length of u by ยต is the length of its moustache.
    Lemma ฮผ_ln : ฮผ u k (ln u) = ln (moustache u k).

This lemma could be restated as the statement that in the graph of moustache u k, every vertex is either reachable or co-reachable from split_point u k.
    Lemma visible_moustache :
      vertices (moustache u k) โ‰ˆ visible (๐•ฒ (moustache u k))
               (split_point u k).


The image of k by ฮผ u k is split_point u k.
    Lemma ฮผ_k : ฮผ u k k = split_point u k.

  End seq.

If a vertex in u is either reachable or co-reachable from k, then ฮผ sends it to a vertex of the moustache.
  Lemma ฮผ_internal u k :
    0 < k < ln u โ†’ k โˆˆ (vertices u) โ†’
    internal_map (ฮผ u k)
                 (filter_graph (fun i โ‡’ k -[ ๐•ฒ u ]?โ†’ i)
                               (fun j โ‡’ j -[ ๐•ฒ u ]?โ†’ k)
                               (๐•ฒ u))
                 (๐•ฒ (moustache u k)).

ฮผ u k is a morphism from the k-visible part of the graph of u to the moustache graph.
  Lemma ฮผ_morph u k :
    0 < k < ln u โ†’ k โˆˆ (vertices u) โ†’
    ([] โŠจ (filter_graph (fun i : nat โ‡’ k -[ ๐•ฒ u ]?โ†’ i)
                        (fun j : nat โ‡’ j -[ ๐•ฒ u ]?โ†’ k)
                        (๐•ฒ u))
     -{ฮผ u k}โ†’ ๐•ฒ (moustache u k)).

We are now equipped to prove the lemma necessary for the induction step corresponding to the sequential product: assuming there is a morphism from v1โจพv2 to u, then one of three things happen:
  • every variable in v1 is a test, and there is a morphism from v2 to u;
  • every variable in v2 is a test, and there is a morphism from v1 to u;
  • there is an internal vertex of u, say k, such that the graph of pref u k (resp. suf u k) is smaller that that of v1 (resp. v2).
  Lemma morphism_seq_step (u v1 v2 : ๐’๐ X) A :
    A โŠจ ๐•ฒ u โŠฒ ๐•ฒ (v1 โจพ v2) โ†’
    (โŒˆv1โŒ‰โŠ† A โˆง A โŠจ ๐•ฒ u โŠฒ ๐•ฒ v2)
    โˆจ (โŒˆv2โŒ‰โŠ† A โˆง A โŠจ ๐•ฒ u โŠฒ ๐•ฒ v1)
    โˆจ (โˆƒ k, 0 < k < ln u โˆง k โˆˆ (vertices u)
            โˆง A โŠจ ๐•ฒ (pref u k) โŠฒ ๐•ฒ v1
            โˆง A โŠจ ๐•ฒ (suf u k) โŠฒ ๐•ฒ v2).

Completeness lemma

  Lemma ๐’๐_inf_is_morph A u v :
    A โŠจ ๐•ฒ u โŠฒ ๐•ฒ v โ†’ A โŠจ u << v.

Main result

  Theorem ๐’๐_inf_is_morph_iff A u v :
    A โŠจ ๐•ฒ u โŠฒ ๐•ฒ v โ†” A โŠจ u << v.

End s.