Local and asynchronous beta-reduction

(an analysis of Girard’s EX formula)

2 December 1992

Vincent Danos

Équipe de Logique, URA 753 du CNRS

Université de Paris 7

e-mail: danos at logique.jussieu.fr

& Laurent Regnier

Laboratoire de mathématiques discrètes, UPR 9016 du CNRS Université d’Aix-Marseille e-mail: regnier at logique.jussieu.fr

Abstract

We build a confluent, local, asynchronous reduction on λ-terms, using infinite objects (partial injections of Girard’s algebra L*), which is simple (only one move), intelligible (semantic setting of the reduction), general (based on a largescale decomposition of β), and may be mechanized.

Équipe de Logique Mathématique UFR de mathématiques Couloir 45-55, 5ème étage

Université de Paris 7

2 place Jussieu 75251 Paris Cedex 05

FRANCE Phone: (33-1) 43 29 77 26

Introduction

Captatio Benevolentiae. λ-calculus certainly is the simplest syntax ever developed for proof denotation & normalization in intuitionistic logic. Discovered by Church, rediscovered by Gentzen (under the guise of natural deduction), turned into a functional language by Mc-Carthy (LISP), and nowadays clearly seen to be extendable to classical logic as well, λcalculus is a fair syntax.

Longing for a mathematical account of β-reduction. Albeit the computation rule of λcalculus, β-reduction, is simple, understood as an operation on symbols, it is too ingenuous to be satisfying. Especially, when one considers how ingeniously λ-calculus has been implemented.

Geometry of interaction. Endeavours to provide mathematical accounts of β-reduction, were initiated and rallied by Girard under the banner “geometry of interaction”; where “interaction” means dealing with logical computation processes, and “geometry of” means by geometric means (here the means will rather be of algebraic nature).

There also is the connotation that such processes should be examined under the Linear Logic looking-glass (because LL already provides a decomposition of intuitionistic and classical logic), and inspected at a larger scale than usual, hoping for a simplification. Diving deep enough in the structure of β should try and unmask the global and sequential process of β-reduction as only a lot of local and parallel microscopic moves.

Background & idea of the paper. The paper is readable with no specialized knowledge of the subject. But let us say how it relates to previous work. We reinterpreted in preceding studies ([3],[8]) Girard’s seminal execution formula EX, as the computation of “regular” paths in the graph representation (inherited from proof-nets of Linear Logic) of λ-terms. EX is a “scalar”, attached to any such graph, and belonging to the dynamic algebra L* (EX and L* both are defined in [5]), on which one can read back the result of the ordinary β-computation (whenever there is one) in case of data-types (typically Church numerals).

The mere fact that objects with such a geometrical “touch” (I mean those regular paths) lurk somewhere under the skirts of the old lady (β-reduction) is encouraging.

Now the idea of the paper is to devise a local reduction implementing this path-computation: could it be that one could locally reduce the graph representations of λ-terms in such a way that EX is preserved ? Curiously, the question has an easy and positive answer.

The simplification. The easiness of this construction relies on a simplification of the problem: we choose to describe this virtual reduction by putting to use infinite objects (namely partial one-to-one transformations of ). This means technically that we use the “semantic form” of L* (instead of the syntactic form as a rewriting system (see [8])) to label the edges of our graph representation of terms.

The benefit is twofold: first, it makes the reduction rule natural and intelligible; second, it makes the proofs easier. This simplification is innocuous, since one can go back to finite objects (though some additional work is involved) and build a “mechanical” reduction. This shall be done in the second part of this paper (see [4]), where we shall also build optimal reductions (as in [1]), using an amazingly simple constraint bearing on the reductions here defined.

Contents of the paper. λ-calculus is embedded into graphs labeled by partial one-to-one transformations (sections 8, 9); then over such graphs, considered abstractly (sections 1, 2), and named “virtual nets”, a LOCAL and ASYNCHRONOUS reduction consisting in the iteration of one single move, “the composition of two edges”, is defined (section 3); the virtual nets yielded by such reductions are (in general) no more images of λ-terms; so to speak, virtual reduction steps out of λ-calculus (which is not that surprising) never to go back again (which may be more surprising).

This reduction preserves the key-property of “well-splitting” (section 4): any images of three partial transformations labeling coincident edges have a void intersection; which says intuitively that there is no “colliding” in the computation of EX over the virtual net. Girard’s formula EX then is shown to be an invariant of this reduction (section 5), which means that this reduction indeed is a computation of the term; also the reduction is proved to be confluent (section 7) using the square freedom property introduced in section 6.^{1}

“Local & asynchronous” means what. Local means control over the size of objects duplicated, & synchronous means that explicit scheduling is involved in computations; so β is asynchronous but global, while environment machines are local but synchronous.

By the way, this study can also be seen as a kind of most general setting (no mathematical commitment here, of course) wherein to examine existing λ-machines and design new ones.

Comparison to Abadi et al.’s paper. In [1], the authors elucidate the shared λ-calculus of Lamping with the help of Girard’s interpretation of λ-calculus in L*. They prove consistency of this other graph reduction by the same property: EX is an invariant. So at first sight our two constructions bear strong resemblance. With a good deal of circumspection (the real relation is still a matter of puzzlement to us), we could say that:

— our proposition seems to encompass more general reductions, for the “triangle”, the key sharing operator of Lamping, can’t be split in two halves, whereas in the corresponding notion here (exponential coefficients belonging to the same variable) there is no such restriction;

— our unique reduction rule is easily understood on a semantic basis, and seen to be consistent and complete, and thus allows a swift and easy ride to the crucial property (EX’s invariance) thanks to the setting of the question on semantical ground (discussed before); while their rules seem to convey less obvious intuitions about why they are so, or why they are complete.

It certainly would be interesting to say more about the relation between these two reductions. Anyway, this paper is not an elucidation of Abadi et al’s elucidation of Lamping’s reduction, but a proposition by its own, though using the same basic ingredient, i.e., Girard’s EX.

