In most this module, we establish the following lemma: for every series-parallel term u, there exists a word w and an interpretation σ such that for every other 𝐒𝐏 term v, the graph of v is larger than the graph of u if and only if w belongs to the σ-interpretation of v. This lemma will allow us to prove completeness of our axiomatization with respect to language interpretations. In the second part of the module, we generalise the result to weak terms and primed weak terms. In this module, we call a list of natural numbers a sequence is it of the form [a(0);a(1);...;a(n)] such that for every i<n, a(i)+1=a(i+1). Equivalently, they are those sequences produced using the function seq.

Main construction

Let us fix a term u and a set of variables 𝐀 for this section.

We write the reachability relation in the graph of u as ⤏.

To make some definitions easier, we define the function co_nth i l. This function returns the smallest index j such that the jth element of the list l is equal to i.

If i appears in the list l, then the element at index co_nth i l in the list l is equal to i.

If i is in l, this function returns an index smaller than the length of l.

The following simple observation follows easily from co_nth_In.

We will mainly apply this function on lists without duplicates. In such lists, the function is injective.

In lists with no duplicates, we can prove the dual of lemma co_nth_In.

Vert is a list containing exactly the vertices of the graph of u, without any duplication, and listed in increasing order.

N is the number of vertices in the graph of u.

The word w_u will be the witness we announced earlier. It is defined as the sequence of natural numbers from 0 to 2 × N - 1.

The function γ finds the index of a vertex in the list Vert. It provides us with a bijection between the vertices of u and the numbers from 0 to N-1.

γ is order preserving.

Moreover, we know that the ordering of natural numbers contains the path ordering of vertices. Therefore using the previous lemma we get the following monotonicity property.

The following two observations are fairly self evident.

The next few lemmas are simple observations on sequences and on the function co_nth.

These observations allow us to prove that the image of the output of the graph of u by γ is N-1.

ω i j is the sequence of numbers from 2*γ i to 2*γ j - 1.

In particular we can use ω to define w_u.

This lemma is almost tautological, but it turns out to come in handy several times.

We now define the witnessing interpretation. For every edge (i,a,j) in the graph of u, the word ω i j is in σ a. Furthermore, if a belongs to the set 𝐀, then the empty word is in σ a.

The only way for the empty word to appear in σ a is when a belongs to the set 𝐀.

A simple observation we can make is that for any letter a the length of any word in σ a is even. This can be neatly extended to the language of any series-parallel term according to σ.

This result mainly relies on the fact that the seq function is essentially bijective.

If a word in the σ-interpretation of some term v is a sequence, then it can be expressed as ω i j, for some vertices i,j such that i⤏j.

For every pair of vertices i≤j, if ω i j belongs to the σ-interpretation of a sequential product v1⨾v2, then there exists a vertex k between i and j, such that ω i k belongs to the language of v1 and ω k j to that of v2. This lemma is critical in the proof of the main lemma to make the induction case for products go through.

By a simple induction on v, one can check that the empty word belongs to the language of v exactly if all of the variables in v belong to the set 𝐀.

To prove that from the fact that w_u is in the language ⟦v⟧ σ we can build a morphism from v to u, we need to strengthen the statement slightly to make the induction work better. The statement that turns out to be sufficient is the following: if ω i j belongs to ⟦v⟧ σ, then there is an internal premorphism from v to u that must in addition map 0 to i and ln v to j.

For the converse direction, we use the following lemma, also proved by induction on the term v.

With the two technical lemmas we just proved, the proof of the main result of this module becomes very simple.

Weak terms

Nothing deep happens here, we just apply the results and constructions above to get a similar theorem.

Primed weak terms

For primed weak terms, another problem arises. Because of the way we have set up the translation form terms and expressions into weak terms, it is not sufficient to have a lemma of the shape ∃ w (σ: 𝕬[X'→nat]), ∀ v : 𝐖', 𝕲w (π{u}) ≲ 𝕲w (π{v}) ↔ w ⋵ ⟦π{v}⟧σ. We need our witnessing interpretation σ to arise as Ξ σ' for some σ' : 𝕬[X→nat]. Thus we massage the construction we proved correct earlier, to put it into the appropriate shape.

This is the witnessing interpretation. It works mostly like the one we built for series-parallel terms, but we make use of the boolean in the letters from the duplicated alphabet: if (i,a,j) is an edge, then ω i j is in the language σΞ (a,true), and its mirror image is in the language of σΞ (a,false).

First, we make some observations about σΞ.

When looking for sequences, we can relate Ξ σΞ and σ'.

Hence we can transfer the presence of a witness in ⟦v⟧(Ξ (σΞ u)) to the presence of the witness in the interpretation we set up for weak terms.

We now prove our witnessing lemma by putting together lemmas witness_Ξ and word_of_term_correct.