# 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.
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.
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.
The length of a term is also its greatest vertex.
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).
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.
Hence we get that the path relation is a partial order, thus proving that the graph of a term is always acyclic.
Is it not hard to show that it is also connected, thus making it a good graph.
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.
The extremities of every edge in ๐ฒ u are vertices.
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.
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.
The next few lemma extract from a path in either ๐ฒ (u1 โจพ u2) or ๐ฒ (u1 โฅ u2) paths in either ๐ฒ u1 or ๐ฒ u2.

# 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.
The graph of a term e is greater than the point graph (0,[],0) if and only if all of its variables are tests.
The parametric ordering of series-parallel terms is contained in the graph ordering with the same parameter.

# 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.

## 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.
split_point u k is the length of pref u k.
The graphs of moustache u k and of pref u k โจพ suf u k are equal.
moustache u k is provably smaller than pref u k โจพ suf u k.
u is provably smaller than its moustache.
split_point u k is a vertex of 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.
ฮผ 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.
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).