About the mechanization. The furthering of this analysis to the concrete presentation of L* (see [8]), denoted by mL*, which like L* is an inverse semigroup (axiomatized by equations (1)–(4) in section 1) and a decidable one, relies on the building over mL* of a “bar” construct (axiomatized by equations (5)–(6), also in section 1). The results stated here still hold in the syntactic case, since we really only use these equations. As said, we kept here the partial one-to-one transformations for intuitive support.

1A somewhat less vital issue, for invariance of EX is sufficient for proving consistency of this method.

Thanks. We would like to thank Yves Legrandgerard who pointed out talk that our algebraic structure looked very much like the well known structure of inverse semigroups and gave us the useful reference [2]. This has been a source of inspiration for us, which stimulated the redaction of this paper.

1 Algebraic material: L*

Let L* be the inverse semigroup (see [2]) of partial one-to-one transformations of any countable set, say .

Put 0 and 1 to be respectively the nowhere defined transformation and the identity of .

Let x be in L*; we denote the inverse transformation by x^{∗}.

For any x, y in L* we have:

(x^{∗})^{∗} = x  (1)
(xy)^{∗} = y^{∗}x^{∗}  (2)

We set ⟨x⟩ = xx^{∗} (resp. ⟨x^{∗}⟩ = x^{∗}x), which is readily seen to be an idempotent (namely 1 restricted to the codomain (resp. domain) of x), the right (resp. left) unit of x. Note that any idempotent in L* may be written as ⟨x⟩ for some x.

For any x, y in L*, with these notations we have,

⟨x⟩x = x  (3)
⟨x⟩⟨y⟩ = ⟨y⟩⟨x⟩  (4)

Now define for all x in L*, \overline{x} to be 1 − ⟨x⟩ = 1 − xx^{∗}, i.e., the identity restricted to the complementary of the codomain of x. Here are some relations satisfied by this operation on L*:

\overline{1} = 0 and \overline{0} = 1  (5)
x\overline{y} = \overline{xy}x  (6)

By the way, (1)–(4) is a set of axioms for inverse semigroups (see [7]) and (1)–(6) is a set of axioms for the “bar-inverse semigroups”, which is the notion (introduced by the authors) needed for the mechanization.

Proposition 1 The axioms (1)–(6) have the following consequences:

\overline{x} \overline{x} = \overline{x},  \overline{x} \overline{y} = \overline{y} \overline{x}  (7)
\overline{x}⟨y⟩ = ⟨y⟩\overline{x}  (8)
\overline{xy} \overline{x\overline{y}} = \overline{x}  (9)
\overline{x}x = 0  (10)
\overline{\overline{x}}x = x  (11)
\overline{xx^{∗}} = \overline{x}  (12)

and:

⟨x⟩⟨y⟩ = 0 iff x^{∗}y = 0 iff \overline{y}x = x iff \overline{x}y = y  (13)

The proof is a straightforward computation using the well known fact that idempotents of an inverse semigroup commute. The relations (1)–(13) are the very properties of L* that we shall use in the sequel, so that we could everywhere replace L* with any “bar-inverse semigroup”.

A last notation: suppose x and y have disjoint domains and disjoint codomains, we write x⊕y for the “disjoint union” of x and y, which is indeed a one-to-one partial transformation.

2 Virtual structures

Let G be an unoriented graph. The ∗-semigroup C(G) of oriented paths has for product the composition along the graph (the product of two uncomposable paths is 0), and for involution, the reversal of paths (which transposes products of paths, i.e., (ϕ_{1}ϕ_{2})^{∗} = ϕ_{2}^{∗}ϕ_{1}^{∗}).

Clearly, C(G) is generated by paths of length 1, which we will call oriented edges.

Let v ←^{x} u be the matrix indexed by the vertices of G with the element x of L* at position vu, and 0 elsewhere. This notation is natural if one considers that: w ←^{y} v · v ←^{x} u = w ←^{yx} u. Let L*(G) be the set of matrices of the form v ←^{x} u, for x in L* and u, v vertices of G. It is readily seen that L*(G) is also an inverse semigroup; the three operations defined on L* are extended in the following way:

\begin{matrix}(v ←^{x} u)^{∗} = u ←^{x∗} v, ⟨v ←^{x} u⟩ = v \underleftarrow{⟨x⟩} v, \\ \overline{v ←^{x} u} = v ←^{\overline{x}} v, \end{matrix}

and the relations of the foregoing section still hold. Let finally L*_{+}(G) denote the contracted algebra over L*(G), i.e., the -module over L*(G) quotiented by the identification between the null matrix (i.e., the 0 of L*(G)) and the sum with 0 term (i.e., the 0 of the -module).

Definition 1 (Virtual Structure) A weight over a graph G is a ∗-antimorphism w from C(G) into L*(G) defined on oriented edges by: w(α) = v ←^{x} u, where α goes from u to v, and x is in L*.

Since w is required to be a antimorphism, for any paths ϕ, ϕ_{1} and ϕ_{2} we have: w(ϕ^{∗}) = w(ϕ)^{∗}, w(ϕ_{1}ϕ_{2}) = w(ϕ_{2})w(ϕ_{1}).

A virtual structure V = (G, w) consists in a finite graph G and a weight over G.

Note that composition is reversed between paths and elements of L*(G).

A path ϕ is said to be a regular path if w(ϕ) ≠ 0.

Notations: α, β, γ will stand for oriented edges; a, b, c for their weights; ϕ, ψ for paths; f and g for their weights; π will be an idempotent of L*(G); α^{(∗)} will stand for either α or α^{∗}; and the same for a^{(∗)}.

We shall also resort to the following notation for virtual structures (also useful to visualize computations): first we draw the graph G; next we choose an orientation for each edge; then for each chosen oriented edge α going from u to v, we label α with x if the weight of α is

w(α) = v ←^{x} u.

3 Virtual reduction

We first define two local transformations on a virtual structure:

— Splitting of α by π, consists in replacing α by α_{1} and α_{2} (we obtain a structure V′ with one more edge than V) with weigths:

w(α_{1}) = πa, w(α_{2}) = \overline{π}a

— Merging of β and α, only defined if β and α^{∗} are distinct oriented edges and if ⟨b⟩ = ⟨a^{∗}⟩, consists in erasing β and α and replacing them by an oriented edge γ = β :: α with same source, goal and weight as βα.

In the first case we say that we split α and in the second case we say that we merge β and α.

Definition 2 (Composition) Let V be a virtual structure, β and α two w-composable oriented edges, i.e., satisfying α ≠ β^{(∗)} and ab ≠ 0. The composition of β and α consists in:

— splitting β in β_{1} and β_{2} by the right unit ⟨a^{∗}⟩ of α;

— splitting α^{∗} in α_{1}^{∗} and α_{2}^{∗} by the left unit ⟨b⟩ of β;

— merging β_{1} and α_{1}.

The weight of β_{1} :: α_{1} is given by the following computation:

w(β_{1} :: α_{1}) = w(α_{1})w(β_{1}) = a⟨b⟩⟨a^{∗}⟩b = a⟨a^{∗}⟩⟨b⟩b
= ab = w(βα)

The whole composition process is summarized in the following picture:

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.} x  y

leads to:

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  xy x\overline{y}  \overline{x^{∗}}y

where a = w ←^{x} v and b = v ←^{y} u for some x and y in L* and some vertices u, v, w of V.

The idea is that the residual α_{2} of α is weighted by a restricted to the complementary of the left unit of b (i.e., \overline{b}), because we want to get rid of the “part” of a which has already been put to use in the composition (same explanation for β_{2}). In other words, \overline{b} operates like an internal synchronization device, modelling the partial “consumption” of α during the composition.

If this intuition is correct, then a consequence is that it should readily prohibit recomposition; and indeed:

w(α_{2})w(β_{2}) = a\overline{b} \overline{a^{∗}}b = a\overline{a^{∗}} \overline{b}b = 0.

By the way, we supposed ab ≠ 0 in the definition, because ab = 0 entails ⟨a^{∗}⟩⟨b⟩ = 0, so \overline{a^{∗}}b = b and a\overline{b} = a (this composition would just add a 0-weighted edge).

Definition 3 (Virtual reduction) A virtual reduction of a structure V is a sequence of compositions.

4 Splitness

Definition 4 (Splitness) Let α, β and γ be three distinct oriented edges in a virtual structure V. We say that α, β and γ are well split if:

⟨a⟩⟨b⟩⟨c⟩ = 0

If V is such that any three oriented edges are well split, then V is a split virtual structure.

Now think of α as coming with a bag full of things and offering them to β^{∗} and γ^{∗}; α’s bag is represented by its left unit ⟨w(α)⟩ and what β^{∗} and γ^{∗} want is something in their right unit ⟨w(β)⟩ and ⟨w(γ)⟩. The condition expresses that they are not going to quarrel.

Remember that composition was intuitively designed in such a way that edges were partially consumed in the process; now, dually, well-splitting makes sure that noboby else wanted to make use of the now forgotten part of any edge engaged in a composition. Another way to say this: if one composes β with α^{∗}, then from the point of view of γ, nothing changed (this intuition is formalized by the invariance theorem to come).

In the last section, we show how to build some split structures. For the time being we concentrate on their study.

Proposition 2 (Conservation of Splitness) Let V be a split structure. If V′ is obtained either by splitting, or by merging (hence also by composition) then V′ is a split structure. Thus if V′ is obtained by reduction of V, then it is split.

Proof: we use the notations of the definition of splitting and merging. Let’s first consider the splitting case and pick three distinct coincident oriented edges distinct in V′. The number of those edges concerned by the splitting of α (i.e., equal to α_{i} or α_{i}^{∗}) is 0, 1 or 2.

If it is 0 there is nothing to say.

If it is 1, we have to check that ⟨a_{i}^{(∗)}⟩⟨b⟩⟨c⟩ = 0. Set ω_{1} = π and ω_{2} = \overline{π}; we have ⟨a_{i}⟩ = ⟨ω_{i}a⟩ = ω_{i}⟨a⟩ and ⟨a_{i}^{∗}⟩ = ⟨a^{∗}ω_{i}⟩ = ⟨a^{∗}⟩⟨a^{∗}ω_{i}⟩. Since ⟨a^{(∗)}⟩⟨b⟩⟨c⟩ = 0 the result is obvious.

If it is 2 we have to check that ⟨a_{i}^{(∗)}⟩⟨a_{j}^{(∗)}⟩⟨c⟩ = 0 where a_{i}^{(∗)} and a_{j}^{(∗)} are distinct, then the same kind of computation yields the result.

Let’s consider now the merging case; the result follows from the computations: ⟨ab⟩ = abb^{∗}a^{∗} = a⟨b⟩a^{∗} = a⟨a^{∗}⟩a^{∗} = ⟨a⟩ and ⟨b^{∗}a^{∗}⟩ = b^{∗}a^{∗}ab = b^{∗}⟨a^{∗}⟩b = b^{∗}⟨b⟩b = ⟨b^{∗}⟩ showing that the right and left units of γ are respectively the same than the right unit of β and the left unit of α. •

5 Invariance of EX

Let V be a virtual structure, β, α two w-composable oriented edges and V′ the virtual structure obtained by composing β and α. We use the notations of definition 2.

We define the lifting morphism from C(G′) onto C(G) mapping ϕ to ϕ̂, by α̂_{2} = α, β̂_{2} = β, β̂_{1} :: α_{1} = βα, else γ̂ = γ.

Reciprocally, if ϕ is a path in C(G), one may define the derivate ϕ′ of ϕ in C(G′) by: ϕ′ is the path of C(G′) such that ϕ̂′ is ϕ and ϕ′ contains no subpath β_{2}α_{2} and α_{2}^{∗}β_{2}^{∗}. The unicity of ϕ′ is clear from the definition of the lifting morphism. Note that ϕ′ is the only path in V′ whose lifting in V is eventually regular; more precisely, if ψ is any path in V′ distinct from ϕ′ and such that ψ̂ = ϕ, then w(ψ) = 0. Indeed, since ψ̂ = ϕ and is distinct from ϕ′, it must contains a subpath β_{2}α_{2} (or α_{2}^{∗}β_{2}^{∗}). But we checked that these path have null weight.

We call direct path a path containing no subpath of the form ϕϕ^{∗} and straight path a regular direct path. The following lemma states a conservation law for weights of paths along virtual reduction.

Lemma 3 (Derivation) Let V be a virtual structure, ϕ a direct path in V with weight f linking vertice u to vertice v, β, α two w-composable oriented edges with weights b and a, and V′ the virtual structure obtained by composing them. Then the derivate ϕ′ of ϕ is a direct path with weight f′ satisfying:

f′ = π_{1}fπ_{2}

where:

π_{1} = \overline{a^{∗}}  if ϕ = ψβ \overline{b}  if ϕ = ψα^{∗} v ←^{1} v else

and

π_{2} = \overline{a^{∗}}  if ϕ = β^{∗}ψ \overline{b}  if ϕ = αψ u ←^{1} u else

Note that π_{2} = u ←^{1} u means that fπ_{2} = f since f = v ←^{x} u for some x in L*, being the weight of a path linking u to v. Same remark applies to π_{1}.

Proof: the fact that ϕ′ is direct is immediate from the definition. Let α′ and β′ be the residuals α_{2} and β_{2} of respectively α and β, a′ and b′ their weights and β :: α the new oriented edge. Thus a′ = a\overline{b} and b′ = \overline{a^{∗}}b. During the proof we use the following notations: ψ (resp. ψ_{0}) is a path, g (resp. g_{0}) its weight, ψ′ (resp. ψ′_{0}) its derivate by the βα composition and g′ (resp. g′_{0}) the weight of ψ′ (resp. ψ′_{0}); γ is an oriented edge, c its weight, γ′ its residual by the βα composition and c′ the weight of γ′.

The proof is by induction on the length of ϕ.

A. If ϕ is of length 1:

• if ϕ = α then ϕ′ = α′ and f′ = a′ = a\overline{b} which is just what the lemma states;

• if ϕ = β then ϕ′ = β′ and f′ = b′ = \overline{a^{∗}}b which is again what we need;

• if ϕ = α^{∗} or β^{∗} the result is the same;

• if ϕ = γ an oriented edge whose underlying edge is distinct from α and β’s ones then ϕ′ = γ so that f′ = f.

B. If ϕ = ψγ where γ is distinct from α and β^{∗}; then ϕ′ = ψ′γ′ and we have: f′ = c′g′. By induction on the length of ψ we get: g′ = π_{1}gπ_{2}, for some π_{1} and π_{2}. Hence f′ = c′π_{1}gπ_{2}. Note that π_{2} depends only on the oriented edge ψ (hence ϕ) starts with; thus, since by induction on ψ, π_{2} has the form stated by the lemma for ψ, it also has the good form for ϕ. It remains to show that c′π_{1}g is equal to π′_{1}cg for the right π′_{1}.

Now if γ = α^{∗} then c′ = \overline{b}a^{∗} = \overline{b}c; if γ = β then c′ = \overline{a^{∗}}b = \overline{a^{∗}}c and if γ is distinct from α, β, α^{∗}, β^{∗} then c′ = c. Thus we have:

f = cg and f′ = \begin{matrix}\overline{b}cπ_{1}gπ_{2} & if γ = α^{∗} \\ \overline{a^{∗}}cπ_{1}gπ_{2} & if γ = β \\ cπ_{1}gπ_{2} & if γ ≠ α^{∗}, β \end{matrix}

It suffices to show that cπ_{1}g = cd in any case to get the result. This is done by examining ψ:

• if ψ = ψ_{0}α^{∗} then ψ′ = ψ′_{0}α′^{∗}, g = a^{∗}g_{0} and g′ = \overline{b}a^{∗}g′_{0}, i.e. π_{1} = \overline{b}. Now, since we supposed that γ ≠ α, γ ≠ β^{∗} and β is w-composable with α (thus β and α^{∗} are distinct) we may apply the well splitting to γ^{∗}, β and α^{∗} which gives:

⟨c^{∗}⟩⟨b⟩⟨a^{∗}⟩ = 0
iff ⟨c^{∗}⟩\overline{b}⟨a^{∗}⟩ = ⟨c^{∗}⟩⟨a^{∗}⟩  by (13)
iff c⟨c^{∗}⟩\overline{b}⟨a^{∗}⟩a^{∗} = c⟨c^{∗}⟩⟨a^{∗}⟩a^{∗}
iff c\overline{b}a^{∗} = ca^{∗}  by (3)

Finally we get the wanted result: cπ_{1}g = c\overline{b}a^{∗}g_{0} = ca^{∗}g_{0} = cg.

• if ψ = ψ_{0}β the computation is similar, using the fact that γ^{∗}, β and α^{∗} are distinct so

by well splitting:

⟨c^{∗}⟩⟨a^{∗}⟩⟨b⟩ = 0

which is equivalent to:

c\overline{a^{∗}}b = cb

• if ψ is anything else then g′ = gπ_{2}, i.e., π_{1} = v ←^{1} v, wich immediately gives the result.

C. If ϕ = ψγα with γ ≠ β; Since γ may not be α^{∗} (otherwise ϕ is not a direct path), by induction on ψ_{0} = ψγ we have g′_{0} = g_{0}π_{2} = cgπ_{2} for some π_{2}; thus we may write:

f = acg and f′ = a\overline{b}cgπ_{2}

If we use the well-splitting property between α^{∗}, β and γ (they are distinct since: ϕ being direct γ ≠ α^{∗}; β and α being w-composable, β ≠ α^{∗}; and γ ≠ β by hypothesis) we obtain:

a\overline{b}c = ac which is just what we need to conclude.

D. If ϕ = ψβα; then ϕ′ = ψ′β :: α and f′ = abg′. At this point we have to check ψ:

• if ψ = ψ_{0}β, then, by induction on ψ, g′ = \overline{a^{∗}}bg_{0}π_{2}. We may use the well splitting of β^{∗}, β and α^{∗} because α ≠ β^{(∗)} by w-composability and β ≠ β^{∗}; we deduce:

b\overline{a^{∗}}b = bb

The result follows from:

f = abbg_{0} and f′ = ab\overline{a^{∗}}bg_{0}π_{2} = abbg_{0}π_{2}

• if ψ = ψ_{0}α^{∗} then a similar reasoning leads to the result.

• in any other case we have the result since, by induction on ψ, g′ = gπ_{2}.

E. If ϕ = ψβ^{∗}; we apply the same reasoning as in C. and D. •

Definition 5 (Execution Formula) The boundary of a a structure V = (G, w) is a set B of vertices of G satisfying: for any two oriented edges α and β whose goals are in B,

⟨a⟩⟨b⟩ = 0.

An execution path of the structure V with boundary B is a straight path linking two vertices in B. Thus an execution path ϕ is maximal in the sense that for any path ψ: w(ϕψ) = w(ψϕ) = 0.

Let us denote by C_{e}(G) the set of execution paths in G. The execution of V is a self-inverse element of L*_{+}(G) defined by:

EX(V) = ⨁_{ϕ∈C_{e}(G)} w(ϕ).

By definition of maximality, any two terms w(ϕ) and w(ϕ′) have disjoint domains and codomains, hence the ⊕.

A structure may have no boundary, thus a null execution. For instance the structure consisting in one node and one oriented edge with weight 1 has a null execution.

Theorem 4 (Invariance of EX) If V is a split virtual structure with boundary B, and V′ is obtained by reducing V, then, defining the boundary of V′ to be B, we have EX(V) = EX(V′); in other words, EX is an invariant of the reduction.

We may define the boundary of V′ to be B: let α′ and β′ be two oriented edges of V′ with weight a′ and b′ and whose goals are in B. Then α′ and β′ come from two oriented edges α = α̂′ and β = β̂′ with weights a and b and whose goals are in B. Thus ⟨a⟩⟨b⟩ = 0. But by the derivation lemma, a′ = π_{1}aπ_{2} and b′ = π′_{1}bπ′_{2} for some idempotents π_{1}, π_{2}, π′_{1} and π′_{2}. Hence ⟨a′⟩⟨b′⟩ = ⟨π_{1}aπ_{2}⟩⟨π′_{1}bπ′_{2}⟩ = ⟨π_{1}aπ_{2}⟩⟨a⟩⟨b⟩⟨π′_{1}bπ′_{2}⟩ = 0

Suppose V has a normal form (this need not be the case in general) then any regular path in V has length one (else one can compose along it), so EX(V) is trivially read on its normal form.

Proof: we first deal with a one step-reduction, i.e., a composition βα. Let ϕ be a maximal path in V. Using the notations of the derivation lemma we have for instance f′ = \overline{a^{∗}}fπ_{2} for some π_{2}. But this is the case if ϕ = ψβ, and since β is composable with α we deduce that ϕ is composable with α. ϕ being maximal, we must have w(ϕα) = af = 0 thus ⟨a^{∗}⟩f = 0, thus \overline{a^{∗}}f = f. Similarly: if ϕ = ψα^{∗} then \overline{b}f = f; if ϕ = β^{∗}ψ then f\overline{a^{∗}} = f and if ϕ = αψ then f\overline{b} = f. In any case f′ = f. In particular if ϕ is an execution path, then ϕ is maximal so that its derivate is an execution path of V′ (since the boundary of V′ is the same than the boundary of V) with same weight.

Reciprocally, let ϕ be an execution path in V′. Then ϕ̂ is an execution path of V since V and V′ have the same boundary. Furthermore (ϕ̂)′ = ϕ thus ϕ and ϕ̂ have the same weight.

The case of a general reduction follows immediately by an easy induction. •

6 Square-freedom

Definition 6 (Virtual Net) A virtual structure is square-free if for any straight path ϕ, w(ϕ)^{2} = 0.

A split and square-free virtual structure will be called a virtual net.

Henceforth, we shall only deal with virtual nets. This is the very reason why we didn’t define the composition of α with itself. If the structure is square-free, then the path αα has null weight which makes the composition αα useless.

Proposition 5 (Square-freedom invariance) Any reduction of a virtual net V leads to a virtual net.

Proof: since we already checked that splitness is invariant along the reduction, it remains to show that this is also the case for the square-freedom condition. It is a direct consequence of the derivation lemma. We first treat the case of a one-step reduction. Let V′ be the virtual structure obtained by composing β and α in V and ϕ′ a path in V′ such that ϕ′ϕ′ is a path. Let ϕ = ϕ̂′. Then it’s easy to see that ϕ is a path in V such that ϕϕ is a path and that the derivate of ϕ in V′ is ϕ′. Applying the lemma with f = w(ϕ), f′ = w(ϕ′) we obtain for some idempotents π_{1} and π_{2}:

f′ = π_{1}fπ_{2}
= π_{1}f⟨f^{∗}⟩π_{2} = π_{1}⟨f⟩fπ_{2}  by (3)
= π_{1}fπ_{2}⟨f^{∗}⟩ = ⟨f⟩π_{1}fπ_{2}  by (8)

From the hypothesis that V is a virtual net we deduce f^{2} = 0, hence ⟨f^{∗}⟩⟨f⟩ = 0 and then:

f^{′2} = π_{1}fπ_{2}⟨f^{∗}⟩⟨f⟩π_{1}fπ_{2} = 0

The general case of a reduction of length n is solved by an easy induction. •

7 Confluence

Lemma 6 (Local confluence) Let V be a virtual net, α, β, γ and δ some oriented edges in V such that β is w-composable with α and δ is w-composable with γ. Let V_{1} (resp. V_{2}) be the virtual net obtained by composing β and α (resp. δ and γ). Then there is a reduction ρ_{1} of V_{1} and a reduction ρ_{2} of V_{2} such that both ρ_{1} and ρ_{2} leads to the same virtual net V′.

Proof: let a, b, c and d be the weights of respectively α, β, γ and δ. If V′ is any virtual net obtained by reducing V and μ any oriented edge in V, we shall say “μ in V′” for “the residual of μ in V′”.

By definition of composition, V_{1} contains the following oriented edges:

α with weight a\overline{b}
β with weight \overline{a^{∗}}b
β :: α with weight ab

the other ones being the same as in V.

Taking in account the symmetry of the problem — the composition βα is the same as the composition α^{∗}β^{∗}, there are five possible situations for α, β, γ and δ:

1. the four underlying unoriented edges are distinct;

2. γ = α and the undelying unoriented edges of α, β and δ are distinct; the two compositions are βα and δα.

3. δ = α and the underlying edges of α, β and γ are distinct; the two compositions are βα and αγ.

4. γ = α and δ = β^{∗}; the two compositions are βα and β^{∗}α. In this case we must have that the underlying edges of α and β are distinct otherwise the composition βα is not defined.

5. δ = α and γ = β; the two compositions are βα and αβ. The same remark applies.

1. If the four underlying edges are distinct, the result is immediate: in V_{1}, compose δ and γ whose weights are the same than in V; in V_{2}, compose β and α whose weights are the same than in V. Then both V_{1} and V_{2} reduce in the same V′.

2. Compositions βα and δα: since β and δ are distinct and composable with α, by splitness we have:

⟨a^{∗}⟩⟨b⟩⟨d⟩ = 0

If we compose δ and α in V_{1} we obtain V′ in which we have:

α with weight a\overline{b} \overline{d}
β with weight \overline{a^{∗}}b
δ with weight \overline{\overline{b}a^{∗}}d
β :: α with weight ab
δ :: α with weight a\overline{b}d

the other oriented edges being unchanged. The splitness condition above is equivalent to:

a\overline{b}d = ad

Hence we have the following computation:

\overline{\overline{b}a^{∗}}d = d\overline{d^{∗}\overline{b}a^{∗}}  by (6)
= d\overline{d^{∗}a^{∗}}
= \overline{a^{∗}}d  by (6)

Finally, in V′ we have:

α with weight a\overline{b} \overline{d}
β with weight \overline{a^{∗}}b
δ with weight \overline{a^{∗}}d
β :: α with weight ab
δ :: α with weight ad

The result is symmetrical in β and δ thus if we exchange them we show that V_{2} reduces in V′ by composing β and α.

3. Compositions βα and αγ: Let’s compose α and γ in V_{1} obtaining V′_{1} which contains: α with weight \overline{c^{∗}}a\overline{b}, γ with weight c\overline{a\overline{b}}, α :: γ with weight ca\overline{b}. Now let’s compose β :: α with γ. We obtain V′ in which we have: γ with weight c\overline{a\overline{b}} \overline{ab} = c\overline{a}

by (9), β :: α with weight \overline{\overline{a\overline{b}}c^{∗}}ab and β :: α :: γ with weight c\overline{a\overline{b}}ab, the other oriented edges being unchanged. Furthermore we have:

c\overline{a\overline{b}}ab = ca\overline{\overline{b}}b  by (6)
= cab  by (11)

and:

\overline{\overline{a\overline{b}}c^{∗}}ab = ab\overline{b^{∗}a^{∗}\overline{a\overline{b}}c^{∗}}  by (6)
= ab\overline{b^{∗}a^{∗}c^{∗}}
= \overline{c^{∗}}ab  by (6)

Finally V′ contains:

α with weight \overline{c^{∗}}a\overline{b}
β with weight \overline{a^{∗}}b
γ with weight c\overline{a}
β :: α with weight \overline{c^{∗}}ab
α :: γ with weight ca\overline{b}
β :: α :: γ with weight cab

Again the situation is symmetrical if we exchange β and γ; thus if we reduce V_{2} by composing β and α, then β with α :: γ we obtain the same V′.

4. Compositions βα and β^{∗}α: both β and β^{∗} are composable with α; thus α^{∗}, β and β^{∗} are three distinct coincident edges so that we have by splitness ⟨b^{∗}⟩⟨b⟩⟨a^{∗}⟩ = 0; this is, by (13) equivalent to:

b\overline{b}a^{∗} = ba^{∗}

Note that by square-freedom, we also have b^{2} = 0 which is equivalent to b\overline{b} = b. This implies the above equation. Nevertheless, we only need the former one for the proof.

Let’s compose β^{∗} and α in V_{1}, obtaining V′_{1} in which we have: α with weight a\overline{b} \overline{b^{∗}\overline{a^{∗}}}, β with weight \overline{a^{∗}}b\overline{\overline{b}a^{∗}}, β :: α with weight ab and β^{∗} :: α with weight a\overline{b}b^{∗}\overline{a^{∗}}. Now, by splitness we have a\overline{b}b^{∗}\overline{a^{∗}} = ab^{∗}\overline{a^{∗}}. Furthermore, we may prove that:

\overline{a^{∗}}b\overline{\overline{b}a^{∗}} = \overline{a^{∗}} \overline{b\overline{b}a^{∗}}b  by (6)
= \overline{a^{∗}} \overline{ba^{∗}}b  by splitness
= \overline{a^{∗}}b\overline{a^{∗}}  by (6)

So that in V′_{1} we have: β with weight \overline{a^{∗}}b\overline{a^{∗}}, β^{∗} :: α with weight ab^{∗}\overline{a^{∗}}. We now reduce V′_{1} by composing α^{∗} and β :: α obtaining V′ which contains: α with weight

a\overline{b} \overline{b^{∗}\overline{a^{∗}}} \overline{b^{∗}a^{∗}} = a\overline{b} \overline{b^{∗}} by (9), β :: α with weight ab\overline{\overline{b^{∗}\overline{a^{∗}}} \overline{b}a^{∗}} and α^{∗} :: β :: α with weight ab\overline{b^{∗}\overline{a^{∗}}} \overline{b}a^{∗}. Using the splitness equation, we have:

ab\overline{b^{∗}\overline{a^{∗}}} \overline{b}a^{∗} = a\overline{\overline{a^{∗}}}b\overline{b}a^{∗}  by (6)
= ab\overline{b}a^{∗}  by (11)
= aba^{∗}

and that

ab\overline{\overline{b^{∗}\overline{a^{∗}}} \overline{b}a^{∗}} = \overline{ab\overline{b^{∗}\overline{a^{∗}}} \overline{b}a^{∗}}ab  by (6)

= \overline{aba^{∗}}ab
= ab\overline{a^{∗}}  by (6)

so that V′ finally contains:

α with weight a\overline{b} \overline{b^{∗}}
β with weight \overline{a^{∗}}b\overline{a^{∗}}
β :: α with weight ab\overline{a^{∗}}
β^{∗} :: α with weight ab^{∗}\overline{a^{∗}}
α^{∗} :: β :: α with weight aba^{∗}

Now if we exchange β with β^{∗} in the whole computation, the result is unchanged since (α^{∗} :: β :: α)^{∗} = α^{∗} :: β^{∗} :: α and (aba^{∗})^{∗} = ab^{∗}a^{∗}. This shows that if we compose β with α, then α^{∗} with β^{∗} :: α in V_{2} we obtain the same virtual net V′.

5. Compositions βα and αβ: If we can compose β with α and α with β, it must be that αβαβ and βαβα are some paths in V. Thus by square-freedom we have baba = 0 and abab = 0. This is equivalent to:

aba\overline{b} = aba
\overline{b^{∗}}aba = aba
bab\overline{a} = bab
\overline{a^{∗}}bab = bab

Let’s compose α and β in V_{1}. We obtain V′_{1} in which we have: α with weight \overline{b^{∗}\overline{a^{∗}}}a\overline{b}, β with weight \overline{a^{∗}}b\overline{a\overline{b}} and α :: β with weight \overline{a^{∗}}ba\overline{b}. Now let’s compose α with β :: α obtaining V′′_{1} in which we have:

α with weight \overline{b^{∗}a^{∗}} \overline{b^{∗}\overline{a^{∗}}}a\overline{b} = \overline{b^{∗}}a\overline{b} by (9)
β with weight \overline{a^{∗}}b\overline{a\overline{b}}
β :: α with weight ab\overline{\overline{b^{∗}\overline{a^{∗}}}a\overline{b}} = ab\overline{a}
α :: β with weight \overline{a^{∗}}ba\overline{b}
α :: β :: α with weight ab\overline{b^{∗}\overline{a^{∗}}}a\overline{b} = aba

since we have:

ab\overline{b^{∗}\overline{a^{∗}}}a\overline{b} = a\overline{\overline{a^{∗}}}ba\overline{b}  by (6)
= aba\overline{b}  by (11)
= aba  by square-freedom of βα

and

ab\overline{\overline{b^{∗}\overline{a^{∗}}}a\overline{b}} = \overline{ab\overline{b^{∗}\overline{a^{∗}}}a\overline{b}}ab  by (6)

= \overline{aba}ab
= ab\overline{a}  by (6)

We define V′ to be obtained from V′′_{1} by composing β :: α with β so that in V′ we have: β

with weight \overline{a^{∗}}b\overline{a\overline{b}} \overline{ab\overline{a}}, β :: α with weight \overline{\overline{a\overline{b}}b^{∗}\overline{a^{∗}}}ab\overline{a} and β :: α :: β with weight \overline{a^{∗}}b\overline{a\overline{b}}ab\overline{a}. Now we have:

\overline{a^{∗}}b\overline{a\overline{b}}ab = \overline{a^{∗}}ba\overline{\overline{b}}b  by (6)
= \overline{a^{∗}}bab  by (13)
= bab  by square-freedom of βα

from which one deduces, again by square-freedom of βα, that the weight of β :: α :: β is bab\overline{a} = bab and that the weight of β :: α is \overline{b^{∗}}ab\overline{a}. Let’s now simplify the weight of β:

\overline{a^{∗}}b\overline{a\overline{b}} \overline{ab\overline{a}} = \overline{a^{∗}}\overline{ba\overline{b}}b\overline{ab\overline{a}}  by (6)
= \overline{a^{∗}}\overline{ba\overline{b}} \overline{bab\overline{a}}b  by (6)
= \overline{a^{∗}}\overline{ba\overline{b}} \overline{bab}b by square-freedom of αβ
= \overline{a^{∗}}\overline{ba\overline{b}}b\overline{ab}  by (6)
= \overline{a^{∗}}b\overline{a\overline{b}} \overline{ab}  by (6)
= \overline{a^{∗}}b\overline{a}  by (9)

Finally V′ is defined by:

α with weight \overline{b^{∗}}a\overline{b}
β with weight \overline{a^{∗}}b\overline{a}
β :: α with weight \overline{b^{∗}}ab\overline{a}
α :: β with weight \overline{a^{∗}}ba\overline{b}
α :: β :: α with weight aba
β :: α :: β with weight bab

The result follows immediately from the symmetry between α and β. Note this case is the only one in which we used square-freedom. •

Theorem 7 (Confluence) The virtual reduction of virtual nets is confluent.

Proof: we use a standard lemma in confluence proofs: if ρ_{0} is any confluent relation on a set X and if ρ is the transitive cloture of ρ_{0} then ρ is confluent.

Let Φ be the set of paths of length 3 in the virtual net V. Note that Φ is finite since a virtual net is a finite graph. We say that a reduction ρ of V is a ρ_{0}-reduction if at any step of the reduction ρ, the oriented edges β and α being composed are such that the path βα is a subpath of the derivate of an element of Φ. Thus, at least one derivate of an element of Φ stricly decreases at each step of a ρ_{0}-reduction. Since the number of derivates of the elements of Φ is left unchanged by any reduction we deduce that the ρ_{0}-reductions of V are notherian. Now if we inspect the proof of local confluence, we see that all the reductions involved are ρ_{0}-reductions; thus the ρ_{0}-reductions of V are confluent. To end the proof it suffices to show that the transitive cloture of the ρ_{0}-reductions of V is the set of all reductions of V which is clear. •

8 More algebraic material

In order to embed λ-calculus into virtual nets, we first have to build in L* the following items:

— two multiplicative coefficients p and q such that:

p^{∗}p = q^{∗}q = 1,  p^{∗}q = q^{∗}p = 0.

— a morphism !, i.e.:

\begin{aligned}!(1) & = & 1, & !(0) & = & 0, \\ !(a)!(b) & = & !(ab), & !(a)^{∗} & = & !(a^{∗}). \end{aligned}

— for each two integers c and i, an exponential coefficient x_{ci} such that:

x_{ci}^{∗}x_{dj} = 0 if i ≠ j
x_{ci}^{∗}x_{ci} = 1
!(a) x_{ci} = x_{ci}!^{c}(a)

The integer c is the lift of x_{ci} and the integer i is the name of x_{ci}.

A possible way to do this is:

— let p (resp. q) be the partial transformation defined on by: p(n) = 2n (resp. 2n + 1).

— let φ : (n, m) → φ(n, m) = ⌈n, m⌉ be a one-to-one map from ^{2} onto . If x is a partial transformation, we denote by !(x) the partial transformation defined by:

!(x)⌈n, m⌉ = ⌈n, x(m)⌉

It is easy to see that ! is an isomorphism of L* into itself.

We shall denote by ⌈n_{1}, …, n_{k}⌉ the integer ⌈n_{1}, ⌈n_{2}, …, ⌈n_{k−1}, n_{k}⌉ …⌉⌉. By definition of φ, for any n and for any k > 0, n may be uniquely written as: n = ⌈n_{1}, …, n_{k}⌉. Hence, for all k we have:

!^{k}(x)⌈n_{1}, …, n_{k}, n_{k+1}⌉ = ⌈n_{1}, …, n_{k}, x(n_{k+1})⌉

For each two integers i and c, we define x_{ci} by:

x_{ci}⌈n_{1}, …, n_{c}, n_{c+1}⌉ = ⌈⌈i, n_{1}, …, n_{c}⌉, n_{c+1}⌉

9 Embedding lambda-calculus

We now show how to translate a λ-term T in a virtual structure T^{v} with a boundary B_{T}. The construction is by induction on the terms. Let x_{1}, …, x_{n} be the free occurrences of variables in T, then T^{v} has the form:

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} … x_{c_{n}n} T^{v} x_{c_{1}1}

The x_{c_{i}i}’s are the weights of the “free occurrences” of T^{v} and are defined by the translation. The goals of the free occurrences of T^{v} and the root of T^{v} are all the vertices in the boundary of T^{v}.

— x_{1}^{v} is:

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} x_{01}

— (UV)^{v} is:

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} p^{∗} U^{v}  !(V^{v}) q x_{c_{j}j}  x_{c_{i}+1 n+i}

where n is the number of occurrences of free variables in U and !(V^{v}) means that the weight of each oriented edge inside V^{v} gets a !.

— (λx.U)^{v} is:

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} q^{∗} p^{∗}  U^{v} x_{c_{1}i_{1}} x_{c_{k}i_{k}}  x_{ci}

where x_{i_{1}}, …, x_{i_{k}} are the occurrences of x in U (k is possibly zero).

For example, ((λx.xx)λx.xx)^{v} is represented on the figure below.

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} q^{∗} p^{∗} p^{∗}  q  p^{∗} q  !(q^{∗}) !(q) !(p^{∗})  !(p^{∗}) x_{12} x_{01}  !(x_{14}) !(x_{03})

Theorem 8 For any term T, the virtual structure T^{v} is split and square-free; in other words it is a virtual net.

Square-freedom for λ-calculus was proved in [6] and splitness is easily proved by induction on T.

References

[1] Martin Abadi, Georges Gonthier, and Jean-Jacques Lévy. Linear logic without boxes. In Proceedings LICS, 1992.

[2] A.H. Clifford and G.B. Preston. The algebraic theory of semi-groups. In Mathematical Surveys, volume 7. A.M.S., 1961.

[3] Vincent Danos. Une Application de la Logique Linéaire à l’Étude des Processus de Normalisation (principalement du λ-calcul). PhD thesis, Université Paris 7, June 1990.

[4] Vincent Danos and Laurent Regnier. Mechanization of virtual reduction. Draft, December 1992.

[5] Jean-Yves Girard. Geometry of interaction 1: an interpretation of system F. In Proceedings of A.S.L. Meetings, 1988.

[6] Pasquale Malacaria and Laurent Regnier. Some results on the interpretation of λ-calculus in operator algebras. In Proceedings L.I.C.S., 1991.

[7] Mario Petrich. Inverse Semigroups. Pure and Applied Mathematics. John Wiley & sons, 1984.

[8] Laurent Regnier. Lambda-Calcul et Réseaux. PhD thesis, Université Paris 7, January 1992.