theoremrubric theorem corollaryrubric corollary lemmarubric lemma
propositionrubric proposition definitionrubric definition remarkrubric remark

# Interaction Graphs: Exponentials

Thomas Seiller111Institut des Hautes Études Scientifiques (IHÉS) Le Bois-
Marie, 35 Route de Chartres, 91440 Bures-sur-Yvette, France222This work was
partially supported by the ANR project ANR-10-BLAN-0213 LOGOI
<EMAIL_ADDRESS>
# Interaction Graphs: Exponentials

Thomas Seiller111Institut des Hautes Études Scientifiques (IHÉS) Le Bois-
Marie, 35 Route de Chartres, 91440 Bures-sur-Yvette, France222This work was
partially supported by the ANR project ANR-10-BLAN-0213 LOGOI
<EMAIL_ADDRESS>
###### Abstract

This paper is the fourth of a series [Sei12a, Sei14a, Sei14c] exposing a
systematic combinatorial approach to Girard’s Geometry of Interaction program
[Gir89b]. This program aims at obtaining particular realizability models for
linear logic that accounts for the dynamics of cut-elimination. This fourth
paper tackles the complex issue of defining exponential connectives in this
framework. In order to succeed in this, we use the notion of _graphings_ , a
generalization of graphs which was defined in earlier work [Sei14c]. We
explain how we can use this framework to define a GoI for Elementary Linear
Logic (ELL) with second-order quantification, a sub-system of linear logic
that captures the class of elementary time computable functions.

###### Contents

  1. 1 Introduction
  2. 2 Interaction Graphs
  3. 3 Thick Graphs and Contraction
  4. 4 Construction of an Exponential Connective on the Real Line
  5. 5 Soundness for Behaviors
  6. 6 Contraction and Soundness for Polarized Conducts
  7. 7 Conclusion and Perspectives

##  1 Introduction

###  1.1 Geometry of Interaction

A Geometry of Interaction (GoI) model, i.e. a construction that fulfills the
GoI research program [Gir89b], is in a first approximation a representation of
linear logic proofs that accounts for the dynamics of cut-elimination. A proof
is no longer a morphism from $A$ to $B$ — a function from $A$ into $B$ — but
an operator acting on the space $A\oplus B$. As a consequence, the modus
ponens is no longer represented by composition. The operation representing
cut-elimination, i.e. the obtention of a cut-free proof of $B$ from a cut-free
proof of $A$ and a cut-free proof of $A\multimap B$, consists in constructing
the solution to an equation called the _feedback equation_ (illustrated in
Figure 2). A GoI model hence represents both the proofs and the dynamics of
their normalization. Contrarily to denotational semantics, a proof $\pi$ and
its normalized form $\pi^{\prime}$ are not represented by the same object.
However, they remain related since the normalization procedure has a
semantical counterpart — the execution formula $\textnormal{Ex}(\cdot)$ —
which satisfies $\textnormal{Ex}(\pi)=\pi^{\prime}$. This essential difference
between denotational semantics and GoI is illustrated in Figure 1.

$\pi$$\lVert\pi\rVert$$\rho$$\lVert\rho\rVert$$\lVert\cdot\rVert$$\lVert\cdot\rVert$cutelimination
(a) Denotational Semantics

$\pi$$\lVert\pi\rVert$$\rho$$\lVert\rho\rVert$$\lVert\cdot\rVert$$\lVert\cdot\rVert$cutelimination$\textnormal{Ex}(\cdot)$
(b) Geometry of Interaction

Figure 1: Denotational Semantics vs Geometry of Interaction

$P\in\mathcal{L}(\mathbb{H\oplus K})$ represents 333Here, $\mathbb{H}$ and
$\mathbb{K}$ are separable infinite-dimensional Hilbert spaces, and
$\mathcal{L}(\star)$ denotes the set of operators acting on the Hilbert space
$\star$: bounded (or, equivalently, continuous) linear maps from $\star$ to
$\star$. a program/proof of implication $A\in\mathcal{L}(\mathbb{H})$
represents an argument. $R\in\mathcal{L}(\mathbb{K})$ represents the result of
the computation if:
$R(\xi)=\xi^{\prime}\Leftrightarrow\exists\eta,\eta^{\prime}\in\mathbb{H},\left\\{\begin{array}[]{lcl}P(\eta\oplus\xi)&=&\eta^{\prime}\oplus\xi^{\prime}\\\
A(\eta^{\prime})&=&\eta\end{array}\right.$

(a) Formal statement

$\mathbb{H}$$\xi$$\mathbb{K}$$A$$P$$A(\eta)$$\mathbb{H}$$\xi^{\prime}$$\mathbb{K}$$\eta$
(b) Illustration of the equation

Figure 2: The Feedback Equation

The GoI program has a second aim: define by realizability techniques a
reconstruction of logical operations from the dynamical model just exposed.
The objects of study in a GoI construction are a generalization of the notion
of proof — paraproofs, in the same sense the proof structure where a
generalization of the notion of sequent calculus proof. This is reminiscent of
game semantics where not all strategies are interpretations of programs, or
Krivine’s classical realizability [Kri01, Kri09] where terms containing
continuation constants are distinguished from “proof-like terms”. This point
of view allows a reconstruction of logic as a description of how paraproofs
interact. It is therefore a sort of ”discursive syntax” where paraproofs are
opposed one to another, where they argue together in a way reminiscent of game
semantics, each one trying to prove the other wrong. This argument terminates
when one of them gives up. The discussion itself corresponds to the execution
formula, which describes the solution to the feedback equation and generalizes
the cut-elimination procedure to this generalized notion of proofs. Two
paraproofs are then said _orthogonal_ — denoted by the symbol $\simperp$ —
when this arguement (takes place and) terminates. A notion of formula is then
drawn from this notion of orthogonality: a formula is a set of paraproofs $A$
equal to its bi-orthogonal closure $A^{\simbot\simbot}$ or, equivalently, a
set of paraproofs $A=B^{\simbot}$ which is the orthogonal to a given set of
paraproofs $B$.

Drawing some intuitions from the Curry-Howard correspondence, one may propose
an alternative reading to this construction in terms of programs. Since proofs
correspond to well-behaved programs, paraproofs are a generalization of those,
representing somehow _badly-behaved programs_. If the orthogonality relation
represents negation from a logical point of view, it represents a notion of
_testing_ from a computer science point of view. The notion of formula defined
from it corresponds to a notion of type, defined interactively from how
(para)programs behave. This point of view is still natural when thinking about
programs: a program is of type $\mathbf{nat}\rightarrow\mathbf{nat}$ because
it produces a natural number when given a natural number as an argument. On
the logical side, this change may be more radical: a proof is a proof of the
formula $\text{Nat}\Rightarrow\text{Nat}$ because it produces a proof of Nat
each time it is cut (applied) to a proof of Nat.

Once the notion of type/formula defined, one can reconstruct the connectives:
from a ”low-level” — between paraproofs — definition, one obtains a ”high-
level” definition — between types. For instance, the connective $\otimes$ is
first defined between any two paraproofs $\mathfrak{a,b}$, and this definition
is then extended to types by defining $A\otimes
B=\\{\mathfrak{a}\otimes\mathfrak{b}\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathfrak{a}\in A,\mathfrak{b}\in B\\}^{\simbot\simbot}$. As a consequence,
the connectives are not defined in an _ad hoc_ way, but their definition is a
consequence of their computational meaning: the connectives are defined on
proofs/programs and their definition at the level of types is just the
reflection of the interaction between the execution — the dynamics of proofs —
and the low-level definition on paraproofs. Logic thus arises as generated by
computation, by the normalization of proofs: types/formulas are not there to
tame the programs/proofs but only to describe their behavior. This is
reminiscent of realizability in the sense that a type is defined as the set of
its (para-)proofs. Of course, the fact that we consider a generalized notion
of proofs from the beginning has an effect on the construction: contrarily to
usual realizability models (except from classical realizability in the sense
of Krivine [Kri01, Kri09]), the types $A$ and $A^{\simbot}$ (the negation of
$A$) are in general both non-empty. This is balanced by the fact that one can
define a notion of successful paraproofs, which corresponds in a way to the
notion of winning strategy in game semantics. This notion on paraproofs then
yields a high-level definition: a formula/type is _true_ when it contains a
successful paraproof.

###  1.2 Interaction Graphs and Graphings

Interaction Graphs were first introduced [Sei12a] to define a combinatorial
approach to Girard’s geometry of interaction in the hyperfinite factor
[Gir11]. The main idea was that the execution formula — the counterpart of the
cut-elimination procedure — can be computed as the set of alternating paths
between graphs, and that the measurement of interaction defined by Girard
using the Fuglede-Kadison determinant [FK52] can be computed as a measurement
of a set of cycles.

The setting was then extended to deal with additive connectives [Sei14a],
showing by the way that the constructions were a combinatorial approach not
only to Girard’s hyperfinite GoI construction but also to all the earlier
constructions [Gir87, Gir89a, Gir88, Gir95a]. This result could be obtained by
unveiling a single geometrical property, which we called the _trefoil
property_ , upon which all the constructions of geometry of interaction
introduced by Girard are built.

In a third paper, we explored a wide generalization of the graph
framework444This generalization, or more precisely a fragment of it, already
appeared in the author’s PhD thesis [Sei12b].. We introduced the notion of
_graphing_ which we now informally describe. If $(X,\mathcal{B},\mu)$ is a
measured space and $\mathfrak{m}$ is a monoid of measurable maps555For
technical reasons, we in fact consider monoids of Borel-preserving non-
singular maps [Sei14c]. $X\rightarrow X$ (the internal law is composition),
then a graphing in $\mathfrak{m}$ is a countable family of restrictions of
elements of $\mathfrak{m}$ to measurable subsets. These restrictions of
elements of $\mathfrak{m}$ are regarded as edges of a graph _realized_ as
measurable (partial) maps. We showed that the notions of paths and cycles in a
graphing could be defined. As a consequence, one can define the _execution_ as
the set of alternating paths between graphings, mimicking the corresponding
operation of graphs. On the other hand, a more complex argument shows that one
can define appropriate measures of cycles in order to insure that the trefoil
property holds. As a consequence, we obtained whole hierarchies of models of
multiplicative-additive linear logic in this way. The purpose of this paper is
to exhibit a family of such models in which one can interpret Elementary
Linear Logic [Gir95b, DJ03] with second-order quantification.

###  1.3 Outline of the paper

In Section 2, we recall some important definitions and properties on directed
weighted graphs. This allows us to introduce important notations that will be
used later on. We then recall some definitions and properties about the
additive construction [Sei14a]. These properties are essential to the
understanding of the construction of the multiplicative-additive fragment of
linear logic in the setting of interaction graphs.

In Section 3, we define and study the notion of _thick graphs_ , and show how
it can be used to interpret the contraction $\mathbf{\oc A\multimap\oc
A\otimes\oc A}$ for some specific formulas $\mathbf{A}$. This motivates the
definition of a _perennisation_ $\Omega$ from which one can define an
exponential $\mathbf{A}\mapsto\mathbf{\oc_{\Omega}A}$. We also explain why it
is necessary to work with a generalization of graphs, namely graphings, in
order to define perennisations that are suitably expressive.

In Section 4, we give a definition of an exponential connective defined from a
suitable notion of perennisation. We show for this a result which allows us to
encode any bijection over the natural numbers as a measure-preserving map over
the unit interval of the real line. This result is then used to encode some
combinatorics as measure-preserving maps and show that functorial promotion
can be implemented for the exponential we defined.

We then prove a soundness result for a variant (in Section 5) of Elementary
Linear Logic (ELL). This result, though interesting, is not ideal since we
restrict to proofs that are in some sense ”intuitionnistic”. Indeed, for
technical reasons explained later on, the introduction of exponentials cannot
be performed without being associated to a tensor product. Since the
interpretation of elementary time functions in ELL relies heavily on those
proofs that are not intuitionnistic in this sense666This fact was pointed out
to the author by Damiano Mazza..

Consequently, we introduce (in Section 6) a notion of polarities which
generalize the notion of _perennial/co-perennial_ formulas defined before. The
discussion on polarities leads to a refinement of the sequent calculus
considered in the previous section which does not suffer from the drawbacks
explained above. We then prove a soundness result for this calculus.

##  2 Interaction Graphs

###  2.1 Basic Definitions

Departing from the realm of infinite-dimensional vector spaces and linear maps
between them, we proposed in previous work [Sei12a, Sei14a] a graph-
theoretical construction of GoI models. We give here a brief overview of the
main definitions and results. The graphs we consider are directed and
weighted, where the weights are taken in a _weight monoid_ $(\Omega,\cdot)$.

######  Definition .

A _directed weighted graph_ is a tuple $G$, where $V^{G}$ is the set of
vertices, $E^{G}$ is the set of edges, $s^{G}$ and $t^{G}$ are two functions
from $E^{G}$ to $V^{G}$, the _source_ and _target_ functions, and $\omega^{G}$
is a function $E^{G}\rightarrow\Omega$.

The construction is centered around the notion of alternating paths. Given two
graphs $F$ and $G$, an alternating path is a path $e_{1}\dots e_{n}$ such that
$e_{i}\in E^{F}$ if and only if $e_{i+1}\in E^{G}$. The set of alternating
paths will be used to define the interpretation of cut-elimination in the
framework, i.e. the graph $F\mathop{\mathopen{:}\mathclose{:}}G$ — the
_execution of $F$ and $G$_ — is defined as the graph of alternating paths
between $F$ and $G$ whose source and target are in the symmetric difference
$V^{F}\Delta V^{G}$. The weight of a path is naturally defined as the product
of the weights of the edges it contains.

######  Definition .

Let $F,G$ be directed weighted graphs. The set of alternating paths between
$F$ and $G$ is the set of paths $e_{0},e_{1},\dots,e_{n}$ such that $e_{i}\in
E^{G}\Rightarrow e_{i+1}\in E^{F}$ and $e_{i}\in E^{F}\Rightarrow e_{i+1}\in
E^{G}$. We write $\text{{Path}}(F,G)$ the set of such paths, and
$\text{{Path}}(F,G)_{V}$ the subset of $\text{{Path}}(F,G)$ containing the
paths whose source and target lie in $V$.

The execution $F\mathop{\mathopen{:}\mathclose{:}}G$ of $F$ and $G$ is then
defined by:

$\displaystyle V^{F\mathop{\mathopen{:}\mathclose{:}}G}$ $\displaystyle=$
$\displaystyle V^{F}\Delta V^{G}$ $\displaystyle
E^{F\mathop{\mathopen{:}\mathclose{:}}G}$ $\displaystyle=$
$\displaystyle\text{{Path}}(F,G)_{V^{F\mathop{\mathopen{:}\mathclose{:}}G}}$

where the source and target maps are naturally defined, and the weight of a
path is the product of the weights of the edges it is composed of.

As it is usual in mathematics, this notion of paths cannot be considered
without the associated notion of cycle: an _alternating cycle_ between two
graphs $F$ and $G$ is a cycle which is an alternating path $e_{1}e_{2}\dots
e_{n}$ such that $e_{1}\in V^{F}$ if and only if $e_{n}\in V^{G}$. For
technical reasons, we actually consider the related notion of $1$-circuit.

######  Definition .

A _$1$ -circuit_ is an alternating cycle $\pi=e_{1}\dots e_{n}$ which is not a
proper power of a smaller cycle. In mathematical terms, there do not exists a
cycle $\rho$ and an integer $k$ such that $\pi=\rho^{k}$, where the power
represents iterated concatenation.

We denote by $\mathcal{C}(F,G)$ the set of $1$-circuits in the following. We
show that these notions of paths and cycles satisfy a property we call the
_trefoil property_ which will turn out to be fundamental. The trefoil property
states that there exists weight-preserving bijections:

$\mathcal{C}(F\mathop{\mathopen{:}\mathclose{:}}G,H)\cup\mathcal{C}(F,G)\cong\mathcal{C}(G\mathop{\mathopen{:}\mathclose{:}}H,F)\cup\mathcal{C}(G,H)\cong\mathcal{C}(H\mathop{\mathopen{:}\mathclose{:}}F,G)\cup\mathcal{C}(H,F)$

We showed, based only on the trefoil property, how one can define the
multiplicative and additive connectives of Linear Logic, obtaining a model
fulfilling the GoI research program. This construction is moreover
parametrized by a map from the set $\Omega$ to $\mathbb{R}_{\geqslant
0}\cup\\{\infty\\}$, and therefore yields not only one but a whole family of
models. This parameter is introduced to define the notion of orthogonality in
our setting, a notion that account for linear negation. Indeed, given a map
$m$ and two graphs $F,G$ we define
$\mathopen{\llbracket}F,G\mathclose{\rrbracket}_{m}$ as the sum
$\sum_{\pi\in\mathcal{C}(F,G)}m(\omega(\pi))$, where $\omega(\pi)$ is the
weight of the cycle $\pi$. The orthogonality is then constructed from this
measurement.

We moreover showed how, from any of these constructions, one can obtain a
$\ast$-autonomous category $\mathfrak{Graph}_{MLL}{}$ with
$\parr\not\cong\otimes$ and $1\not\cong\bot$, i.e. a non-degenerate
denotational semantics for Multiplicative Linear Logic (MLL). However, as in
all the versions of GoI dealing with additive connectives, our construction of
additives does not define a categorical product. We solve this issue by
introducing a notion of _observational equivalence_ within the model. We are
then able to define a categorical product from our additive connectives when
considering classes of observationally equivalent objects, thus obtaining a
denotational semantics for Multiplicative Additive Linear Logic (MALL).

###  2.2 Models of MALL in a Nutshell

We recall the basic definitions of projects, and behaviors, which will be
respectively used to interpret proofs and formulas, as well as the definition
of connectives.

  * •

a _project_ of carrier $V^{A}$ is a triple $\mathfrak{a}=(a,V^{A},A)$, where
$a$ is a real number, $A=\sum_{i\in I^{A}}\alpha^{A}_{i}A_{i}$ is a finite
formal (real-)weighted sum of graphings of carrier included in $V^{A}$;

  * •

two projects $\mathfrak{a,b}$ are _orthogonal_ when:

$\mathopen{\ll}\mathfrak{a},\mathfrak{b}\mathclose{\gg}_{m}=a(\sum_{i\in
I^{A}}\alpha^{B}_{i})+b(\sum_{i\in I^{B}}\alpha^{B}_{i})+\sum_{i\in
I^{A}}\sum_{j\in
I^{B}}\alpha_{i}^{A}\alpha^{B}_{j}\mathopen{\llbracket}A_{i},B_{j}\mathclose{\rrbracket}_{m}\neq
0,\infty$

  * •

the _execution_ of two projects $\mathfrak{a,b}$ is defined as:

$\mathfrak{a\mathop{\mathopen{:}\mathclose{:}}b}=(\mathopen{\ll}\mathfrak{a},\mathfrak{b}\mathclose{\gg}_{m},V^{A}\Delta
V^{B},\sum_{i\in I^{A}}\sum_{j\in
I^{B}}\alpha^{A}_{i}\alpha^{B}_{j}A_{i}\mathop{\mathopen{:}\mathclose{:}}B_{j})$

  * •

if $\mathfrak{a}$ is a project and $V$ is a measurable set such that
$V^{A}\subset V$, we define the extension $\mathfrak{a}_{\uparrow V}$ as the
project $(a,V,A)$;

  * •

a _conduct_ $\mathbf{A}$ of carrier $V^{A}$ is a set of projects of carrier
$V^{A}$ which is equal to its bi-orthogonal $\mathbf{A}^{\simbot\simbot}$;

  * •

a _behavior_ $\mathbf{A}$ of carrier $V^{A}$ is a conduct such that for all
$\lambda\in\mathbf{R}$,

$\begin{array}[]{rcl}\mathfrak{a}\in\mathbf{A}&\Rightarrow&\mathfrak{a+\lambda
0}\in\mathbf{A}\\\
\mathfrak{b}\in\mathbf{A}^{\simbot}&\Rightarrow&\mathfrak{b+\lambda
0}\in\mathbf{A}^{\simbot}\end{array}$

  * •

we define, for every measurable set the _empty_ behavior of carrier $V$ as the
empty set $\mathbf{0}_{V}$, and the _full behavior_ of carrier $V$ as its
orthogonal $\mathbf{T}_{V}=\\{\mathfrak{a}\leavevmode\nobreak\
|\leavevmode\nobreak\ \mathfrak{a}\text{ of support }V\\}$;

  * •

if $\mathbf{A,B}$ are two behaviors of disjoint carriers, we define:

$\displaystyle\mathbf{A\otimes B}$ $\displaystyle=$
$\displaystyle\\{\mathfrak{a\mathop{\mathopen{:}\mathclose{:}}b}\leavevmode\nobreak\
|\leavevmode\nobreak\
\mathfrak{a}\in\mathbf{A},\mathfrak{b}\in\mathbf{B}\\}^{\simbot\simbot}$
$\displaystyle\mathbf{A\multimap B}$ $\displaystyle=$
$\displaystyle\\{\mathfrak{f}\leavevmode\nobreak\ |\leavevmode\nobreak\
\forall\mathfrak{a}\in\mathbf{A},\mathfrak{f\mathop{\mathopen{:}\mathclose{:}}a}\in\mathbf{B}\\}$
$\displaystyle\mathbf{A\oplus B}$ $\displaystyle=$
$\displaystyle(\\{\mathfrak{a}_{\uparrow V^{A}\cup V^{B}}\leavevmode\nobreak\
|\leavevmode\nobreak\
\mathfrak{a}\in\mathbf{A}\\}^{\simbot\simbot}\cup\\{\mathfrak{b}_{\uparrow
V^{A}\cup V^{B}}\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathfrak{b}\in\mathbf{B}\\}^{\simbot\simbot})^{\simbot\simbot}$
$\displaystyle\mathbf{A\with B}$ $\displaystyle=$
$\displaystyle\\{\mathfrak{a}_{\uparrow V^{A}\cup V^{B}}\leavevmode\nobreak\
|\leavevmode\nobreak\
\mathfrak{a}\in\mathbf{A^{\simbot}}\\}^{\simbot}\cap\\{\mathfrak{b}_{\uparrow
V^{A}\cup V^{B}}\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathfrak{b}\in\mathbf{B}^{\simbot}\\}^{\simbot}$

  * •

two elements $\mathfrak{a,b}$ of a conduct $\mathbf{A}$ are _observationally
equivalent_ when:

$\forall\mathfrak{c}\in\mathbf{A}^{\simbot},\leavevmode\nobreak\
\mathopen{\ll}\mathfrak{a},\mathfrak{c}\mathclose{\gg}_{m}=\mathopen{\ll}\mathfrak{b},\mathfrak{c}\mathclose{\gg}_{m}$

One important point in this work is the fact that all results rely on a single
geometric property, namely the previously introduced _trefoil property_ which
describes how the sets of $1$-circuits evolve during an execution. This
property insures on its own the four following facts:

  * •

we obtain a $\ast$-autonomous category $\mathfrak{Graph}_{MLL}{}$ whose
objects are conducts and morphisms are projects;

  * •

the observational equivalence is a congruence on this category;

  * •

the quotiented category $\mathfrak{Cond}{\leavevmode\nobreak\ }$ inherits the
$\ast$-autonomous structure;

  * •

the quotiented category $\mathfrak{Cond}{\leavevmode\nobreak\ }$ has a full
subcategory $\mathfrak{Behav}{\leavevmode\nobreak\ }$ with products whose
objects are behaviors.

This can be summarized in the following two theorems.

######  Theorem .

For any map $m:\Omega\rightarrow\mathbf{R}\cup\\{\infty\\}$, the categories
$\mathfrak{Cond}{\leavevmode\nobreak\ }$and $\mathfrak{Graph}_{MLL}{}$ are
non-degenerate categorical models of Multiplicative Linear Logic with
multiplicative units.

######  Theorem .

For any map $m:\Omega\rightarrow\mathbf{R}\cup\\{\infty\\}$, the full
subcategory $\mathfrak{Behav}{\leavevmode\nobreak\ }$ of
$\mathfrak{Cond}{\leavevmode\nobreak\ }$ is a non-degenerate categorical model
of Multiplicative-Additive Linear Logic with additive units.

The categorical model we obtain has two layers (see Figure 3). The first layer
consists in a non-degenerate (i.e. $\otimes\neq\parr$ and
$\mathbf{1}\neq\mathbf{\bot}$) $\ast$-autonomous category
$\mathfrak{Cond}{\leavevmode\nobreak\ }$, hence a denotational model for MLL
with units. The second layer is the full subcategory
$\mathfrak{Behav}{\leavevmode\nobreak\ }$which does not contain the
multiplicative units but is a non-degenerate model (i.e. $\otimes\neq\parr$,
$\oplus\neq\with$ and $\mathbf{0}\neq\mathbf{\top}$) of MALL with additive
units that does not satisfy the mix and weakening rules.

$\mathfrak{Cond}{\leavevmode\nobreak\ }$
---
($\ast$-autonomous)
$\mathfrak{Behav}{\leavevmode\nobreak\ }$
---
(closed under $\otimes,\multimap,\with,\oplus,(\cdot)^{\simbot}$)
NO weakening, NO mix
$\bullet_{\bot}$$\bullet_{\mathbf{1}}$$\bullet_{\mathbf{T}}$$\bullet_{\mathbf{0}}$
Figure 3: The categorical models

We here recall some technical results obtained in our paper on additives
[Sei14a] and that will be useful in the following.

######  Proposition .

If $A$ is a non-empty set of projects of same carrier $V^{A}$ such that
$(a,A)\in A$ implies $a=0$, then $\mathfrak{b}\in A^{\simbot}$ implies
$\mathfrak{b}+\lambda\mathfrak{0}_{V^{A}}\in A^{\simbot}$ for all
$\lambda\in\mathbb{R}$.

######  Proposition .

If $A$ is a non-empty set of projects of carrier $V$ such that
$\mathfrak{a}\in A\Rightarrow\mathfrak{a+\lambda 0}_{V}\in A$, then any
project in $A^{\simbot}$ is wager-free, i.e. if $(a,A)\in A^{\simbot}$ then
$a=0$.

######  Lemma  (Homothety).

Conducts are closed under homothety: for all $\mathfrak{a}\in\mathbf{A}$ and
all $\lambda\in\mathbf{R}$ with $\lambda\neq 0$,
$\lambda\mathfrak{a}\in\mathbf{A}$.

######  Proposition .

We denote by $\mathbf{A\odot B}$ the set
$\\{\mathfrak{a}\otimes\mathfrak{b}\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathfrak{a}\in\mathbf{A},\mathfrak{b}\in\mathbf{B}\\}$. Let $E,F$ be non-
empty sets of projects of respective carriers $V,W$ with $V\cap W=\emptyset$.
Then

$(E\odot F)^{\simbot\simbot}=(E^{\simbot\simbot}\odot
F^{\simbot\simbot})^{\simbot\simbot}$

######  Proposition .

Let $\mathbf{A,B}$ be conducts. Then:

$(\\{\mathfrak{a}\otimes\mathfrak{0}_{\mathnormal{B}}\leavevmode\nobreak\
|\leavevmode\nobreak\
\mathfrak{a}\in\mathbf{A}\\}\cup\\{\mathfrak{0}_{\mathnormal{A}}\otimes\mathfrak{b}\leavevmode\nobreak\
|\leavevmode\nobreak\
\mathfrak{b}\in\mathbf{B}\\})^{\simbot\simbot}=\mathbf{A\oplus B}$

######  Proposition  (Distributivity).

For any behaviors $\mathbf{A,B,C}$, and delocations $\phi,\psi,\theta,\rho$ of
$\mathbf{A},\mathbf{A},\mathbf{B},\mathbf{C}$ respectively, there is a project
$\mathfrak{distr}$ in the behavior

$\mathbf{((\phi(A)\\!\multimap\\!\theta(B))\\!\with\\!(\psi(A)\\!\multimap\\!\rho(C)))\\!\multimap\\!(A\\!\multimap\\!(B\\!\with\\!C))}$

###  2.3 Graphings

In subsequent work [Sei14c], we introduced a generalization of graphs to which
the previously described results can extended. This generalization allows,
among other things, for the definition of second order quantification. The
main purpose of this generalization is that a vertex can always be cut in an
arbitrary (finite) number of sub-vertices, with the idea that these sub-
vertices are smaller (hence vertices have a _size_) and form a partition of
the initial vertex (where two sub-vertices have the same size). These notions
could be introduced and dealt with combinatorially, but we chose to use
measure-theoretic notions in order to ease the intuitions and some proofs. In
fact, a _graphing_ — the notion which is introduced as a generalization of the
notion of graph — can be though of and used as a graph. Another important
feature of the construction is the fact that it depends on a _microcosm_ — a
monoid of non-singular transformations — which somehow describes that
computational principles allowed in the model.

######  Definition .

Let $(X,\mathcal{B},\lambda)$ be a measured space. We denote by
$\mathcal{M}(X)$ the set of Borel-preserving non-singular transformations777A
non-singular transformation $f:X\rightarrow X$ is a measurable map which
preserves the sets of null measure, i.e. $\lambda(f(A))=0$ if and only if
$\lambda(A)=0$. A Borel-preserving map is a map such that the images of Borel
sets are Borel sets. $X\rightarrow X$. A _microcosm_ of the measured space $X$
is a subset $\mathfrak{m}$ of $\mathcal{M}(X)$ which is closed under
composition and contains the identity.

As in the graph construction described above, we will consider a notion of
graphing depending on a _weight-monoid_ $\Omega$, i.e. a monoid
$(\Omega,\cdot,1)$ which contains the possible weights of the edges.

######  Definition  (Graphings).

Let $\mathfrak{m}$ be a microcosm of a measured space
$(X,\mathcal{B},\lambda)$ and $V^{F}$ a measurable subset of $X$. A _$\Omega$
-weighted graphing in $\mathfrak{m}$_ of carrier $V^{F}$ is a countable family
$F=\\{(\omega_{e}^{F},\phi_{e}^{F}:S_{e}^{F}\rightarrow T_{e}^{F}\\}_{e\in
E^{F}}$, where, for all $e\in E^{F}$ (the set of _edges_):

  * •

$\omega_{e}^{F}$ is an element of $\Omega$, the _weight_ of the edge $e$;

  * •

$S_{e}^{F}\subset V^{F}$ is a measurable set, the _source_ of the edge $e$;

  * •

$T_{e}^{F}=\phi_{e}^{F}(S_{e}^{F})\subset V^{F}$ is a measurable set, the
_target_ of the edge $e$;

  * •

$\phi_{e}^{F}$ is the restriction of an element of $\mathfrak{m}$ to
$S_{e}^{F}$, the _realization_ of the edge $e$.

It is natural, as we are working with measure-theoretic notions, to identify
two graphings that differ only on a set of null measure. This leads to the
definition of an equivalence relation between graphings: that of _almost
everywhere equality_. Moreover, since we want vertices to be _decomposable_
into any finite number of parts, we want to identify a graphing $G$ with the
graphing $G^{\prime}$ obtained by replacing an edge $e\in E^{F}$ by a finite
family of edges $e_{i}\in G^{\prime}$ ($i=1,\dots,n$) subject to the
conditions:

  * •

the family $\\{S^{G^{\prime}}_{e_{i}}\\}_{i=1}^{n}$ (resp.
$\\{T^{G^{\prime}}_{e_{i}}\\}_{i=1}^{n}$) is a partition of $S_{e}^{G}$ (resp.
$T_{e}^{G}$);

  * •

for all $i=1,\dots,n$, $\phi_{e_{i}}^{G^{\prime}}$ is the restriction of
$\phi_{e}^{G}$ on $S^{G^{\prime}}_{e_{i}}$.

Such a graphing $G^{\prime}$ is an example of a _refinement of $G$_, and one
can easily generalize the previous conditions to define a general notion of
refinement of graphings. Figure 4 gives the most simple example of refinement.
To be a bit more precise, we define, in order to ease the proofs, a notion of
refinement _up to almost everywhere equality_. We then define a second
equivalence relation on graphings by saying that two graphings are equivalent
if and only if they have a common refinement (up to almost everywhere
equality).

$[0,2]$$[3,5]$$x\mapsto 5-x$$[0,1]$$[1,2]$$[3,4]$$[4,5]$$x\mapsto
5-x$$x\mapsto 5-x$ Figure 4: A graphing and one of its refinements

The objects under study are thus equivalence classes of graphings modulo this
equivalence relation. Most of the technical results on graphings contained in
our previous paper [Sei14c] aim at showing that these objects can actually be
manipulated as graphs: one can define paths and cycles and these notions are
coherent with the quotient by the equivalence relation just mentioned. Indeed,
the notions of paths and cycles in a graphings are quite natural, and from two
graphings $F,G$ in a microcosm $\mathfrak{m}$ one can define its execution
$F\mathop{\mathopen{:}\mathclose{:}}G$ which is again a graphing in
$\mathfrak{m}$888As a consequence, a microcosm is a closed world for the
execution of programs.. A more involved argument then shows that the trefoil
property holds for a family of measurements
$\mathopen{\llbracket}\cdot,\cdot\mathclose{\rrbracket}_{m}$, where
$m:\Omega\rightarrow\mathbf{R}_{\geqslant 0}\cup\\{\infty\\}$ is any
measurable map. These results are obtained as a generalization of
constructions considered in the author’s thesis999In the cited work, the
results were stated in the particular case of the microcosm of measure-
preserving maps on the real line..

######  Theorem .

Let $\Omega$ be a monoid, $\mathfrak{m}$ a microcosm and
$m:\Omega\rightarrow\mathbf{R}_{\geqslant 0}\cup\\{\infty\\}$ be a measurable
map. The set of $\Omega$-weighted graphings in $\mathfrak{m}$ yields a model,
denoted by $\mathbb{M}[\Omega,\mathfrak{m}]_{m}$, of multiplicative-additive
linear logic whose orthogonality relation depends on $m$.

##  3 Thick Graphs and Contraction

In this section, we will define the notion of _thick graphs_ , and extend the
addictive construction defined in our earlier paper [Sei14a] to that setting.
The introduction of these objects will be motivated in Section 3.3, where we
will explain how thick graphs allows for the interpretation of the contraction
rule. This contraction rule being satisfied only for a certain kind of
conducts — interpretations of formulas, this will justify the definition of
the exponentials.

###  3.1 Thick Graphs

######  Definition .

Let $S^{G}$ and $D^{G}$ be finite sets. A directed weighted _thick graph_ $G$
of carrier $S^{G}$ and _dialect_ $D^{G}$ is a directed weighted graph over the
set of vertices $S^{G}\times D^{G}$.

We will call _slices_ the set of vertices $S^{G}\times\\{d\\}$ for $d\in
D^{G}$.

Figure 5 shows two examples of thick graphs. Thick graphs will be represented
following a graphical convention very close to the one we used for sliced
graphs:

  * •

Graphs are once again represented with colored edges and delimited by hashed
lines;

  * •

Elements of the carrier $S^{G}$ are represented on a horizontal scale, while
elements of the dialect $D^{G}$ are represented on a vertical scale;

  * •

Inside a given graph, slices are separated by a _dotted_ line.

$1_{1}$$2_{1}$$1_{2}$$2_{2}$$2_{1}$$3_{1}$$2_{2}$$3_{2}$slice $2$slice
$1$Gslice $2$slice $1$H Figure 5: Two thick graphs $G$ and $H$, both with
dialect $\\{1,2\\}$

######  Remark .

If $G=\sum_{i\in I^{G}}\alpha^{G}_{i}G_{i}$ is a sliced graph such that
$\forall i\in I^{G},\alpha^{G}_{i}=1$, then $G$ can be identified with a thick
graph of dialect $I^{G}$. Indeed, one can define the thick graph $\\{G\\}$ by:

$\displaystyle V^{\\{G\\}}$ $\displaystyle=$ $\displaystyle V^{G}\times I^{G}$
$\displaystyle E^{\\{G\\}}$ $\displaystyle=$ $\displaystyle\uplus_{i\in
I^{G}}E^{G_{i}}$ $\displaystyle s^{\\{G\\}}$ $\displaystyle=$ $\displaystyle
e\in E^{G_{i}}\mapsto(s^{G_{i}}(e),i)$ $\displaystyle t^{\\{G\\}}$
$\displaystyle=$ $\displaystyle e\in E^{G_{i}}\mapsto(t^{G_{i}}(e),i)$
$\displaystyle\omega^{\\{G\\}}$ $\displaystyle=$ $\displaystyle e\in
E^{G_{i}}\mapsto\omega^{G_{i}}(e)$

######  Definition  (Variants).

Let $G$ be a thick graph and $\phi:D^{G}\rightarrow E$ a bijection. One
defines $G^{\phi}$ as the graph:

$\displaystyle V^{G^{\phi}}$ $\displaystyle=$ $\displaystyle S^{G}\times E$
$\displaystyle E^{G^{\phi}}$ $\displaystyle=$ $\displaystyle E^{G}$
$\displaystyle s^{G^{\phi}}$ $\displaystyle=$
$\displaystyle(Id_{V^{G}}\times\phi)\circ s^{G}$ $\displaystyle t^{G^{\phi}}$
$\displaystyle=$ $\displaystyle(Id_{V^{G}}\times\phi)\circ t^{G}$
$\displaystyle\omega^{G^{\phi}}$ $\displaystyle=$ $\displaystyle\omega^{G}$

If $G$ and $H$ are two thick graphs such that $H=G^{\phi}$ for a bijection
$\phi$, then $H$ is called a _variant_ of $G$. The relation defined by $G\sim
H$ if and only if $G$ is a variant of $H$ can easily be checked to be an
equivalence relation.

######  Definition  (Dialectal Interaction).

Let $G$ and $H$ be thick graphs.

  1. 1.

We denote by $G^{\dagger_{D^{H}}}$ the thick graph of dialect $D^{G}\times
D^{H}$ defined as $\\{\sum_{i\in D^{H}}G\\}$;

  2. 2.

We denote by $H^{\ddagger_{D^{G}}}$ the thick graph of dialect $D^{G}\times
D^{H}$ defined as $\\{\sum_{i\in D^{G}}H\\}^{\tau}$ where $\tau$ is the
natural bijection $D^{H}\times D^{G}\rightarrow D^{G}\times
D^{H},(a,b)\mapsto(b,a)$.

$1_{1,1}$$2_{1,1}$$1_{2,1}$$2_{2,1}$$1_{1,2}$$2_{1,2}$$1_{2,2}$$2_{2,2}$slices
$(\cdot,1)$slices
$(\cdot,2)$$2_{1,1}$$3_{1,1}$$2_{1,2}$$3_{1,2}$$2_{2,1}$$3_{2,1}$$2_{2,2}$$3_{2,2}$slices
$(1,\cdot)$slices $(2,\cdot)$ Figure 6: The graphs $G^{\dagger_{D^{H}}}$ and
$H^{\ddagger_{D^{G}}}$

We can then define the plugging $F\square G$ of two thick graphs as the
plugging of the graphs $F^{\dagger_{D^{G}}}$ and $G^{\ddagger_{D^{F}}}$.
Figure 7 shows the result of the plugging of $G$ and $H$, the thick graphs
represented in Figure 5.

$1_{1,1}$$2_{1,1}$$1_{2,1}$$2_{2,1}$$1_{1,2}$$2_{1,2}$$1_{2,2}$$2_{2,2}$$3_{1,1}$$3_{1,2}$$3_{2,1}$$3_{2,2}$
Figure 7: Plugging of the thick graphs $G$ and $H$

One can then define the execution $G\mathop{\mathopen{:}\cdot\mathclose{:}}H$
of two thick graphs $G$ and $H$ as the execution of the graphs
$G^{\dagger_{D^{H}}}$ and $H^{\ddagger_{D^{G}}}$. Figure 8 shows the set of
alternating paths in the plugging of the thick graphs $G$ and $H$ introduced
in Figure 5. Figure 9 and Figure 10 represent the result of the execution of
these two thick graphs, the first is three-dimensional representation which
can help make the connection with the set of alternating paths in Figure 8,
while the second is a two-dimensional representation of the same graph. In a
natural way, the measurement of the interaction between two thick graphs $G,H$
is defined as
$\mathopen{\llbracket}G^{\dagger_{D^{H}}},H^{\ddagger_{D^{G}}}\mathclose{\rrbracket}_{m}$.

######  Definition .

The execution $F\mathop{\mathopen{:}\cdot\mathclose{:}}G$ of two thick graphs
$F,G$ is the thick graph of carrier $S^{F}\Delta S^{G}$ and dialect
$D^{F}\times D^{G}$ defined as
$F^{\dagger_{D^{G}}}\mathop{\mathopen{:}\mathclose{:}}G^{\ddagger_{D^{F}}}$.

$1_{1,1}$$1_{2,1}$$1_{1,2}$$1_{2,2}$$3_{1,1}$$3_{1,2}$$3_{2,1}$$3_{2,2}$
Figure 8: Alternating paths in the plugging of thick graphs $G$ and $H$
$1_{1,1}$$1_{2,1}$$1_{1,2}$$1_{2,2}$$3_{1,1}$$3_{1,2}$$3_{2,1}$$3_{2,2}$slice
$(1,1)$slice $(2,1)$slice $(1,2)$slice $(2,2)$ Figure 9: Result of the
execution of the thick graphs $G$ and $H$
$1_{1,1}$$1_{2,1}$$1_{1,2}$$1_{2,2}$$3_{1,1}$$3_{1,2}$$3_{2,1}$$3_{2,2}$slice
$(2,1)$slice $(1,1)$slice $(2,2)$slice
$(1,2)$$G\mathop{\mathopen{:}\cdot\mathclose{:}}H$ Figure 10: The thick graph
$G\mathop{\mathopen{:}\cdot\mathclose{:}}H$ represented in two dimensions.

######  Remark .

Since we only modified the graphs before plugging them together, we can make
the following remark. Let $F,G,H$ be thick graphs. Then the thick graph
$F\mathop{\mathopen{:}\cdot\mathclose{:}}(G\mathop{\mathopen{:}\cdot\mathclose{:}}H)$
is defined as

$F^{\dagger_{D^{G}\times
D^{H}}}\mathop{\mathopen{:}\mathclose{:}}(G^{\dagger_{D^{H}}}\mathop{\mathopen{:}\mathclose{:}}H^{\ddagger_{D^{G}}})^{\ddagger_{D^{F}}}=F^{\dagger_{D^{G}\times
D^{H}}}\mathop{\mathopen{:}\mathclose{:}}((G^{\dagger_{D^{H}}})^{\ddagger_{D^{F}}}\mathop{\mathopen{:}\mathclose{:}}H^{\ddagger_{D^{F}\times
D^{G}}})$

If one supposes that $S^{F}\cap S^{G}\cap S^{H}=\emptyset$, it is clear that
$(S^{F}\times D)\cap(S^{G}\times D)\cap(S^{H}\times D)=\emptyset$. We can
deduce from the associativity of execution that

$F^{\dagger_{D^{G}\times
D^{H}}}\mathop{\mathopen{:}\mathclose{:}}((G^{\dagger_{D^{H}}})^{\ddagger_{D^{F}}}\mathop{\mathopen{:}\mathclose{:}}H^{\ddagger_{D^{F}\times
D^{G}}})=(F^{\dagger_{D^{G}\times
D^{H}}}\mathop{\mathopen{:}\mathclose{:}}((G^{\dagger_{D^{H}}})^{\ddagger_{D^{F}}}))\mathop{\mathopen{:}\mathclose{:}}H^{\ddagger_{D^{F}\times
D^{G}}}$

But:

$(F^{\dagger_{D^{G}\times
D^{H}}}\mathop{\mathopen{:}\mathclose{:}}((G^{\dagger_{D^{H}}})^{\ddagger_{D^{F}}})\mathop{\mathopen{:}\mathclose{:}}H^{\ddagger_{D^{F}\times
D^{G}}}=((F^{\dagger_{D^{G}}}\mathop{\mathopen{:}\mathclose{:}}G^{\ddagger_{D^{F}}})^{\dagger_{D^{H}}})\mathop{\mathopen{:}\mathclose{:}}H^{\ddagger_{D^{F}\times
D^{G}}}$

The latter is by definition the thick graph
$(F\mathop{\mathopen{:}\cdot\mathclose{:}}G)\mathop{\mathopen{:}\cdot\mathclose{:}}H$.
This shows that the associativity of $\mathop{\mathopen{:}\cdot\mathclose{:}}$
on thick graphs is a simple consequence of the associativity of
$\mathop{\mathopen{:}\mathclose{:}}$ on simple graphs.

######  Proposition  (Associativity).

Let $F,G,H$ be thick graphs such that $S^{F}\cap S^{G}\cap S^{H}=\emptyset$.
Then:

$F\mathop{\mathopen{:}\cdot\mathclose{:}}(G\mathop{\mathopen{:}\cdot\mathclose{:}}H)=(F\mathop{\mathopen{:}\cdot\mathclose{:}}G)\mathop{\mathopen{:}\cdot\mathclose{:}}H$

######  Definition .

Let $F$ and $G$ be two thick graphs. We define $\text{{Cy}}^{e}(F,G)$ as the
set of circuits in $F^{\dagger_{D^{G}}}\square G^{\ddagger_{D^{F}}}$.

We also define, being given a dialect $D^{H}$,

  * •

the set $\text{{Cy}}^{e}(F,G)^{\dagger_{D^{H}}}$ of circuits in the graph
$(F^{\dagger_{D^{G}}})^{\dagger_{D^{H}}}\square(G^{\ddagger_{D^{F}}})^{\dagger_{D^{H}}}$

  * •

the set $\text{{Cy}}^{e}(F,G)^{\ddagger_{D^{H}}}$ of circuits in the graph
$(F^{\ddagger_{D^{G}}})^{\dagger_{D^{H}}}\square(G^{\ddagger_{D^{F}}})^{\dagger_{D^{H}}}$

######  Proposition .

Let $F,G,H$ be thick graphs and $\phi:D^{H}\rightarrow D$ a bijection. Then:

$\displaystyle\text{{Cy}}^{e}(F,H)$ $\displaystyle\cong$
$\displaystyle\text{{Cy}}^{e}(F,H^{\phi})$
$\displaystyle\text{{Cy}}^{e}(F,G)^{\dagger_{D^{H}}}$ $\displaystyle\cong$
$\displaystyle\text{{Cy}}^{e}(F,G)^{\dagger_{\phi(D^{H})}}$
$\displaystyle\text{{Cy}}^{e}(F,G)^{\dagger_{D^{H}}}$ $\displaystyle\cong$
$\displaystyle\text{{Cy}}^{e}(F,G)^{\ddagger_{D^{H}}}$

As in Section 3.1, one considers the three thick graphs $F,G,H$. We are
interested in the circuits in
$\text{{Cy}}^{e}(F,G\mathop{\mathopen{:}\cdot\mathclose{:}}H)\cup(\text{{Cy}}^{e}(G,H)^{\ddagger{D^{F}}})$.
By definition, these are the circuits in one of the following graphs:

$F^{\dagger_{D^{G}\times
D^{H}}}\square((G^{\dagger_{D^{H}}}\mathop{\mathopen{:}\mathclose{:}}H^{\ddagger_{D^{G}}})^{\ddagger_{D^{F}}})=F^{\dagger_{D^{G}\times
D^{H}}}\square((G^{\dagger_{D^{H}}})^{\ddagger_{D^{F}}}\mathop{\mathopen{:}\mathclose{:}}H^{\ddagger_{D^{F}\times
D^{G}}})$ $(G^{\dagger_{D^{H}}}\square
H^{\ddagger_{D^{G}}})^{\ddagger{D^{F}}}=(G^{\dagger_{D^{H}}})^{\ddagger_{D^{F}}}\square
H^{\ddagger_{D^{F}\times D^{G}}}$

We can now use the trefoil property to deduce that these sets of circuits are
in bijection with the set of circuits in the following graphs:

$(F^{\dagger_{D^{G}\times
D^{H}}}\mathop{\mathopen{:}\mathclose{:}}(G^{\ddagger_{D^{F}}})^{\dagger_{D^{H}}})\square
H^{\ddagger_{D^{F}\times
D^{G}}}=(F^{\dagger_{D^{G}}}\mathop{\mathopen{:}\mathclose{:}}G^{\ddagger_{D^{F}}})^{\dagger_{D^{H}}}\square
H^{\ddagger_{D^{F}\times D^{G}}})$ $(F^{\dagger_{D^{G}\times
D^{H}}}\square(G^{\ddagger_{D^{F}}})^{\dagger_{D^{H}}}=(F^{\dagger_{D^{G}}}\square
G^{\ddagger_{D^{F}}})^{\dagger{D^{H}}}$

This shows that the trefoil property holds for thick graphs.

######  Proposition  (Geometric Trefoil Property for Thick Graphs).

If $F$, $G$, $H$ are thick graphs such that $S^{F}\cap S^{G}\cap
S^{H}=\emptyset$, then:

$\text{{Cy}}^{e}(F,G\mathop{\mathopen{:}\cdot\mathclose{:}}H)\cup\text{{Cy}}^{e}(G,H)^{\dagger_{D^{F}}}\cong\text{{Cy}}^{e}(F\mathop{\mathopen{:}\cdot\mathclose{:}}G,H)\cup\text{{Cy}}^{e}(F,G)^{\dagger_{D^{H}}}$

######  Corollary  (Geometric Adjunction for Thick Graphs).

If $F$, $G$, $H$ are thick graphs such that $S^{G}\cap S^{H}=\emptyset$, we
have:

$\text{{Cy}}^{e}(F,G\cup
H)\cong\text{{Cy}}^{e}(F\mathop{\mathopen{:}\cdot\mathclose{:}}G,H)\cup\text{{Cy}}^{e}(F,G)^{\dagger_{D^{H}}}$

######  Definition .

Being given a circuit quantifying map $m$, one can define a measurement of the
interaction between thick graphs. For every couple of thick graphs $F,G$, it
is defined as:

$\mathopen{\llbracket}F,G\mathclose{\rrbracket}_{m}=\sum_{\pi\in\text{{Cy}}^{e}(F,G)}\frac{1}{\text{Card}(D^{F}\times
D^{G})}m(\omega(\pi))$

######  Proposition  (Numerical Trefoil Property for Thick Graphs).

Let $F,G,H$ be thick graphs such that $S^{F}\cap S^{G}\cap S^{H}=\emptyset$.
Then:

$\mathopen{\llbracket}F,G\mathop{\mathopen{:}\cdot\mathclose{:}}H\mathclose{\rrbracket}_{m}+\mathopen{\llbracket}G,H\mathclose{\rrbracket}_{m}=\mathopen{\llbracket}H,F\mathop{\mathopen{:}\cdot\mathclose{:}}G\mathclose{\rrbracket}_{m}+\mathopen{\llbracket}F,G\mathclose{\rrbracket}_{m}$

###### Proof.

The proof is a simple calculation using the geometric trefoil property for
thick graphs (Section 3.1). We denote by $n^{F}$ (resp. $n^{G}$, $n^{H}$) the
cardinality of the dialect $D^{F}$ (resp. $D^{G}$, $D^{H}$).

$\displaystyle\mathopen{\llbracket}F,G\mathop{\mathopen{:}\cdot\mathclose{:}}H\mathclose{\rrbracket}_{m}+\mathopen{\llbracket}G,H\mathclose{\rrbracket}_{m}$
$\displaystyle=$
$\displaystyle\sum_{\pi\in\text{{Cy}}^{e}(F,G\mathop{\mathopen{:}\cdot\mathclose{:}}H)}\frac{1}{n^{F}n^{G}n^{H}}m(\omega(\pi))+\sum_{\pi\in\text{{Cy}}^{e}(G,H)}\frac{1}{n^{G}n^{H}}m(\omega(\pi))$
$\displaystyle=$
$\displaystyle\sum_{\pi\in\text{{Cy}}^{e}(F,G\mathop{\mathopen{:}\cdot\mathclose{:}}H)}\frac{1}{n^{F}n^{G}n^{H}}m(\omega(\pi))+\sum_{\pi\in\text{{Cy}}^{e}(G,H)^{\dagger_{D^{F}}}}\frac{1}{n^{F}n^{G}n^{H}}m(\omega(\pi))$
$\displaystyle=$
$\displaystyle\sum_{\pi\in\text{{Cy}}^{e}(F,G\mathop{\mathopen{:}\cdot\mathclose{:}}H)\cup\text{{Cy}}^{e}(G,H)^{\dagger_{D^{F}}}}\frac{1}{n^{F}n^{G}n^{H}}m(\omega(\pi))$
$\displaystyle=$
$\displaystyle\sum_{\pi\in\text{{Cy}}^{e}(H,F\mathop{\mathopen{:}\cdot\mathclose{:}}G)\cup\text{{Cy}}^{e}(F,G)^{\dagger_{D^{H}}}}\frac{1}{n^{F}n^{G}n^{H}}m(\omega(\pi))$
$\displaystyle=$
$\displaystyle\sum_{\pi\in\text{{Cy}}^{e}(H,F\mathop{\mathopen{:}\cdot\mathclose{:}}G)}\frac{1}{n^{F}n^{G}n^{H}}m(\omega(\pi))+\sum_{\pi\in\text{{Cy}}^{e}(F,G)^{\dagger_{D^{H}}}}\frac{1}{n^{F}n^{G}n^{H}}m(\omega(\pi))$
$\displaystyle=$
$\displaystyle\sum_{\pi\in\text{{Cy}}^{e}(H,F\mathop{\mathopen{:}\cdot\mathclose{:}}G)}\frac{1}{n^{F}n^{G}n^{H}}m(\omega(\pi))+\sum_{\pi\in\text{{Cy}}^{e}(F,G)}\frac{1}{n^{F}n^{G}}m(\omega(\pi))$
$\displaystyle=$
$\displaystyle\mathopen{\llbracket}H,F\mathop{\mathopen{:}\cdot\mathclose{:}}G\mathclose{\rrbracket}_{m}+\mathopen{\llbracket}F,G\mathclose{\rrbracket}_{m}$

∎

######  Corollary  (Numerical Adjunction for Thick Graphs).

Let $F,G,H$ be thick graphs such that $S^{G}\cap S^{H}=\emptyset$. Then:

$\mathopen{\llbracket}F,G\mathop{\mathopen{:}\cdot\mathclose{:}}H\mathclose{\rrbracket}_{m}=\mathopen{\llbracket}H,F\mathop{\mathopen{:}\cdot\mathclose{:}}G\mathclose{\rrbracket}_{m}+\mathopen{\llbracket}F,G\mathclose{\rrbracket}_{m}$

######  Remark .

About the Hidden Convention of the Numerical Measure
The measurement of interaction we defined hides a convention: each slice of a
thick graph $F$ is considered as having a ”weight” equal to $1/n^{F}$, so that
the total weight of the set of all slices have weight $1$. This convention
corresponds to the choice of working with a _normalized trace_ (such that
$tr(1)=1$) on the idiom in Girard’s hyperfinite geometry of interaction. It
would have been possible to consider another convention which would impose
that each slice have a weight equal to $1$ (this would correspond to working
with the usual trace on matrices in Girard’s hyperfinite geometry of
interaction). In this case, the measurement of the interaction between two
thick graphs $F,G$ is defined as:

$\mathopen{\llparenthesis}F,G\mathclose{\rrparenthesis}=\sum_{\pi\in\text{{Cy}}^{e}(F,G)}m(\omega(\pi))$

The numerical trefoil property is then stated differently: for all thick
graphs $F$, $G$, and $H$ such that $S^{F}\cap S^{G}\cap S^{H}=\emptyset$, we
have:

$\mathopen{\llparenthesis}F,G\mathop{\mathopen{:}\cdot\mathclose{:}}H\mathclose{\rrparenthesis}+n^{F}\mathopen{\llparenthesis}G,H\mathclose{\rrparenthesis}=\mathopen{\llparenthesis}H,F\mathop{\mathopen{:}\cdot\mathclose{:}}G\mathclose{\rrparenthesis}+n^{H}\mathopen{\llparenthesis}F,G\mathclose{\rrparenthesis}$

We stress the apparition of the terms $n^{F}$ and $n^{H}$ in this equality:
their apparition corresponds exactly to the apparition of the terms
$\textbf{1}_{F}$ and $\textbf{1}_{H}$ in the equality stated for the trefoil
property for sliced graphs.

###  3.2 Sliced Thick Graphs

One can of course apply the additive construction presented in our previous
paper [Sei14a] in the case of thick graphs. A _sliced thick graph_ $G$ of
carrier $S^{G}$ s a finite family $\sum_{i\in I^{G}}\alpha^{G}_{i}G_{i}$
where, for all $i\in I^{G}$, $G_{i}$ is a thick graph such that
$S^{G_{i}}=S^{G}$, and $\alpha^{G}_{i}\in\mathbf{R}$. We define the _dialect_
of $G$ to be the set $\uplus_{i\in I^{G}}D^{G_{i}}$. We will abusively call a
_slice_ a couple $(i,d)$ where $i\in I^{G}$ and $d\in D_{G_{i}}$; we will say
a graph $G$ is a _one-sliced graph_ when $I^{G}=\\{i\\}$ and
$D_{G_{i}}=\\{d\\}$ are both one-element sets.

One can extend the execution and the measurement of the interaction by
applying the thick graphs constructions slice by slice:

$\displaystyle(\sum_{i\in
I^{F}}\alpha^{F}_{i}F_{i})\mathop{\mathopen{:}\mathclose{:}}(\sum_{i\in
I^{G}}\alpha^{G}_{i}G_{i})$ $\displaystyle=$
$\displaystyle\\!\\!\\!\\!\sum_{(i,j)\in I^{F}\times
I^{G}}\\!\\!\\!\\!\alpha^{F}_{i}\alpha^{G}_{j}F_{i}\mathop{\mathopen{:}\cdot\mathclose{:}}G_{j}$
$\displaystyle\mathopen{\llbracket}\sum_{i\in
I^{F}}\alpha^{F}_{i}F_{i},\sum_{i\in
I^{G}}\alpha^{G}_{i}G_{i}\mathclose{\rrbracket}_{m}$ $\displaystyle=$
$\displaystyle\\!\\!\\!\\!\sum_{(i,j)\in I^{F}\times
I^{G}}\\!\\!\\!\\!\alpha^{F}_{i}\alpha^{G}_{j}\mathopen{\llbracket}F_{i},G_{j}\mathclose{\rrbracket}_{m}$

Figure 11 shows two examples of sliced thick graphs. The graphical convention
we will follow for representing sliced and thick graphs corresponds to the
graphical convention for sliced graphs, apart from the fact that the graphs
contained in the slices are replaced by thick graphs. Thus, two slices are
separated by a dashed line, two elements in the dialect of a thick graph (i.e.
the graph contained in a slice) are separated by a dotted line.

$1_{1}$$1_{2}$$1_{3}$$2_{1}$$2_{2}$$2_{3}$$3_{1}$$3_{2}$$3_{3}$$\frac{1}{2}F$$3G$$1_{a}$$2_{a}$$1_{b}$$2_{b}$$F_{a}$$F_{b}$
Figure 11: Examples of sliced thick graphs: $\frac{1}{2}F+3G$ and
$F_{a}+F_{b}$

One should however notice that some sliced thick graphs (for instance the
graph $F_{a}+F_{b}$ represented in red in Figure 11) can be considered both as
a thick graph — hence a sliced thick graph with a single slice — or as a
sliced graph with two slices — hence a sliced thick graph with two slices.
Indeed, consider the graphs:

$\begin{array}[]{rcl|rcl|rcl}&F_{a}&&&F_{b}&&&F_{c}\\\ \hline\cr\hline\cr
V^{F_{a}}&=&\\{1,2\\}&V^{F_{b}}&=&\\{1,2\\}&V^{F_{c}}&=&\\{1,2\\}\times\\{a,b\\}\\\
E^{F_{a}}&=&\\{f,g\\}&E^{F_{b}}&=&\\{f,g\\}&E^{F_{c}}&=&\\{f_{a},f_{b},g_{a},g_{b}\\}\\\
s^{F_{a}}&=&\left\\{\begin{array}[]{l}f\mapsto 1\\\ g\mapsto
2\end{array}\right.&s^{F_{b}}&=&\left\\{\begin{array}[]{l}f\mapsto 1\\\
g\mapsto
1\end{array}\right.&s^{F_{c}}&=&\left\\{\begin{array}[]{l}f_{i}\mapsto
s^{F_{i}}(f)\\\ g_{i}\mapsto s^{F_{i}}(g)\end{array}\right.\\\
t^{F_{a}}&=&\left\\{\begin{array}[]{l}f\mapsto 2\\\ g\mapsto
2\end{array}\right.&t^{F_{b}}&=&\left\\{\begin{array}[]{l}f\mapsto 2\\\
g\mapsto
1\end{array}\right.&t^{F_{c}}&=&\left\\{\begin{array}[]{l}f_{i}\mapsto
t^{F_{i}}(f)\\\ g_{i}\mapsto t^{F_{i}}(g)\end{array}\right.\\\
\omega^{F_{a}}&\equiv&1&\omega^{F_{b}}&\equiv&1&\omega^{F_{c}}&\equiv&1\end{array}$

One can then define the the two sliced thick graphs $G_{1}=F_{c}$ and
$G_{2}=\frac{1}{2}F_{a}+\frac{1}{2}F_{b}$. These two graphs are represented in
Figure 12. They are similar in a very precise sense: one can show that if $H$
is any sliced thick graph, and $m$ is any circuit-quantifying map, then
$\mathopen{\llbracket}G_{1},H\mathclose{\rrbracket}_{m}=\mathopen{\llbracket}G_{2},H\mathclose{\rrbracket}_{m}$.
We say they are _universally equivalent_. Notice that this explains in a very
formal way the remark about the convention on the measurement of interaction
Section 3.1.

$1_{a}$$2_{a}$$1_{b}$$2_{b}$$F_{c}$$1_{a}$$2_{a}$$1_{b}$$2_{b}$$\frac{1}{2}F_{a}$$\frac{1}{2}F_{b}$
Figure 12: Les graphes $G_{1}$ et $G_{2}$

######  Definition  (Universally equivalent graphs).

Let $F,G$ be two graphs. We say that $F$ and $G$ are _universally equivalent_
(for the measurement
$\mathopen{\llbracket}\cdot,\cdot\mathclose{\rrbracket}_{m}$) — which will be
denoted by $F\simeq_{u}G$ — if for all graph $H$:

$\mathopen{\llbracket}F,H\mathclose{\rrbracket}_{m}=\mathopen{\llbracket}G,H\mathclose{\rrbracket}_{m}$

The next proposition states that if $F^{\prime}$ is obtained from a graph $F$
by a renaming of edges, then $F\simeq_{u}F^{\prime}$.

######  Proposition .

Let $F,F^{\prime}$ be two graphs such that $V^{F}=V^{F^{\prime}}$, and $\phi$
a bijection $E^{F}\rightarrow E^{F^{\prime}}$ such that:

$\displaystyle s^{G}\circ\phi=s^{F},\leavevmode\nobreak\ \leavevmode\nobreak\
t^{G}\circ\phi=t^{F},\leavevmode\nobreak\ \leavevmode\nobreak\
\omega^{G}\circ\phi=\omega^{F}$

Then $F\simeq_{u}F^{\prime}$.

###### Proof.

Indeed, the bijection $\phi$ induces, from the hypotheses in the source and
target functions, a bijection between the sets of cycles $\text{{Cy}}(F,H)$
and $\text{{Cy}}(G,H)$. The condition on the weight map then insures us that
this bijection is $\omega$-invariant, from which we deduce the proposition. ∎

######  Proposition .

Let $F,G$ be sliced graphs. If there exists a bijection $\phi:I^{F}\rightarrow
I^{G}$ such that $F_{i}=G_{\phi(i)}$ and
$\alpha^{F}_{i}=\alpha^{G}_{\phi(i)}$, then $F\simeq_{u}G$.

###### Proof.

By definition:

$\displaystyle\mathopen{\llbracket}G,H\mathclose{\rrbracket}_{m}$
$\displaystyle=$ $\displaystyle\sum_{(i,j)\in I^{G}\times
I^{H}}\alpha^{G}_{i}\alpha^{H}_{j}\mathopen{\llbracket}G_{i},H_{j}\mathclose{\rrbracket}_{m}$
$\displaystyle=$ $\displaystyle\sum_{(i,j)\in I^{F}\times
I^{H}}\alpha^{G}_{\phi(i)}\alpha^{H}_{j}\mathopen{\llbracket}G_{\phi(i)},H_{j}\mathclose{\rrbracket}_{m}$
$\displaystyle=$ $\displaystyle\sum_{(i,j)\in I^{F}\times
I^{G}}\alpha^{F}_{i}\alpha^{G}_{j}\mathopen{\llbracket}F_{i},G_{j}\mathclose{\rrbracket}_{m}$

Thus $F$ and $G$ are universally equivalent. ∎

######  Proposition .

Let $F,G$ be thick graphs. If there exists a bijection $\phi:D^{F}\rightarrow
D^{G}$ such that $G=F^{\phi}$, then $F\simeq_{u}G$.

###### Proof.

Let $F,G$ be thick graphs such that $G=F^{\phi}$ for a bijection
$\phi:D^{G}\rightarrow D^{F}$, and $H$ an arbitrary thick graph. Then the
bijection $\phi\times\text{Id}:D^{G}\times D^{H}\rightarrow D^{F}\times D^{H}$
satisfies that
$G^{\dagger_{D^{H}}}=(F^{\dagger_{D^{H}}})^{\phi\times\text{Id}}$. One can
notice that the set of alternating circuits in $F^{\dagger}\square
H^{\ddagger}$ is the same as the set of alternating circuits in
$(F^{\dagger})^{\phi\times\text{Id}}\square(H^{\dagger})^{\phi\times\text{Id}}=G^{\dagger}\square
H^{\ddagger}$. Thus:

$\displaystyle\mathopen{\llbracket}F,H\mathclose{\rrbracket}_{m}$
$\displaystyle=$ $\displaystyle\sum_{\pi\in\text{{Cy}}(F,H)}m(\omega(\pi))$
$\displaystyle=$ $\displaystyle\sum_{\pi\in\text{{Cy}}(G,H)}m(\omega(\pi))$
$\displaystyle=$
$\displaystyle\mathopen{\llbracket}G,H\mathclose{\rrbracket}_{m}$

And finally $F$ and $G$ are universally equivalent. ∎

######  Proposition .

Let $F=\sum_{i\in I^{F}}\alpha_{i}^{F}F_{i}$ be a sliced thick graph, and let
us define, for all $i\in I^{F}$, $n^{F_{i}}=\text{Card}(D^{F_{i}})$ and
$n^{F}=\sum_{i\in I^{F}}n^{F_{i}}$. Suppose that there exists a scalar
$\alpha$ such that for all $i\in I^{F}$,
$\alpha_{i}^{F}=\alpha\frac{n^{F_{i}}}{n^{F}}$. We then define the sliced
thick graph with a single slice $\alpha G$ of dialect $\uplus
D^{F_{i}}=\cup_{i\in I^{F}}D^{F_{i}}\times\\{i\\}$ and carrier $V^{F}$ by:

$\displaystyle V^{G}$ $\displaystyle=$ $\displaystyle V^{F}\times\uplus
D^{F_{i}}$ $\displaystyle E^{G}$ $\displaystyle=$ $\displaystyle\uplus
E^{F_{i}}=\cup_{i\in I^{F}}E^{F_{i}}\times\\{i\\}$ $\displaystyle s^{G}$
$\displaystyle=$ $\displaystyle(e,i)\mapsto(s^{F_{i}}(e),i)$ $\displaystyle
t^{G}$ $\displaystyle=$ $\displaystyle(e,i)\mapsto(t^{F_{i}}(e),i)$
$\displaystyle\omega^{G}$ $\displaystyle=$
$\displaystyle(e,i)\mapsto\omega^{F_{i}}(e)$
$\displaystyle\left((e,i)\coh^{G}(f,j)\right.$ $\displaystyle\Leftrightarrow$
$\displaystyle\left.(i\neq j)\vee(i=j\wedge e\coh^{F_{i}}f)\right)$

Then $F$ and $G$ are universally equivalent.

###### Proof.

Let $H$ be a sliced thick graph. Then:

$\displaystyle\mathopen{\llbracket}F,H\mathclose{\rrbracket}_{m}$
$\displaystyle=$ $\displaystyle\sum_{i\in I^{H}}\sum_{j\in
I^{F}}\alpha^{H}_{i}\alpha^{F}_{j}\mathopen{\llbracket}F_{i},H_{j}\mathclose{\rrbracket}_{m}$
$\displaystyle=$ $\displaystyle\sum_{i\in I^{H}}\sum_{j\in
I^{F}}\alpha^{H}_{i}\alpha\frac{n^{F_{i}}}{n^{F}}\mathopen{\llbracket}F_{i},H_{j}\mathclose{\rrbracket}_{m}$
$\displaystyle=$ $\displaystyle\sum_{i\in I^{H}}\sum_{j\in
I^{F}}\alpha^{H}_{i}\alpha\frac{n^{F_{i}}}{n^{F}}\frac{1}{n^{F_{i}}n^{H_{j}}}\sum_{\pi\in\text{{Cy}}(F_{i},H_{j})}m(\omega(\pi))$
$\displaystyle=$ $\displaystyle\sum_{i\in I^{H}}\sum_{j\in
I^{F}}\alpha^{H}_{i}\alpha\frac{1}{n^{F}n^{H_{j}}}\sum_{\pi\in\text{{Cy}}(F_{i},H_{j})}m(\omega(\pi))$
$\displaystyle=$ $\displaystyle\sum_{i\in
I^{H}}\alpha^{H}_{i}\alpha\frac{1}{n^{F}n^{H_{j}}}\sum_{j\in
I^{F}}\sum_{\pi\in\text{{Cy}}(F_{i},H_{j})}m(\omega(\pi))$

But one can notice that $\cup_{j\in
I^{F}}\text{{Cy}}(F_{i},H_{j})=\text{{Cy}}(G,H)$. We thus get:

$\displaystyle\mathopen{\llbracket}F,H\mathclose{\rrbracket}_{m}$
$\displaystyle=$ $\displaystyle\sum_{i\in
I^{H}}\alpha^{H}_{i}\alpha\frac{1}{n^{F}n^{H_{j}}}\sum_{j\in
I^{F}}\sum_{\pi\in\text{{Cy}}(F_{i},H_{j})}m(\omega(\pi))$ $\displaystyle=$
$\displaystyle\sum_{i\in
I^{H}}\alpha^{H}_{i}\alpha\frac{1}{n^{F}n^{H_{j}}}\sum_{\pi\in\text{{Cy}}(F,H_{j})}m(\omega(\pi))$
$\displaystyle=$ $\displaystyle\mathopen{\llbracket}\alpha
G,H\mathclose{\rrbracket}_{m}$

Finally, we showed that $F$ and $\alpha G$ are universally equivalent. ∎

One of the consequences of Section 3.2, Section 3.2, and Section 3.2 is that
two graphs $F,G$ such that $G$ is obtained from $F$ by a renaming of the sets
$E^{F},I^{F},D^{F}$ are universally equivalent. We will therefore work from
now on with graphs modulo renaming of these sets.

###  3.3 Thick Graphs and Contraction

In this section, we will explain how the introduction of thick graphs allow
the definition of contraction by using the fact that edges can go from a slice
to another (contrarily to sliced graphs). In the following, we will be working
with sliced thick graphs. The way contraction is dealt with by using slice-
changing edges is quite simple, and the graph which will implement this
transformation is essentially the same as the graph implementing additive
contraction (i.e. the graph implementing distributivity — Section 2.2 —
restricted to the location of contexts) modified with a change of slices.

The graph we obtain is then the superimposition of two $\mathfrak{Fax}$, but
where one of them goes from one slice to the other.

$1_{1}$$2_{1}$$3_{1}$$4_{1}$$5_{1}$$6_{1}$$7_{1}$$8_{1}$$9_{1}$$1_{2}$$2_{2}$$3_{2}$$4_{2}$$5_{2}$$6_{2}$$4_{2}$$5_{2}$$6_{2}$
Figure 13: The graph of a contraction project

######  Definition  (Contraction).

Let $\phi:V^{A}\rightarrow W_{1}$ and $\psi:V^{A}\rightarrow W_{2}$ be two
bijections with $V^{A}\cap W_{1}=V^{A}\cap W_{2}=W_{1}\cap W_{2}=\emptyset$.
We define the project
$\mathfrak{Ctr}^{\phi}_{\psi}=(0,\text{{Ctr}}^{\phi}_{\psi})$, where the graph
$\text{{Ctr}}^{\phi}_{\psi}$ is defined by:

$\displaystyle V^{\text{{Ctr}}^{\phi}_{\psi}}$ $\displaystyle=$ $\displaystyle
V^{A}\cup W_{1}\cup W_{2}$ $\displaystyle D^{\text{{Ctr}}^{\phi}_{\psi}}$
$\displaystyle=$ $\displaystyle\\{1,2\\}$ $\displaystyle
E^{\text{{Ctr}}^{\phi}_{\psi}}$ $\displaystyle=$ $\displaystyle
V^{A}\times\\{1,2\\}\times\\{i,o\\}$ $\displaystyle
s^{\text{{Ctr}}^{\phi}_{\psi}}$ $\displaystyle=$
$\displaystyle\left\\{\begin{array}[]{rcl}(v,1,o)&\mapsto&(\phi(v),1)\\\
(v,1,i)&\mapsto&(v,1)\\\ (v,2,o)&\mapsto&(\psi(v),1)\\\
(v,2,i)&\mapsto&(v,2)\end{array}\right.$ $\displaystyle
t^{\text{{Ctr}}^{\phi}_{\psi}}$ $\displaystyle=$
$\displaystyle\left\\{\begin{array}[]{rcl}(v,1,o)&\mapsto&(v,1)\\\
(v,1,i)&\mapsto&(\phi(v),1)\\\ (v,2,o)&\mapsto&(v,2)\\\
(v,2,i)&\mapsto&(\psi(v),1)\end{array}\right.$
$\displaystyle\omega^{\text{{Ctr}}^{\phi}_{\psi}}$ $\displaystyle\equiv$
$\displaystyle 1$

Figure 13 illustrates the graph of the project $\mathfrak{Ctr}^{\psi}_{\phi}$,
where the functions are defined by
$\phi:\\{1,2,3\\}\rightarrow\\{4,5,6\\},x\mapsto x+3$ and
$\psi:\\{1,2,3\\}\rightarrow\\{7,8,9\\},x\mapsto 10-x$.

######  Proposition .

Let $\mathfrak{a}=(0,A)$ be a project in a behavior $\mathbf{A}$, such that
$D^{A}\cong\\{1\\}$. Let $\phi,\psi$ be two delocations $V^{A}\rightarrow
W_{1}$, $V^{A}\rightarrow W_{2}$ of disjoint codomains. Then
$\mathfrak{Ctr}^{\psi}_{\phi}\mathop{\mathopen{:}\mathclose{:}}\mathfrak{a}\in\mathbf{\phi(A)\otimes\psi(A)}$.

###### Proof.

We will denote by Ctr the graph $\text{Ctr}_{\phi}^{\psi}$ to simplify the
notations. We first compute
$A\mathop{\mathopen{:}\cdot\mathclose{:}}\text{Ctr}$. We get
$A^{\ddagger_{\\{1,2\\}}}=(V^{A}\times\\{1,2\\},E^{A}\times\\{1,2\\},s^{A}\times
Id_{\\{1,2\\}},t^{A}\times Id_{\\{1,2\\}},\omega^{A}\circ\pi)$ where $\pi$ is
the projection: $E^{A}\times\\{1,2\\}\rightarrow E^{A},(x,i)\mapsto x$.
Moreover the graph $\text{Ctr}^{\dagger_{D^{A}}}$ is a variant of the graph
Ctr since $D^{A}\cong\\{1\\}$. Here is what the plugging of
$\text{Ctr}^{\dagger_{D^{A}}}$ with $A^{\ddagger_{\\{1,2\\}}}$ looks like:

$V^{A}\times\\{2\\}$$W_{1}\times\\{2\\}$$W_{2}\times\\{2\\}$$V^{A}\times\\{1\\}$$W_{1}\times\\{1\\}$$w_{2}\times\\{1\\}$$\phi$$\psi$

The result of the execution is therefore a two-sliced graph, i.e. a graph of
dialect $D^{A}\times\\{1,2\\}\cong\\{1,2\\}$, and which contains the graph
$\phi(A)\cup\psi(A)$ in the slice numbered $1$ and contains the empty graph in
the slice numbered $2$.

We deduce from this that
$\mathfrak{Ctr}^{\psi}_{\phi}\mathop{\mathopen{:}\mathclose{:}}\mathfrak{a}$
is universally equivalent (Section 3.2) to the project
$\frac{1}{2}\mathfrak{\phi(a)\otimes\psi(a)}+\frac{1}{2}\mathfrak{0}$ from
Section 3.2. Since
$\mathfrak{\phi(a)\otimes\psi(a)}\in\mathbf{\phi(A)\otimes\psi(A)}$, then the
project $\frac{1}{2}(\mathfrak{\phi(a)\otimes\psi(a)})$ is an element in
$\mathbf{\phi(A)\otimes\psi(A)}$ by the homothety Lemma (Section 2.2).
Moreover, $\mathbf{A}$ is a behavior, hence $\mathbf{\phi(A)\otimes\psi(A)}$
is also a behavior and we can deduce that
$\frac{1}{2}\mathfrak{\phi(a)\otimes\psi(a)}+\frac{1}{2}\mathfrak{0}$ is an
element in $\mathbf{\phi(A)\otimes\psi(A)}$. ∎

Figure 15, Figure 16 and Figure 17 illustrate the plugging and execution of a
contraction with two graphs: the first — $A$ — having a single slice, and the
other — $B$ — having two slices (the graphs are shown in Figure 14). One can
see that the hypothesis $D^{A}\equiv\\{1\\}$ used in the preceding proposition
is necessary, and that slice-changing edges allow to implement contraction of
graphs with a single slice.

$1_{1}$$2_{1}$$3_{1}$$4_{1}$$5_{1}$$6_{1}$$1_{2}$$2_{2}$$3_{2}$$4_{2}$$5_{2}$$6_{2}$
(a) The graph of the project $\mathfrak{Ctr}^{\phi}_{\psi}$

$1$$2$$A$$1_{1}$$1_{2}$$2_{1}$$2_{2}$$B$ (b) The graphs $A$ and $B$ of the
projects $\mathfrak{a}$ and $\mathfrak{b}$

Figure 14: The graphs of the projects $\mathfrak{Ctr}^{\phi}_{\psi}$,
$\mathfrak{a}$ and $\mathfrak{b}$.

$1_{1}$$2_{1}$$3_{1}$$4_{1}$$5_{1}$$6_{1}$$1_{2}$$2_{2}$$3_{2}$$4_{2}$$5_{2}$$6_{2}$$A$$A$
(a) Plugging of $\text{{Ctr}}^{\phi}_{\psi}$ and $A$

$1_{1,1}$$2_{1,1}$$3_{1,1}$$4_{1,1}$$5_{1,1}$$6_{1,1}$$1_{2,1}$$2_{2,1}$$3_{2,1}$$4_{2,1}$$5_{2,1}$$6_{2,1}$$1_{1,2}$$2_{1,2}$$3_{1,2}$$4_{1,2}$$5_{1,2}$$6_{1,2}$$1_{2,2}$$2_{2,2}$$3_{2,2}$$4_{2,2}$$5_{2,2}$$6_{2,2}$
(b) Plugging of $\text{{Ctr}}^{\phi}_{\psi}$ and $B$

Figure 15: Plugging of $\text{{Ctr}}^{\phi}_{\psi}$ with the two graphs $A$
and $B$

$3_{1}$$4_{1}$$5_{1}$$6_{1}$$3_{2}$$4_{2}$$5_{2}$$6_{2}$ (a) Result of the
execution of $\text{{Ctr}}^{\phi}_{\psi}$ and $A$

$3_{1}$$4_{1}$$5_{1}$$6_{1}$ (b) The graph of
$\mathfrak{\phi(a)\otimes\psi(a)}$

Figure 16: Graphs of the projects
$\mathfrak{Ctr}^{\phi}_{\psi}\mathop{\mathopen{:}\mathclose{:}}\mathfrak{a}$
and $\mathfrak{\phi(a)\otimes\psi(a)}$

$3_{1}$$4_{1}$$5_{1}$$6_{1}$$3_{2}$$4_{2}$$5_{2}$$6_{2}$$3_{3}$$4_{3}$$5_{3}$$6_{3}$$3_{4}$$4_{4}$$5_{4}$$6_{4}$
(a) Result of the execution of $\text{{Ctr}}^{\phi}_{\psi}$ and $B$

$3_{1}$$4_{1}$$5_{1}$$6_{1}$$3_{2}$$4_{2}$$5_{2}$$6_{2}$$3_{3}$$4_{3}$$5_{3}$$6_{3}$$3_{4}$$4_{4}$$5_{4}$$6_{4}$
(b) Graph of the project $\mathfrak{\phi(b)\otimes\psi(b)}$

Figure 17: Graphs of the projects
$\mathfrak{Ctr}^{\phi}_{\psi}\mathop{\mathopen{:}\mathclose{:}}\mathfrak{b}$
and $\mathfrak{\phi(b)\otimes\psi(b)}$

We will use the following direct corollary of Section 2.2.

######  Proposition .

If $E$ is a non-empty set of project sharing the same carrier $V^{E}$,
$\mathbf{F}$ is a conduct and $\mathfrak{f}$ satisfies that
$\forall\mathfrak{e}\in E$,
$\mathfrak{f\mathop{\mathopen{:}\mathclose{:}}e}\in\mathbf{F}$, then
$\mathfrak{f}\in E^{\simbot\simbot}\multimap\mathbf{F}$.

This proposition insures us that if $\mathbf{A}$ is a conduct such that there
exists a set $E$ of one-sliced projects with $\mathbf{A}=E^{\simbot\simbot}$,
then the contraction project $\mathfrak{Ctr}^{\psi}_{\phi}$ belongs to the
conduct $\mathbf{A\multimap\phi(A)\otimes\psi(A)}$.

We find here a geometrical explanation to the introduction of exponential
connectives. Indeed, in order to use a contraction, we must be sure we are
working with one-sliced graphs. We will therefore define, for all behavior
$\mathbf{A}$, a conduct $\mathbf{\oc A}$ generated by a set of one-sliced
graphs.

One should notice that a conduct $\mathbf{\oc A}$ generated by a set of one-
sliced projects cannot be a behavior: the projects $(a,\emptyset)$ necessarily
belong to the orthogonal of $\mathbf{\oc A}$. We will therefore introduce
_perennial conducts_ as those conducts generated by a set of wager-free one-
sliced projects. Dually, we introduce the _co-perennial conducts_ as the
conducts that are the orthogonal of a perennial conduct.

But first, we will need a way to associate a wager-free one-sliced project to
any wager-free project. In order to do so, we will introduce the notion of
_thick graphing_.

##  4 Construction of an Exponential Connective on the Real Line

We now consider the microcosm $\mathfrak{mi}$ of measure-inflating maps101010A
_measure-inflating map_ on the real line with Lebesgue measure $\lambda$ is a
non-singular Borel-preserving transformation
$\phi:\mathbf{R}\rightarrow\mathbf{R}$ such that there exists a positive real
number $\mu_{\phi}$ with $\lambda(\phi^{-1}(A))=\mu_{\phi}\lambda(A)$. In
other terms, $\phi$ _transports the measure_ $\lambda$ onto
$\mu_{\phi}\lambda$. on the real line endowed with Lebesgue measure, we fix
$\Omega=]0,1]$ endowed with the usual multiplication and we chose any
measurable map $m:\Omega\rightarrow\mathbf{R}_{\geqslant 0}\cup\\{\infty\\}$
such that $m(1)=\infty$. We showed in a previous work how this framework can
interpret multiplicative-additive linear logic with second order
quantification111111We actually showed how one can interpret second-order
multiplicative-additive linear logic in the model
$\mathbb{M}[\Omega,\mathfrak{aff}]_{m}$ where
$\mathfrak{aff}\subsetneq\mathfrak{mi}$ is the microcosm of affine
transformations on the real line. The result is however valid for any super-
microcosm $\mathfrak{n}\supset\mathfrak{aff}$, hence for $\mathfrak{mi}$,
since a graphing in $\mathfrak{aff}$ can be considered as a graphing in
$\mathfrak{n}$ in a way that is coherent with execution, orthogonality, sums,
etc. [Sei14c]. We now show how to interpret elementary linear logic
exponential connectives in the model $\mathbb{M}[\Omega,\mathfrak{mi}]_{m}$
(defined in Section 2.3).

###  4.1 Sliced Thick Graphings

The sliced graphings are obtained from graphings in the same way we defined
sliced thick graphs from directed weighted graphs: we consider formal weighted
sums $F=\sum_{i\in I^{F}}\alpha^{F}_{i}F_{i}$ where the $F_{i}$ are graphings
of carrier $V^{F_{i}}$. We define the _carrier of $F$_ as the measurable set
$\cup_{i\in I^{F}}V^{F_{i}}$. The various constructions are then extended as
explained above:

$\displaystyle(\sum_{i\in
I^{F}}\alpha^{F}_{i}F_{i})\mathop{\mathopen{:}\mathclose{:}}(\sum_{i\in
I^{G}}\alpha^{G}_{i}G_{i})$ $\displaystyle=$ $\displaystyle\sum_{(i,j)\in
I^{F}\times
I^{G}}\alpha_{i}^{F}\alpha^{G}_{j}F_{i}\mathop{\mathopen{:}\mathclose{:}}G_{j}$
$\displaystyle\mathopen{\llbracket}\sum_{i\in
I^{F}}\alpha^{F}_{i}F_{i},\sum_{i\in
I^{G}}\alpha^{G}_{i}G_{i}\mathclose{\rrbracket}_{m}$ $\displaystyle=$
$\displaystyle\sum_{(i,j)\in I^{F}\times
I^{G}}\alpha_{i}^{F}\alpha^{G}_{j}\mathopen{\llbracket}F_{i}\mathop{\mathopen{:}\mathclose{:}}G_{j}\mathclose{\rrbracket}_{m}$

The trefoil property and the adjunction are then easily obtained through the
same computations as in the proofs of Section 3.1 and Section 3.1.

We will now consider the most general notion of _thick graphing_ one can
define. As it was the case in the setting of graphs, a thick graphing is a
graphing whose carrier has the form $V\times D$. The main difference between
graphings and thick graphings really comes from the way two such objects
interact.

######  Definition .

Let $(X,\mathcal{B},\lambda)$ be a measured space and $(D,\mathcal{D},\mu)$ a
probability space (a measured space such that $\mu(D)=1$). A thick graphing of
carrier $V\in\mathcal{B}$ and dialect $D$ is a graphing on $X\times D$ of
carrier $V\times D$.

######  Definition  (Dialectal Interaction).

Let $(X,\mathcal{B},\lambda)$ be a measured space and $(D,\mathcal{D},\mu)$,
$(E,\mathcal{E},\nu)$ two probability spaces. Let $F,G$ be thick graphings of
respective carriers $V^{F},V^{G}\in\mathcal{B}$ and respective dialects $D,E$.
We define the graphings $F^{\dagger_{E}}$ and $G^{\ddagger_{D}}$ as the
graphings of respective carriers $V^{F},V^{G}$ and dialects $E\times F$:

$\displaystyle F^{\dagger_{E}}$ $\displaystyle=$
$\displaystyle\\{(\omega^{F}_{e},\phi^{F}_{e}\times\text{Id}_{E}:S_{e}^{F}\times
D\times E\rightarrow T_{e}^{F}\times D\times E)\\}_{e\in E^{F}}$
$\displaystyle G^{\ddagger_{D}}$ $\displaystyle=$
$\displaystyle\\{(\omega^{G}_{e},\text{Id}_{X}\times(\tau\circ(\phi^{G}_{e}\times\text{Id}_{D})\circ\tau^{-1}):S_{e}^{G}\times
D\times E\rightarrow T_{e}^{G}\times D\times E)\\}_{e\in E^{G}}$

where $\tau$ is the natural symmetry: $E\times D\rightarrow D\times E$.

######  Definition  (Plugging).

The plugging $F\mathop{\mathopen{:}\mathclose{:}}G$ of two thick graphings of
respective dialects $D^{F},D^{G}$ is defined as
$F^{\dagger_{D^{G}}}\tilde{\square}G^{\ddagger_{D^{F}}}$.

######  Definition  (Execution).

Let $F,G$ be two thick graphings of respective dialects $D^{F},D^{G}$. Their
execution is equal to
$F^{\dagger_{D^{G}}}\mathop{\mathopen{:}\text{\scriptsize{m}}\mathclose{:}}{G}^{\ddagger_{D^{F}}}$.

######  Definition  (Measurement).

Let $F,G$ be two thick graphings of respective dialects $D^{F},D^{G}$, and $q$
a circuit-quantifying map. The corresponding measurement of the interaction
between $F$ and $G$ is equal to
$\mathopen{\llbracket}F^{\dagger_{D^{G}}},G^{\ddagger_{D^{F}}}\mathclose{\rrbracket}_{m}$.

As in the setting of graphs, one can show that all the fundamental properties
are preserved when we generalize from graphings to thick graphings.

######  Proposition .

Let $F,G,H$ be thick graphings such that $V^{F}\cap V^{G}\cap V^{H}$ is of
null measure. Then:

$\displaystyle
F\mathop{\mathopen{:}\mathclose{:}}(G\mathop{\mathopen{:}\mathclose{:}}H)$
$\displaystyle=$
$\displaystyle(F\mathop{\mathopen{:}\mathclose{:}}G)\mathop{\mathopen{:}\mathclose{:}}H$
$\displaystyle\mathopen{\llbracket}F,G\mathop{\mathopen{:}\mathclose{:}}H\mathclose{\rrbracket}_{m}+\mathopen{\llbracket}G,H\mathclose{\rrbracket}_{m}$
$\displaystyle=$
$\displaystyle\mathopen{\llbracket}G,H\mathop{\mathopen{:}\mathclose{:}}F\mathclose{\rrbracket}_{m}+\mathopen{\llbracket}H,F\mathclose{\rrbracket}_{m}$

In a similar way, the extension from thick graphings to sliced thick graphings
should now be quite clear. One extends all operations by ”linearity” to formal
weighted sums of thick graphings, and one obtains, when $F,G,H$ are sliced
thick graphings such that $V^{F}\cap V^{G}\cap V^{H}$ is of null measure:

$\displaystyle
F\mathop{\mathopen{:}\mathclose{:}}(G\mathop{\mathopen{:}\mathclose{:}}H)$
$\displaystyle=$
$\displaystyle(F\mathop{\mathopen{:}\mathclose{:}}G)\mathop{\mathopen{:}\mathclose{:}}H$
$\displaystyle\mathopen{\llbracket}F,G\mathop{\mathopen{:}\mathclose{:}}H\mathclose{\rrbracket}_{m}+\textbf{1}_{F}\mathopen{\llbracket}G,H\mathclose{\rrbracket}_{m}$
$\displaystyle=$
$\displaystyle\mathopen{\llbracket}G,H\mathop{\mathopen{:}\mathclose{:}}F\mathclose{\rrbracket}_{m}+\textbf{1}_{G}\mathopen{\llbracket}H,F\mathclose{\rrbracket}_{m}$

###  4.2 Perennial and Co-perennial conducts

Since we are working with sliced thick graphings, we can follow the
constructions of multiplicative and additive connectives as they are studied
in the author’s second paper on interaction graphs [Sei14a] and which were
quickly recalled in Section 2.2.

######  Definition  (Projects).

A _project_ is a couple $\mathfrak{a}=(a,A)$ together with a support $V^{A}$
where:

  * •

$a\in\mathbf{R}\cup\\{\infty\\}$ is called the wager;

  * •

$A$ is a sliced and thick weighted graphing of carrier $V^{A}$, of dialect
$D^{A}$ a discrete probability space, and index $I^{A}$ a finite set.

######  Remark .

We made here the choice to stay close to the hyperfinite geometry of
interaction defined by Girard [Gir11]. This is why we restrict to discrete
probability spaces as dialects, a restriction that corresponds to the
restriction to finite von Neumann algebras of type I as idioms in Girard’s
setting. However, the results of the preceding section about execution and
measurement, and the definition of the family of circuit-quantifying maps do
not rely on this hypothesis. It should therefore be possible to consider a
more general set of project where the dialects may eventually be continuous.
It may turn out that this generalization could be used to define more
expressive exponential connectives than the one defined in this paper, such as
the usual exponentials of linear logic (recall that the exponentials defined
here are the exponentials of Elementary Linear Logic).

As we explained at the end of Section 3, we will need to consider a particular
kind of conducts which are the kind of conducts obtained from the application
of the exponential modality to a conduct and which are unfortunately not
behaviors. We now study these types of conducts.

######  Definition  (Perennialisation).

A Perennialisation is a function that associates a one-sliced weighted
graphing to any sliced and thick weighted graphing.

######  Definition  (Exponentials).

Let $\mathbf{A}$ be a conduct, and $\Omega$ a perennialisation. We define the
$\mathbf{\oc_{\Omega}A}$ as the bi-orthogonal closure of the following set of
projects:

$\sharp_{\Omega}\mathbf{A}=\\{\oc\mathfrak{a}=(0,\Omega(A))\leavevmode\nobreak\
|\leavevmode\nobreak\ \mathfrak{a}=(0,A)\in\mathbf{A},I^{A}\cong\\{1\\}\\}$

The dual connective is of course defined as
$\mathbf{\wn_{\Omega}A}=\mathbf{(\sharp_{\Omega}A^{\simbot})^{\simbot}}$.

######  Definition .

A conduct $\mathbf{A}$ is a _perennial conduct_ when there exists a set $A$ of
projects such that:

  1. 1.

$\mathbf{A}=A^{\simbot\simbot}$;

  2. 2.

for all $\mathfrak{a}=(a,A)\in A$, $a=0$ and $A$ is a one-sliced graphing.

A _co-perennial_ conduct is a conduct $\mathbf{B}=\mathbf{A}^{\simbot}$ where
$\mathbf{A}$ is a perennial conduct.

######  Proposition .

A co-perennial conduct $\mathbf{B}$ satisfies the _inflation property_ : for
all $\lambda\in\mathbf{R}$,
$\mathfrak{b}\in\mathbf{B}\Rightarrow\mathfrak{b+\lambda b}\in\mathbf{B}$.

###### Proof.

The conduct $\mathbf{A}=\mathbf{B}^{\simbot}$ being perennial, there exists a
set $A$ of one-sliced wager-free projects such that
$\mathbf{A}=A^{\simbot\simbot}$. If $A$ is non-empty, the result is a direct
consequence of Section 2.2. If $A$ is empty, then
$\mathbf{B}=\mathbf{A}^{\simbot}=A^{\simbot}$ is the full behavior
$\mathbf{T}_{V^{B}}$ which obviously satisfies the inflation property. ∎

######  Proposition .

A co-perennial conduct is non-empty.

###### Proof.

Suppose that $\mathbf{A}^{\simbot}$ is a co-perennial conduct of carrier
$V^{A}$. Then there exists a set $A$ of one-sliced wager-free projects such
that $\mathbf{A}=\mathbf{A}^{\simbot\simbot}$. If $A$ is empty, then
$A^{\simbot}=\mathbf{A}^{\simbot}$ is the behavior $\mathbf{T}_{V^{A}}$. If
$\mathbf{A}$ is non-empty, then one can easily check that for all real number
$\lambda\neq 0$, the project
$\mathfrak{Dai}_{\lambda}=(\lambda,(V^{A},\emptyset))$ is an element of
$A^{\simbot}=\mathbf{A}^{\simbot}$. ∎

######  Corollary .

Let $\mathbf{A}$ be a perennial conduct. Then
$\mathfrak{a}=(a,A)\in\mathbf{A}\Rightarrow a=0$.

###### Proof.

Since $\mathbf{A}^{\simbot}$ is co-perennial, it is a non-empty set of
projects with the same carrier which satisfies the inflation property. The
result is then obtained by applying Section 2.2. ∎

######  Proposition .

If $\mathbf{A}$ is a co-perennial conduct, then for all $a\neq 0$, the project
$\mathfrak{Dai}_{a}=(a,(V^{A},\emptyset))$ is an element of $\mathbf{A}$.

###### Proof.

We write $B$ the set of one-sliced wager-free projects such that
$B^{\simbot}=\mathbf{A}$. Then for all element $\mathfrak{b}\in\mathbf{B}$, we
have that $\textbf{1}_{B}=1$, from which we conclude that
$\mathopen{\ll}\mathfrak{b},\mathfrak{Dai_{\text{$a$}}}\mathclose{\gg}_{m}=a\textbf{1}_{B}=a$.
Thus $\mathfrak{Dai}_{a}\in B^{\simbot}=\mathbf{A}$ for all $a\neq 0$. ∎

######  Proposition .

The tensor product of perennial conducts is a perennial conduct.

###### Proof.

Let $\mathbf{A,B}$ be perennial conducts. Then there exists two sets of one-
sliced wager-free projects $E,F$ such that $\mathbf{A}=E^{\simbot\simbot}$ and
$\mathbf{B}=F^{\simbot\simbot}$. Using Section 2.2, we know that
$\mathbf{A\otimes B}=(E\odot F)^{\simbot\simbot}$. But, by definition, $E\odot
F$ contains only projects of the form $\mathfrak{e}\otimes\mathfrak{f}$, where
$\mathfrak{e,f}$ are one-sliced and wager-free. Thus $E\odot F$ contains only
one-sliced wager-free projects and $\mathbf{A\otimes B}$ is therefore a
perennial conduct. ∎

######  Proposition .

If $\mathbf{A,B}$ are perennial conducts, then $\mathbf{A\oplus B}$ is a
perennial conduct.

###### Proof.

This is a consequence of Section 2.2. ∎

######  Proposition .

If $\mathbf{A}$ is a perennial conduct and $\mathbf{B}$ is a co-perennial
conduct, then $\mathbf{A\multimap B}$ is a co-perennial conduct.

###### Proof.

We recall that $\mathbf{A\multimap
B}=(\mathbf{A}\otimes\mathbf{B}^{\simbot})^{\simbot}$. Since $\mathbf{A}$ and
$\mathbf{B}^{\simbot}$ are perennial conducts,
$\mathbf{A}\otimes\mathbf{B}^{\simbot}$ is a perennial conduct, and therefore
$\mathbf{A\multimap B}$ is a co-perennial conduct. In particular,
$\mathbf{A\multimap B}$ is non-empty and satisfies the inflation property. ∎

######  Proposition .

If $\mathbf{A}$ is a perennial conduct and $\mathbf{B}$ is a behavior, then
$\mathbf{A\otimes B}$ is a behavior.

###### Proof.

If $\mathbf{A}=\mathbf{0}_{V^{A}}$ with $\mathbf{B}=\mathbf{0}_{V^{B}}$, then
$\mathbf{A\otimes B}=\mathbf{0}_{V^{A}\cup V^{B}}$ which is a behavior.

Let $A$ be the set of one-sliced wager-free projects such that
$\mathbf{A}=A^{\simbot\simbot}$. We have that $\mathbf{A\otimes
B}=(A\odot\mathbf{B})^{\simbot\simbot}$ by Section 2.2. If
$\mathbf{B}\neq\mathbf{0}_{V^{B}}$ and $A\neq 0$, then $A\odot\mathbf{B}$ is
non-empty and contains only wager-free projects. Thus $\mathbf{(A\otimes
B)^{\simbot}}$ satisfies the inflation property by Section 2.2.

Now suppose there exists $\mathfrak{f}=(f,F)\in\mathbf{(A\otimes
B)^{\simbot}}$ such that $f\neq 0$. Then for all $\mathfrak{a}\in A$ and
$\mathfrak{b}\in\mathbf{B}$, $\mathopen{\ll}\mathfrak{f},\mathfrak{a\otimes
b}\mathclose{\gg}_{m}\neq 0,\infty$. But, since $\mathfrak{a}$ is wager-free
and $\textbf{1}_{A}=1$, $\mathopen{\ll}\mathfrak{f},\mathfrak{a\otimes
b}\mathclose{\gg}_{m}=f\textbf{1}_{B}+b\textbf{1}_{F}+\mathopen{\llbracket}F,A\cup
B\mathclose{\rrbracket}_{m}$. We can then define
$\mu=(-\mathopen{\llbracket}F,A\cup
B\mathclose{\rrbracket}_{m}-b\textbf{1}_{F})/f-\textbf{1}_{B}$. Since
$\mathbf{B}$ is a behavior, $\mathfrak{b+\mu 0}\in\mathbf{B}$. However:

$\displaystyle\mathopen{\ll}\mathfrak{f},\mathfrak{a\otimes(b+\mu
0)}\mathclose{\gg}_{m}$ $\displaystyle=$ $\displaystyle
f(\textbf{1}_{B}+\mu)+b\textbf{1}_{F}+\mathopen{\llbracket}F,A\cup(B+\mu
0)\mathclose{\rrbracket}_{m}$ $\displaystyle=$ $\displaystyle
f(\textbf{1}_{B}+\mu)+b\textbf{1}_{F}+\mathopen{\llbracket}F,A\cup
B\mathclose{\rrbracket}_{m}$ $\displaystyle=$ $\displaystyle
f(\textbf{1}_{B}+(-\mathopen{\llbracket}F,A\cup
B\mathclose{\rrbracket}_{m}-b\textbf{1}_{F})/f-\textbf{1}_{B})+b\textbf{1}_{F}+\mathopen{\llbracket}F,A\cup
B\mathclose{\rrbracket}_{m}$ $\displaystyle=$
$\displaystyle-\mathopen{\llbracket}F,A\cup
B\mathclose{\rrbracket}_{m}-b\textbf{1}_{F}+b\textbf{1}_{F}+\mathopen{\llbracket}F,A\cup
B\mathclose{\rrbracket}_{m}$ $\displaystyle=$ $\displaystyle 0$

But this is a contradiction. Therefore the elements in $\mathbf{(A\otimes
B)^{\simbot}}$ are wager-free.

If $\mathbf{(A\otimes B)^{\simbot}}$ is non-empty, it is a non-empty conduct
containing only wager-free projects and satisfying the inflation property: it
is therefore a (proper) behavior.

The only case left to treat is when $\mathbf{(A\otimes B)^{\simbot}}$ is
empty, but then $\mathbf{A\otimes B}=\mathbf{T}_{V^{A}\cup V^{B}}$ is clearly
a behavior. ∎

######  Corollary .

If $\mathbf{A}$ is perennial and $\mathbf{B}$ is a behavior, then
$\mathbf{A\multimap B}$ is a behavior.

###### Proof.

We recall that $\mathbf{A\multimap B}=(\mathbf{A\otimes
B^{\simbot}})^{\simbot}$. Using the preceding proposition, the conduct
$\mathbf{A\otimes B^{\simbot}}$ is a behavior since $\mathbf{A}$ is a
perennial conduct and $\mathbf{B}^{\simbot}$ is a behavior. Thus
$\mathbf{A\multimap B}$ is a behavior since it is the orthogonal of a
behavior. ∎

######  Corollary .

If $\mathbf{A}$ is a behavior and $\mathbf{B}$ is a co-perennial conduct, then
$\mathbf{A\multimap B}$ is a behavior.

###### Proof.

One just has to write $\mathbf{A\multimap B}=\mathbf{(A\otimes
B^{\simbot})^{\simbot}}$. Since $\mathbf{A\otimes B^{\simbot}}$ is the tensor
product of a behavior with a perennial conduct, it is a behavior. The result
then follows from the fact that the orthogonal of a behavior is a behavior. ∎

######  Proposition .

The weakening (on the left) of perennial conducts holds.

###### Proof.

Let $\mathbf{A,B}$ be conducts, and $\mathbf{N}$ be a perennial conduct. Chose
$\mathfrak{f}\in\mathbf{A\multimap B}$. We will show that
$\mathfrak{f}\otimes\mathfrak{0}_{V^{N}}$ is a project in $\mathbf{A\otimes
N\multimap B}$. For this, we pick $\mathfrak{a}\in\mathbf{A}$ and
$\mathfrak{n}\in\mathbf{N}$ (recall that $\mathfrak{n}$ is necessarily wager-
free). Then for all $\mathfrak{b^{\prime}}\in\mathbf{B^{\simbot}}$,

$\displaystyle\mathopen{\ll}\mathfrak{(f\otimes
0)\mathop{\mathopen{:}\mathclose{:}}(a\otimes
n)},\mathfrak{b^{\prime}}\mathclose{\gg}_{m}$ $\displaystyle=$
$\displaystyle\mathopen{\ll}\mathfrak{f\otimes 0},\mathfrak{(a\otimes
n)\otimes b}\mathclose{\gg}_{m}$ $\displaystyle=$
$\displaystyle\mathopen{\ll}\mathfrak{f\otimes 0},\mathfrak{(a\otimes
b^{\prime})\otimes n}\mathclose{\gg}_{m}$ $\displaystyle=$
$\displaystyle\textbf{1}_{F}(\textbf{1}_{A}\textbf{1}_{B^{\prime}}n+\textbf{1}_{N}\textbf{1}_{A}b^{\prime}+\textbf{1}_{N}\textbf{1}_{B^{\prime}}a)+\textbf{1}_{N}\textbf{1}_{A}\textbf{1}_{B^{\prime}}f+\mathopen{\llbracket}F\cup
0,A\cup B^{\prime}\cup N\mathclose{\rrbracket}_{m}$ $\displaystyle=$
$\displaystyle\textbf{1}_{F}(\textbf{1}_{N}\textbf{1}_{A}b^{\prime}+\textbf{1}_{N}\textbf{1}_{B^{\prime}}a)+\textbf{1}_{N}\textbf{1}_{A}\textbf{1}_{B^{\prime}}f+\mathopen{\llbracket}F\cup
0,A\cup B^{\prime}\cup N\mathclose{\rrbracket}_{m}$ $\displaystyle=$
$\displaystyle\textbf{1}_{N}(\textbf{1}_{F}(\textbf{1}_{A}b^{\prime}+\textbf{1}_{B^{\prime}}a)+\textbf{1}_{A}\textbf{1}_{B^{\prime}}f)+\textbf{1}_{N}\mathopen{\llbracket}F,A\cup
B^{\prime}\mathclose{\rrbracket}_{m}$ $\displaystyle=$
$\displaystyle\textbf{1}_{N}\mathopen{\ll}\mathfrak{f},\mathfrak{a\otimes
b^{\prime}}\mathclose{\gg}_{m}$

Since $\textbf{1}_{N}\neq 0$, $\mathopen{\ll}\mathfrak{(f\otimes
0)\mathop{\mathopen{:}\mathclose{:}}(a\otimes
n)},\mathfrak{b^{\prime}}\mathclose{\gg}_{m}\neq 0,\infty$ if and only if
$\mathopen{\ll}\mathfrak{f\mathop{\mathopen{:}\mathclose{:}}a},\mathfrak{b^{\prime}}\mathclose{\gg}_{m}\neq
0,\infty$. Thus for all $\mathfrak{a\otimes n}\in\mathbf{A\odot N}$,
$\mathfrak{(f\otimes 0)\mathop{\mathopen{:}\mathclose{:}}(a\otimes
n)}\in\mathbf{B}$. This shows that $\mathfrak{f\otimes 0}\in\mathbf{A\otimes
N\multimap B}$ by Section 3.3. ∎

###  4.3 A Construction of Exponentials

We will begin by showing a technical result that will allow us to define
measure preserving transformations from bijections of the set of integers.
This result will be used to show that functorial promotion can be implemented
for our exponential modality.

######  Definition .

Let $\phi:\mathbf{N}\rightarrow\mathbf{N}$ be a bijection and $b$ an integer
$\geqslant 2$. Then $\phi$ induces a transformation
$T^{b}_{\phi}:[0,1]\rightarrow[0,1]$ defined by $\sum_{i\geqslant
0}a_{k}2^{-k}\mapsto\sum_{i\geqslant 0}a_{\phi^{-1}(k)}2^{-k}$.

######  Remark .

Suppose that $\sum_{i\geqslant 0}a_{i}b^{-i}$ and $\sum_{i\geqslant
0}a^{\prime}_{i}b^{-i}$ are two distinct representations of a real number $r$.
Let us fix $i_{0}$ to be the smallest integer such that $a_{i_{0}}\neq
a^{\prime}_{i_{0}}$. We first notice that the absolute value of the difference
between these digits has to be equal to $1$:
$\mathopen{\lvert}a_{i_{0}}-a^{\prime}_{i_{0}}\mathclose{\rvert}=1$. Indeed,
if this was not the case, i.e. if
$\mathopen{\lvert}a_{i_{0}}-a^{\prime}_{i_{0}}\mathclose{\rvert}\geqslant 2$,
the distance between $\sum_{i\geqslant 0}a_{i}b^{-i}$ and $\sum_{i\geqslant
0}a^{\prime}_{i}b^{-i}$ would be greater than $b^{-i_{0}}$, which contradicts
the fact that both sums are equal to $r$. Let us now suppose, without loss of
generality, that $a_{i_{0}}=a^{\prime}_{i_{0}}+1$. Then $a_{j}=0$ for all
$j>i_{0}$ since if there existed an integer $j>i_{0}$ such that $a_{j}\neq 0$,
the distance between the sums $\sum_{i\geqslant 0}a_{i}b^{-i}$ and
$\sum_{i\geqslant 0}a^{\prime}_{i}b^{-i}$ would be greater than $b^{-j}$,
which would again be a contradiction. Moreover, $a^{\prime}_{j}=b-1$ for all
$j>i_{0}$: if this was not the case, one could show in a similar way that the
difference between the two sums would be strictly greater than $0$. We can
deduce from this that only the reals with a finite representation in base $b$
have two distinct representations.

Since the set of such elements is of null measure, the transformation
$T_{\phi}$ associated to a bijection $\phi$ of $\mathbf{N}$ is well defined as
we can define $T_{\phi}$ only on the set of reals that have a unique
representation. We can however chose to deal with this in another way:
choosing between the two possible representations, by excluding for instance
the representations as sequences that are almost everywhere equal to zero.
Then $T_{\phi}$ is defined at all points and bijective. We chose in the
following to follow this second approach since it will allow to prove more
easily that $T_{\phi}$ is measure-preserving. However, this choice is not
relevant for the rest of the construction since both transformations are
almost everywhere equal.

######  Lemma .

Let $T$ be a transformation of $[0,1]$ such that for all interval $[a,b]$,
$\lambda(T([a,b]))=\lambda([a,b])$. Then $T$ is measure-preserving on $[0,1]$.

###### Proof.

A classical result of measure theory states that if $T$ is a transformation of
a measured space $(X,\mathcal{B},\lambda)$, that $\mathcal{B}$ is generated by
$\mathcal{A}$, and that for all $A\in\mathcal{A}$, $\lambda(T(A))=\lambda(A)$,
then $T$ preserves the measure $\lambda$ on $X$. Applying this result with
$X=[0,1]$, and $\mathcal{A}$ as the set of intervals $[a,b]\subset[0,1]$, we
obtain the result. ∎

######  Lemma .

Let $T$ be a bijective transformation of $[0,1]$ that preserves the measure on
all interval $I$ of the shape
$[\sum_{k=1}^{p}a_{k}b^{-k},\sum_{k=1}^{p}a_{k}b^{-k}+b^{-p}]$. Then $T$ is
measure-preserving on $[0,1]$.

###### Proof.

Chose $[a,b]\subset[0,1]$. One can write $[a,b]$ as a union
$\cup_{i=0}^{\infty}[a_{i},a_{i+1}]$, where for all $i\geqslant 0$,
$a_{i+1}=a_{i}+b^{-k_{i}}$. We then obtain, using the hypotheses of the
statement and the $\sigma$-additivity of the measure $\lambda$:

$\displaystyle\lambda(T([a,b]))$ $\displaystyle=$
$\displaystyle\lambda(T(\cup_{i=0}^{\infty}[a_{i},a_{i+1}[))$ $\displaystyle=$
$\displaystyle\lambda(\cup_{i=0}^{\infty}T([a_{i},a_{i+1}[))$ $\displaystyle=$
$\displaystyle\sum_{i=0}^{\infty}\lambda(T([a_{i},a_{i+1}[))$ $\displaystyle=$
$\displaystyle\sum_{i=0}^{\infty}\lambda([a_{i},a_{i+1}[)$ $\displaystyle=$
$\displaystyle\lambda(\cup_{i=0}^{\infty}[a_{i},a_{i+1}[)$ $\displaystyle=$
$\displaystyle\lambda([a,b])$

We now conclude by using the preceding lemma. ∎

######  Theorem .

Let $\phi:\mathbf{N}\rightarrow\mathbf{N}$ be a bijection and $b\geqslant 2$
an integer. Then the transformation $T^{b}_{\phi}$ is measure-preserving.

###### Proof.

We recall first that the transformation $T^{b}_{\phi}$ is indeed bijective
(see Section 4.3).

By using the preceding lemma, it suffices to show that $T^{b}_{\phi}$
preserves the measure on intervals of the shape $I=[a,a+b^{-k}]$ with
$a=\sum_{i=0}^{k}a_{i}b^{-i}$. Let us define
$N=\max\\{\phi(i)\leavevmode\nobreak\ |\leavevmode\nobreak\ 0\leqslant
i\leqslant k\\}$. We then write $[0,1]$ as the union of intervals
$A_{i}=[i\times b^{-N},(i+1)\times b^{-N}]$ where $0\leqslant i\leqslant
b^{N}-1$.

Then the image if $I$ by $T^{b}_{\phi}$ is equal to the union of the $A_{i}$
for $i\times b^{-N}=\sum_{i=0}^{N}x_{i}b^{-i}$, where $x_{\phi(j)}=a_{j}$ for
all $0\leqslant j\leqslant k$. The number of such $A_{j}$ is equal to the
number of sequences $\\{0,\dots,b-1\\}$ of length $N-k$, i.e. $b^{N-k}$. Since
each $A_{j}$ has a measure equal to $b^{-N}$, the image of $I$ by
$T^{b}_{\phi}$ is of measure $b^{-N}b^{N-k}=b^{-k}$, which is equal to the
measure of $I$ since $\lambda(I)=b^{-k}$. ∎

######  Remark .

The preceding theorem can be easily generalized to bijections
$\mathbf{N}+\dots+\mathbf{N}\rightarrow\mathbf{N}$ (the domain being the
disjoint union of $k$ copies of $\mathbf{N}$, $k\in\mathbf{N}$) which induce
measure-preserving bijections from $[0,1]^{k}$ onto $[0,1]$. The particular
case $\mathbf{N}+\mathbf{N}\rightarrow\mathbf{N}$, $(n,i)\mapsto 2n+i$ defines
the well-known measure-preserving bijection between the unit square and the
interval $[0,1]$:

$(\sum_{i\geqslant 0}a_{i}2^{-i},\sum_{i\geqslant
0}b_{i}2^{-i})\mapsto\sum_{i\geqslant 0}a_{2i}2^{-2i}+b_{2i+1}2^{-2i-1}$

Let us now define the bijection:

$\psi:\mathbf{N}+\mathbf{N}+\mathbf{N}\rightarrow\mathbf{N},\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ (x,i)\mapsto 3x+i$

We also define the injections $\iota_{i}$ ($i=0,1,2$):

$\iota_{i}:\mathbf{N}\rightarrow\mathbf{N}+\mathbf{N}+\mathbf{N},\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ x\mapsto(x,i)$

We will denote by $\psi_{i}$ the composite
$\psi\circ\iota_{i}:\mathbf{N}\rightarrow\mathbf{N}$.

######  Definition .

Let $A\subset\mathbf{N}+\mathbf{N}+\mathbf{N}$ be a finite set. We write $A$
as $A_{0}+A_{1}+A_{2}$, and define, for $i=0,1,2$, $n_{i}$ to be the
cardinality of $A_{i}$ if $A_{i}\neq$ and $n_{i}=1$ otherwise. We then define
a partition of $[0,1]$, denoted by
$\mathcal{P}_{A}=\\{P_{A}^{i_{1},i_{2},i_{3}}\leavevmode\nobreak\
|\leavevmode\nobreak\ \forall k\in\\{0,1,2\\},0\leqslant i_{k}\leqslant
n_{i}-1\\}$, by:

$P_{A}^{i_{1},i_{2},i_{3}}=\\{\sum_{j\geqslant
1}a_{j}2^{-j}\leavevmode\nobreak\ |\leavevmode\nobreak\ \forall
k\in\\{0,1,2\\},\frac{i_{k}}{n_{k}}\leqslant\sum_{j\geqslant
1}a_{\psi_{k}(j)}2^{-j}\leqslant\frac{i_{k}+1}{n_{k}}\\}$

When $A_{k}$ is empty or of cardinality $1$, we will not write the
corresponding $i_{k}$ in the triple $(i_{1},i_{2},i_{3})$ since it is
necessarily equal to $0$.

######  Proposition .

Let us keep the notations of the preceding proposition and let
$X=P_{A}^{i_{1},i_{2},i_{3}}$ and $Y=P_{A}^{j_{1},j_{2},j_{3}}$ be two
elements of the partition $\mathcal{P}_{A}$. For all $x=\sum_{l\geqslant
1}a_{l}2^{-l}$, we define
$T_{i_{1},i_{2},i_{3}}^{j_{1},j_{2},j_{3}}(x)=\sum_{l\geqslant 1}b_{l}2^{-l}$
where the sequence $(b_{i})$ is defined by:

$\forall k\in\\{0,1,2\\},\sum_{l\geqslant
1}b_{\psi_{k}(l)}2^{-l}=\sum_{l\geqslant 1}a_{\psi_{k}(l)}2^{-l}+j_{k}-i_{k}$

Then $T_{i_{1},i_{2},i_{3}}^{j_{1},j_{2},j_{3}}:X\rightarrow Y$ is a measure-
preserving bijection.

###### Proof.

For $k=0,1,2$, we will denote by $(m^{k}_{j})$ the sequence such that
$j_{k}-i_{k}=\sum_{l\geqslant 1}m^{k}_{l}2^{-l}$. We can define the real
number $t=\sum_{l\geqslant 1}\sum_{k=0,1,2}m^{k}_{l}2^{-3j+k}$. It is then
sufficient to check that $T_{i_{1},i_{2},i_{3}}^{j_{1},j_{2},j_{3}}(x)=x+t$.
Since $T_{i_{1},i_{2},i_{3}}^{j_{1},j_{2},j_{3}}$ is a translation
translation, it is a measure-preserving bijection. ∎

######  Definition .

Let $A\subset\mathbf{N}$ be a finite set endowed with the normalized — i.e.
such that $A$ has measure $1$ — counting measure, and
$X\subset\mathcal{B}(\mathbf{R}\times A)$ be a measurable set. We define the
measurable subset
$\mathopen{\ulcorner}A\mathclose{\urcorner}\in\mathbf{R}\times[0,1]$:

$\mathopen{\ulcorner}A\mathclose{\urcorner}=\\{(x,y)\leavevmode\nobreak\
|\leavevmode\nobreak\ \exists z\in A,(x,z)\in X,y\in P_{A}^{z}\\}$

We will write $\mathcal{P}^{-1}_{A}:[0,1]\rightarrow A$ the map that
associates to each $x$ the element $z\in A$ such that $x\in P_{A}^{z}$.

######  Proposition .

Let $D^{A}\subset\mathbf{N}$ be a finite set endowed with the normalized
counting measure $\mu$ (i.e. such that $\mu(A)=1$),
$S,T\in\mathcal{B}(\mathbf{R}\times D^{A})$ be measurable sets, and
$\phi:S\rightarrow T$ a measure-preserving transformation. We define
$\mathopen{\ulcorner}\phi\mathclose{\urcorner}:\mathopen{\ulcorner}S\mathclose{\urcorner}\rightarrow\mathopen{\ulcorner}T\mathclose{\urcorner}$
by:

$\mathopen{\ulcorner}\phi\mathclose{\urcorner}:(x,y)\mapsto(x^{\prime},y^{\prime})\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
\phi(x,\mathcal{P}^{-1}_{A}(y))=(x^{\prime},z),\leavevmode\nobreak\
\leavevmode\nobreak\ y^{\prime}=T_{\mathcal{P}^{-1}_{A}(y)}^{z}$

Then $\mathopen{\ulcorner}\phi\mathclose{\urcorner}$ is a measure-preserving
bijection.

###### Proof.

For all $(a,b)\in D^{A}$ we define the set
$S_{a,b}=X\cap\mathbf{R}\times\\{a\\}\cap\phi^{-1}(Y\cap\mathbf{R}\times\\{b\\})$.
The family $(S_{a,b})_{a,b\in D^{A}}$ is a partition of $S$, and the family
$(\mathopen{\ulcorner}S_{a,b}\mathclose{\urcorner})_{a,b\in D^{A}}$ is a
partition of $\oc A$. The restriction of
$\mathopen{\ulcorner}\phi\mathclose{\urcorner}$ to
$\mathopen{\ulcorner}S_{a,b}\mathclose{\urcorner}$ can then be defined as the
composite $T_{a}\circ\phi_{1}$ with:

$\displaystyle\phi_{1}$ $\displaystyle=$
$\displaystyle(\pi_{1}\circ\phi)\times\text{Id}$ $\displaystyle T_{a}$
$\displaystyle=$ $\displaystyle\text{Id}\times T_{a}^{b}$

Since the product (resp. the composition) of measure preserving bijections is
a measure preserving bijection, the restriction of
$\mathopen{\ulcorner}\phi\mathclose{\urcorner}$ to $X_{a}$ is a measure
preserving bijection. Moreover, it is clear that the image of
$\mathopen{\ulcorner}S\mathclose{\urcorner}$ by
$\mathopen{\ulcorner}\phi\mathclose{\urcorner}$ is equal to
$\mathopen{\ulcorner}T\mathclose{\urcorner}$ and we have finished the proof. ∎

######  Definition .

Let $A$ be a thick graphing, i.e. of support $V^{A}\subset\mathbf{R}\times
D^{A}$ measurable, where $D^{A}$ is a finite subset of $\mathbf{N}$ endowed
with the normalized counting measure. We define the graphing:

$\mathopen{\ulcorner}A\mathclose{\urcorner}=\\{(\omega_{e}^{A},\mathopen{\ulcorner}\phi_{e}^{A}\mathclose{\urcorner}:\mathopen{\ulcorner}S_{e}^{A}\mathclose{\urcorner}\rightarrow\mathopen{\ulcorner}T_{e}^{A}\mathclose{\urcorner}\\}_{e\in
E^{A}}$

######  Definition .

Let $A$ be a thick graphing of dialect $D^{A}$, and
$\Omega:\mathbf{R}\times[0,1]\rightarrow\mathbf{R}$ an isomorphism of measured
spaces. We define the graphing $\oc_{\Omega}A$ by:

$\oc_{\Omega}A=\\{(\omega_{e}^{A},\Omega\circ\mathopen{\ulcorner}\phi_{e}^{A}\mathclose{\urcorner}\circ\Omega^{-1}:\Omega(\mathopen{\ulcorner}S_{e}^{A}\mathclose{\urcorner})\rightarrow\Omega(\mathopen{\ulcorner}T_{e}^{A}\mathclose{\urcorner})\\}_{e\in
E^{A}}$

######  Definition .

A project $\mathfrak{a}$ is _balanced_ if $\mathfrak{a}=(0,A)$ where $A$ is a
thick graphing, i.e. $I^{A}$ is a one-element set, for instance
$I^{A}=\\{1\\}$, and $\alpha^{A}_{1}=1$.

######  Definition .

Let $\mathfrak{a}$ be a balanced project. We define
$\oc_{\Omega}\mathfrak{a}=(0,\oc_{\Omega}A)$. If $\mathbf{A}$ is a conduct, we
define:

$\oc_{\Omega}\mathbf{A}=\\{\oc_{\Omega}\mathfrak{a}\leavevmode\nobreak\
|\leavevmode\nobreak\ \mathfrak{a}=(0,A)\in\mathbf{A},\text{ $\mathfrak{a}$
balanced}\\}^{\simbot\simbot}$

We will now show that it is possible to implement the functorial promotion. In
order to do this, we define the bijections
$\tau,\theta:\mathbf{N}+\mathbf{N}+\mathbf{N}\rightarrow\mathbf{N}+\mathbf{N}+\mathbf{N}$:

$\displaystyle\tau$ $\displaystyle:$
$\displaystyle\left\\{\begin{array}[]{rcl}(x,0)&\mapsto&(x,1)\\\
(x,1)&\mapsto&(x,0)\\\ (x,2)&\mapsto&(x,2)\end{array}\right.$
$\displaystyle\theta$ $\displaystyle:$
$\displaystyle\left\\{\begin{array}[]{rcl}(x,0)&\mapsto&(2x,0)\\\
(x,1)&\mapsto&(2x+1,1)\\\ (2x,2)&\mapsto&(x,1)\\\
(2x+1,2)&\mapsto&(x,2)\end{array}\right.$

These bijections induce bijections of $\mathbf{N}$ onto $\mathbf{N}$ through
$\psi:(x,i)\mapsto 3x+i$. We will abusively denote by
$T_{\tau}=T_{\psi\circ\tau\circ\psi^{-1}}$ and
$T_{\theta}=T_{\psi\circ\theta\circ\psi^{-1}}$ the induced measure-preserving
transformations $[0,1]\rightarrow[0,1]$.

Pick $\mathfrak{a}\in\mathbf{\sharp\phi(A)}$ and
$\mathfrak{f}\in\sharp(\mathbf{A\multimap B})$, where $\phi$ is a delocation.
By definition,
$\mathfrak{a}=(0,\Omega(\mathopen{\ulcorner}A\mathclose{\urcorner}))$ and
$\mathfrak{f}=(0,\Omega(\mathopen{\ulcorner}F\mathclose{\urcorner}))$ where
$A,F$ are graphings of respective dialects $D^{A},D^{F}$. We define the
graphing $T=\\{(1,\Omega(\text{Id}\times T_{\tau})),(1,(\Omega(\text{Id}\times
T_{\tau}))^{-1})\\}$ of carrier $V^{\phi(A)}\cup V^{A}$, and denote by
$t,t^{\ast}$ the two edges in $E^{T}$. We fix $(x,y)$ an element of $V^{B}$
and we will try to understand the action of the path
$f_{0}ta_{0}t^{\ast}f_{1}\dots ta_{k-1}t^{\ast}f_{k}$.

We fix the partition $\mathcal{P}_{D^{F}+D^{A}}$ of $[0,1]$, and denote by
$(i,j)$ the integers such that $y\in\mathcal{P}_{D^{F}+D^{A}}^{i,j}$. By
definition of $\mathopen{\ulcorner}F\mathclose{\urcorner}$, the map
$\mathopen{\ulcorner}\phi^{F}_{f_{0}}\mathclose{\urcorner}$ sends this element
to $(x_{1},y_{1})$ which is an element of
$\mathcal{P}_{D^{F}+D^{A}}^{i_{1},j_{1}}$ with $j_{1}=j$. Then, the function
$\phi_{t}$ sends this element on $(x_{2},y_{2})$, where $x_{2}=x_{1}$ and
$y_{2}$ is an element of $\mathcal{P}_{D^{F}+D^{A}}^{j_{1},i_{1}}$. The
function $\mathopen{\ulcorner}\phi_{a_{0}}^{A}\mathclose{\urcorner}$ then
produces an element $(x_{3},y_{3})$ with $y_{3}$ in
$\mathcal{P}_{D^{F}+D^{A}}^{j_{2},i_{2}}$ and $i_{2}=i_{1}$. The element
produced by $\phi_{t^{\ast}}=\phi_{t}^{-1}$ is then $(x_{4},y_{4})$ where
$y_{4}$ is an element of $\mathcal{P}_{D^{F}+D^{A}}^{i_{2},j_{2}}$. One can
therefore see how the graphing $T$ simulates the dialectal interaction. The
following proposition will show how one can use $T$ to implement functorial
promotion.

In order to implement functorial promotion, we will make use of the three
bijections we just defined. Though it may seem a complicated, the underlying
idea is quite simple. We will be working with three disjoint copies of
$\mathbf{N}$, let us say $\mathbf{N}_{i}$ ($i=0,1,2$). When applying
promotion, we will encode the information contained in the dialect on the
first copy $\mathbf{N}_{0}$ (let us stress here that promotion is defined
through a non-surjective map, something that will be essential in the
following). Suppose now that we have two graphs obtained from two promotions:
all the information they contain is located in their first copy
$\mathbf{N}_{0}$. To simulate dialectal information, we need to make these two
sets disjoint: this is where the second copy $\mathbf{N}_{1}$ will be used.
Hence, we apply to one of these promoted graphs the bijection $\tau$ (in
practice we will of course use $\tau$ through the induced transformation
$T_{\tau}$) which exchanges $\mathbf{N}_{0}$ and $\mathbf{N}_{1}$. The
information coming from the dialects of the two graphs are now disjoint. We
then compute the execution of the two graphs to obtain a graph whose
information coming from the dialect is encoded on the two copies
$\mathbf{N}_{0}$ and $\mathbf{N}_{1}$! In order to be able to see this
obtained graph as a graph obtained from a promotion, we need now to move this
information so that it is encoded on the first copy $\mathbf{N}_{0}$ only.
This is where we use the third copy $\mathbf{N}_{2}$: we use the bijection
$\theta$ (once again, we use in practice the induced transformation
$T_{\theta}$) in order to contract the two copies $\mathbf{N}_{0}$ and
$\mathbf{N}_{1}$ on the first copy $\mathbf{N}_{0}$, while deploying the third
copy $\mathbf{N}_{2}$ onto the two copies $\mathbf{N}_{1}$ and
$\mathbf{N}_{2}$.

######  Proposition .

One can implement functorial promotion: for all delocations $\phi,\psi$ and
conducts $\mathbf{A,B}$ such that $\mathbf{\phi(A),A,B,\psi(B)}$ have pairwise
disjoint carriers, there exists a project $\mathfrak{prom}$ in the conduct

$\mathbf{\oc\phi(A)}\otimes\oc(\mathbf{A\multimap
B})\multimap\mathbf{\oc\psi(B)}$

###### Proof.

Let $\mathfrak{f}\in\mathbf{A\multimap B}$ be a balanced project, $\phi,\psi$
two delocations of $\mathbf{A}$ and $\mathbf{B}$ respectively. We define the
graphings $T=\\{(1,\Omega(\text{Id}\times
T_{\tau})),(1,(\Omega(\text{Id}\times T_{\tau}))^{-1})\\}$ of carrier
$V^{\phi(A)}\cup V^{A}$ and $P=\\{(1,\Omega(\text{Id}\times
T_{\theta})),(1,(\Omega(\text{Id}\times T_{\theta}))^{-1})\\}$ of carrier
$V^{B}\cup V^{\psi(B)}$. We define $\mathfrak{t}=(0,T)$ and
$\mathfrak{p}=(0,P)$, and the project:

$\mathfrak{prom}=(0,T\cup P)=\mathfrak{t}\otimes\mathfrak{p}$

We will now show that $\mathfrak{prom}$ is an element in
$\mathbf{(\oc\phi(A)\otimes\oc(A\multimap B))\multimap\oc\psi(B)}$.

We can suppose, up to choosing refinements of $A$ and $F$, that for all $e\in
E^{A}\cup E^{F}$, $(S_{e})_{2}$ and $(T_{e})_{2}$ are one-elements
sets121212The sets $S_{e}$ and $T_{e}$ being subsets of a product, w write
$(S_{e})_{2}$ (resp. $(T_{e})_{2}$) the result of their projection on the
second component..

Pick $\mathfrak{a}\in\mathbf{\sharp\phi(A)}$ and
$\mathfrak{f}\in\sharp(\mathbf{A\multimap B})$. Then, by definition
$\mathfrak{a}=(0,\Omega(\mathopen{\ulcorner}A\mathclose{\urcorner}))$ and
$\mathfrak{f}=(0,\Omega(\mathopen{\ulcorner}F\mathclose{\urcorner}))$ where
$A,F$ are graphings of dialects $D^{A},D^{F}$. We get that $\mathfrak{a\otimes
f}\mathop{\mathopen{:}\mathclose{:}}\mathfrak{prom}=((\mathfrak{a}\mathop{\mathopen{:}\mathclose{:}}\mathfrak{t})\mathop{\mathopen{:}\mathclose{:}}\mathfrak{f})\mathop{\mathopen{:}\mathclose{:}}\mathfrak{p}$
from the associativity and commutativity of
$\mathop{\mathopen{:}\mathclose{:}}$ (recall that $\mathfrak{a\otimes
f}=\mathfrak{a\mathop{\mathopen{:}\mathclose{:}}f}$).

We show that
$\mathopen{\ulcorner}A\mathclose{\urcorner}\mathop{\mathopen{:}\mathclose{:}}\mathopen{\ulcorner}T\mathclose{\urcorner}$
is the graphings composed of the $\oc^{\tau}\phi_{a}$ for $a\in E^{A}$, where
$\oc^{\tau}\phi_{a}$ is defined by:

$\oc^{\tau}\phi_{a}:(x,y)\mapsto(x^{\prime},y^{\prime}),\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\
\phi_{a}(x,\mathcal{P}_{\\{0\\}+D^{A}}^{-1}(y))=(x^{\prime},z),\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
y^{\prime}=T_{\mathcal{P}_{\\{0\\}+D^{A}}^{-1}(y)}^{(z,1)}(y)$

This is almost straightforward. An element in
$\mathopen{\ulcorner}A\mathclose{\urcorner}\mathop{\mathopen{:}\mathclose{:}}\mathopen{\ulcorner}T\mathclose{\urcorner}$
is a path of the form $tat^{\ast}$. It is therefore the function
$\phi_{t}\circ\mathopen{\ulcorner}\phi_{a}\mathclose{\urcorner}\circ\phi_{t}^{-1}$.
By definition,

$\mathopen{\ulcorner}\phi_{a}\mathclose{\urcorner}:(x,y)\mapsto(x^{\prime},y^{\prime})\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
n=\mathcal{P}_{A}^{-1}(y),\leavevmode\nobreak\ \leavevmode\nobreak\
\phi_{a}(x,n)=(x^{\prime},k),\leavevmode\nobreak\ y^{\prime}=T_{n}^{k}(y)$

But $\phi_{t}:\text{Id}\times T_{\tau}$ and $T_{\tau}$ is a bijection from
$\mathcal{P}_{A}(y)$ to $\mathcal{P}_{\\{0\\}+A}(1,y)$.

We now describe the graphing
$G=(\mathopen{\ulcorner}A\mathclose{\urcorner}\mathop{\mathopen{:}\mathclose{:}}\mathopen{\ulcorner}T\mathclose{\urcorner})\mathop{\mathopen{:}\mathclose{:}}\mathopen{\ulcorner}F\mathclose{\urcorner}$.
It is composed of the paths of the shape
$\rho=f_{0}(ta_{0}t^{\ast})f_{1}(ta_{1}t^{\ast})f_{2}\dots
f_{n-1}(ta_{n-1}t^{\ast})f_{n}$. The associated function is therefore:

$\phi_{\rho}=\mathopen{\ulcorner}\phi_{f_{0}}\mathclose{\urcorner}(\oc^{\tau}\phi_{a_{0}})\mathopen{\ulcorner}\phi_{f_{1}}\mathclose{\urcorner}\dots\mathopen{\ulcorner}\phi_{f_{n-1}}\mathclose{\urcorner}(\oc^{\tau}\phi_{a_{n-1}})\mathopen{\ulcorner}\phi_{f_{n}}\mathclose{\urcorner}$

Let $\pi=f_{0}a_{0}f_{1}\dots f_{n-1}a_{n-1}f_{n}$ be the corresponding path
in $F\mathop{\mathopen{:}\mathclose{:}}A$. The function $\phi_{\pi}$ has, by
definition, as domain and codomain measurable subsets of $\mathbf{R}\times
D^{F}\times D^{A}$. We define, for such a function, the function
$\mathop{\rotatebox[origin={c}]{180.0}{$\oc$}}\phi_{\pi}$ by:

$\displaystyle\mathop{\rotatebox[origin={c}]{180.0}{$\oc$}}\phi_{\pi}:(x,y)\mapsto(x^{\prime},y^{\prime})$
$\displaystyle(n,m)=\mathcal{P}_{D^{F}+D^{A}}^{-1}(y),\leavevmode\nobreak\
\leavevmode\nobreak\ \phi_{\pi}(x,n,m)=(x^{\prime},k,l),\leavevmode\nobreak\
\leavevmode\nobreak\ y^{\prime}=T_{(n,m)}^{(k,l)}(y)$

One can then check that
$\mathop{\rotatebox[origin={c}]{180.0}{$\oc$}}\phi_{\pi}=\phi_{\rho}$.

Finally,
$G\mathop{\mathopen{:}\mathclose{:}}\mathopen{\ulcorner}P\mathclose{\urcorner}$
is the graphing composed of paths that have the shape $p\rho p^{\ast}$ where
$\rho$ is a path in $G$. But $\phi_{p}=\text{Id}\times T_{\theta}$ applies a
bijection, for all couple $(k,l)\in D^{F}\times D^{A}$, from the set
$\mathcal{P}_{D^{F}+D^{A}}^{k,l}$ to the set
$\mathcal{P}_{\theta(D^{F}+D^{A})}^{\theta(k,l)}$ where:

$\theta(D^{F}+D^{A})=\\{\theta(f,a)\leavevmode\nobreak\ |\leavevmode\nobreak\
f\in D^{F},a\in D^{A}\\}$

We deduce that:

$\displaystyle\phi_{p\rho p^{\ast}}:(x,y)\mapsto(x^{\prime},y^{\prime})$
$\displaystyle
n=\theta(k,l)=\mathcal{P}_{\theta(D^{F}+D^{A})}^{-1}(y)\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
\phi_{\pi}(x,k,l)=(x^{\prime},k^{\prime},l^{\prime})\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
y^{\prime}=T_{n}^{\theta(k^{\prime},l^{\prime})}(y)$

Modulo the bijection $\mu:D^{F}\times
D^{A}\rightarrow\theta(D^{F}+D^{A})\subset\mathbf{N}$, we get that
$G\mathop{\mathopen{:}\mathclose{:}}\mathopen{\ulcorner}P\mathclose{\urcorner}$
is the delocation (along $\psi$) of the graphing
$\oc(F\mathop{\mathopen{:}\mathclose{:}}A)$.

Therefore, for all $\mathfrak{a},\mathfrak{f}$ in $\mathbf{\sharp
A},\mathbf{\sharp(A\multimap B)}$ respectively there exists a project
$\mathfrak{b}$ in $\mathbf{\sharp\psi(B)}$ such that
$\mathfrak{prom}\mathop{\mathopen{:}\mathclose{:}}(\mathfrak{a}\otimes\mathfrak{f})=\mathfrak{b}$.
We showed that for all $\mathfrak{g}\in\mathbf{\sharp{A}\odot\sharp(A\multimap
B)}$, one has
$\mathfrak{prom}\mathop{\mathopen{:}\mathclose{:}}\mathfrak{g}\in\mathbf{\oc
B}$, and thus $\mathfrak{prom}$ is an element in $(\sharp
A\odot\sharp(A\multimap B))^{\simbot\simbot}\multimap\mathbf{B}$ by Section
3.3. But $(\sharp A\odot\sharp(A\multimap B))^{\simbot\simbot}=\mathbf{\oc
A\otimes\oc(A\multimap B)}$ by Section 2.2. ∎

$\oc\phi(A)$$\phi(V^{A})\times[0,1]$$\oc F$$\oc V^{A}$$\oc V^{B}$$(V^{A}\cup
V^{B})\times[0,1]$$\oc\psi(B)$$\psi(V^{B})\times[0,1]$$\Omega$$\Omega$$\Omega$$\text{Id}\times
T_{\tau}$$\text{Id}\times T_{\theta}$ (a) Global Picture

$\phi(V^{A})\times D^{A}$$\phi(V^{A})\times
D^{A}$$\phi(V^{A})\times[0,1]$$\phi(V^{A})\times[0,1]$$\mathcal{P}_{D^{A}}$$\mathcal{P}_{\\{0\\}+D^{A}}$$\text{Id}\times
T_{\tau}$$\text{Id}\times\tau$ (b) Action of $T_{\tau}$

$\psi(V^{B})\times D^{F}\times
D^{A}$$\psi(V^{B})\times\theta(D^{F}+D^{A})$$\phi(V^{A})\times[0,1]$$\phi(V^{A})\times[0,1]$$\mathcal{P}_{D^{F}+D^{A}}$$\mathcal{P}_{\theta(D^{F}+D^{A})}$$\text{Id}\times
T_{\theta}$$\text{Id}\times\theta$ (c) Action of $T_{\theta}$

Figure 18: Functorial Promotion

In the setting of its hyperfinite geometry of interaction [Gir11], Girard
shows how one can obtain the exponentials isomorphism as an equality between
the conducts $\oc(\mathbf{A\with B})$ and $\mathbf{\oc A\otimes\oc B}$. Things
are however quite different here. Indeed, if the introduction of behaviors in
place of Girard’s negative/positive conducts is very interesting when one is
interested in the additive connectives, this leads to a (small) complication
when dealing with exponentials. The first thing to notice is that the proof of
the implication $\oc A\otimes\oc B\multimap\oc(A\with B)$ in a sequent
calculus with functorial promotion and without dereliction and digging rules
cannot be written if the weakening rule is restrained to the formulas of the
form $\wn A$:

ax $\vdash A,A^{\simbot}$ weak $\vdash A,B^{\simbot},A^{\simbot}$ ax $\vdash
B,B^{\simbot}$ weak $\vdash B,B^{\simbot},A^{\simbot}$ $\with$ $\vdash
B^{\simbot},A^{\simbot},A\with B$ $\oc$ $\vdash\wn B^{\simbot},\wn
A^{\simbot},\oc(A\with B)$ $\vdash\oc A\otimes\oc B\multimap\oc(A\with B)$

In Girard’s setting, weakening is available for all positive conducts (the
conducts on which one can apply the $\wn$ modality), something which is
coherent with the fact that the inclusion $\mathbf{\oc A\otimes\oc
B\subset\oc(A\with B)}$ is satisfied. In our setting, however, weakening is
never available for behaviors and we think the latter inclusion is therefore
not satisfied. This question stays however open.

Concerning the converse inclusion, it does not seem clear at first that it is
satisfied in our setting either. This issue comes from the contraction rule.
Indeed, since the latter does not seem to be satisfied in full generality (see
Section 5.1), one could think the inclusion $\mathbf{\oc(A\with B)\subset\oc
A\otimes\oc B}$ is not satisfied either. We will show however in Section 6,
through the introduction of alternative ”additive connectives”, that it does
hold (a result that will not be used until the last section).

######  Proposition .

The conduct $\mathbf{1}$ is a perennial conduct, equal to $\oc\mathbf{T}$.

###### Proof.

By definition, $\mathbf{1}=\\{(0,\emptyset)\\}^{\simbot\simbot}$ is a
perennial conduct. Moreover, the balanced projects in $\mathbf{T}$ are the
projects of the shape $\mathfrak{t}_{D}=(0,\emptyset)$ with dialects
$D\subset\mathbf{N}$. Each of these satisfy
$\oc\mathfrak{t}_{D}=(0,\emptyset)$. Thus
$\sharp\mathbf{T}=\\{(0,\emptyset)\\}$ and $\mathbf{\oc T}=\mathbf{1}$. ∎

######  Corollary .

The conduct $\mathbf{\bot}$ is a co-perennial conduct, equal to
$\wn\mathbf{0}$.

###### Proof.

This is straightforward:

$\mathbf{\bot}=\mathbf{1}^{\simbot}=\mathbf{(\oc T)^{\simbot}}=\mathbf{(\sharp
T)^{\simbot\simbot\simbot}}=\mathbf{(\sharp T)^{\simbot}}=\mathbf{(\sharp
0^{\simbot})^{\simbot}}=\mathbf{\wn 0}$

∎

##  5 Soundness for Behaviors

###  5.1 Sequent Calculus

To deal with the three kinds of conducts we are working with (behaviors,
perennial and co-perennial conducts), we introduce three types of formulas.

######  Definition .

We define three types of formulas, (B)ehaviors, (N)egative — perennial, and
(P)ositive — co-perennial, inductively defined by the following grammar:

$\displaystyle B$ $\displaystyle:=$
$\displaystyle\mathbf{T}\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathbf{0}\leavevmode\nobreak\ |\leavevmode\nobreak\ X\leavevmode\nobreak\
|\leavevmode\nobreak\ X^{\simbot}\leavevmode\nobreak\ |\leavevmode\nobreak\
B\otimes B\leavevmode\nobreak\ |\leavevmode\nobreak\ B\parr
B\leavevmode\nobreak\ |\leavevmode\nobreak\ B\oplus B\leavevmode\nobreak\
|\leavevmode\nobreak\ B\with B\leavevmode\nobreak\ |\leavevmode\nobreak\
\forall X\leavevmode\nobreak\ B\leavevmode\nobreak\ |\leavevmode\nobreak\
\exists X\leavevmode\nobreak\ B\leavevmode\nobreak\ |\leavevmode\nobreak\
N\otimes B\leavevmode\nobreak\ |\leavevmode\nobreak\ P\parr B$ $\displaystyle
N$ $\displaystyle:=$ $\displaystyle\mathbf{1}\leavevmode\nobreak\
|\leavevmode\nobreak\ P^{\simbot}\leavevmode\nobreak\ |\leavevmode\nobreak\
\oc B\leavevmode\nobreak\ |\leavevmode\nobreak\ N\otimes N\leavevmode\nobreak\
|\leavevmode\nobreak\ N\oplus N$ $\displaystyle P$ $\displaystyle:=$
$\displaystyle\mathbf{\bot}\leavevmode\nobreak\ |\leavevmode\nobreak\
N^{\simbot}\leavevmode\nobreak\ |\leavevmode\nobreak\ \wn
B\leavevmode\nobreak\ |\leavevmode\nobreak\ P\parr P\leavevmode\nobreak\
|\leavevmode\nobreak\ P\with P$

We will denote by $\tt FV\rm(\Gamma)$ the set of free variables in $\Gamma$,
where $\Gamma$ is a sequence of formulas (of any type).

######  Definition .

We define _pre-sequents_ $\Delta\Vvdash\Gamma;\Theta$ where $\Delta,\Theta$
contain negative (perennial) formulas, $\Theta$ containing at most one
formula, and $\Gamma$ contains only behaviors.

Section 3.3 supposes that we are working with behaviors, and cannot be used to
interpret contraction in full generality. It is however possible to show in a
similar way that contraction can be interpreted when the sequent contains at
least one behavior (this is the next proposition). This restriction of the
context is necessary: without behaviors in the sequent one cannot interpret
the contraction since the inflation property is essential for showing that
$(1/2)\phi(\oc\mathfrak{a})\otimes\psi(\oc\mathfrak{a})+(1/2)\mathfrak{0}$ is
an element of $\mathbf{\phi(\oc A)\otimes\psi(\oc A)}$.

######  Proposition .

Let $\mathbf{A}$ be a conduct and $\phi,\psi$ be disjoint delocations of $\oc
V^{A}$. Let $\mathbf{C}$ be a behavior and $\theta$ a delocation disjoint from
$\phi$ and $\psi$. Then the project $\mathfrak{Ctr}_{\phi\cup\theta}^{\psi}$
is an element of the behavior:

$\mathbf{(\oc A\otimes C)\multimap(\phi(\oc A)\otimes\psi(\oc
A)\otimes\theta(C))}$

###### Proof.

The proof follows the proof of Section 3.3. We show in a similar manner that
the project
$\mathfrak{Ctr}_{\phi\cup\theta}^{\psi}\mathop{\mathopen{:}\mathclose{:}}(\mathfrak{a\otimes
c})$ is universally equivalent to:

$\frac{1}{2}\phi(\oc\mathfrak{a})\otimes\psi(\oc\mathfrak{a})\otimes\theta(\mathbf{C})+\frac{1}{2}\mathfrak{0}$

Since $\mathbf{\oc A}$ is a perennial conduct and $\mathbf{C}$ is a behavior,
$\mathbf{(\phi(\oc A)\otimes\psi(\oc A)\otimes\theta(C))}$ is a behavior. Thus
$\mathfrak{Ctr}_{\phi\cup\theta}^{\psi}\mathop{\mathopen{:}\mathclose{:}}(\mathfrak{a\otimes
c})$ is an element in $\mathbf{(\phi(\oc A)\otimes\psi(\oc
A)\otimes\theta(C))}$. Finally we showed that the project
$\mathfrak{Ctr}_{\phi\cup\theta}^{\psi}$ is an element of $\mathbf{(\oc
A\otimes C)\multimap(\phi(\oc A)\otimes\psi(\oc A)\otimes\theta(C))}$, and
that the latter is a behavior. ∎

In a similar way, the proof of distributivity relies on the property that
$\mathbf{A+B}\subset\mathbf{A\with B}$ which is satisfied for behaviors but
not in general. It is therefore necessary to restrict to pre-sequents that
contain at least one behavior in order to interpret the $\with$ rule. Indeed,
we can think of a pre-sequent $\Delta\Vvdash\Gamma;\Theta$ as the
conduct131313This will actually be the exact definition of its interpretation.

$\left(\bigparr_{N\in\Delta}N^{\simbot}\right)\parr\left(\bigparr_{B\in\Gamma}B\right)\parr\left(\bigparr_{N\in\Theta}N\right)$

Such a conduct is a behavior when the set $\Gamma$ is non-empty and the set
$\Theta$ is empty, but it is neither a perennial conduct nor a co-perennial
conduct when $\Gamma=\emptyset$. We will therefore restrict to pre-sequents
such that $\Gamma\neq\emptyset$ and $\Theta=\emptyset$.

######  Definition  (Sequents).

A sequent $\Delta\vdash\Gamma;$ is a pre-sequent $\Delta\Vvdash\Gamma;\Theta$
such that $\Gamma$ is non-empty and $\Theta$ is empty.

######  Definition  (The Sequent Calculus
$\textnormal{ELL}_{\textnormal{comp}}$).

A proof in the sequent calculus $\textnormal{ELL}_{\textnormal{comp}}$ is a
derivation tree constructed from the derivation rules shown in Figure 19 page
19.

ax $\vdash C^{\simbot},C;$ $\Delta_{1}\vdash\Gamma_{1},C;$
$\Delta_{2}\vdash\Gamma_{2},C^{\simbot};$ cut
$\Delta_{1},\Delta_{2}\vdash\Gamma_{1},\Gamma_{2};$

(a) Identity Group

$\Delta_{1}\vdash\Gamma_{1},C_{1};$ $\Delta_{2}\vdash\Gamma_{2},C_{2};$
$\otimes$ $\Delta_{1},\Delta_{2}\vdash\Gamma_{1},\Gamma_{2},C_{1}\otimes
C_{2};$ $\Delta\vdash\Gamma,C_{1},C_{2};$ $\parr$
$\Delta\vdash\Gamma,C_{1}\parr C_{2};$ $\Delta,N_{1},N_{2}\vdash\Gamma;$
$\otimes^{pol}_{g}$ $\Delta,N_{1}\otimes N_{2}\vdash\Gamma;$
$\Delta,P^{\simbot}\vdash\Gamma,C;$ $\parr^{mix}$ $\Delta\vdash\Gamma,P\parr
C;$ $\Delta\vdash\Gamma,C;$ $\mathbf{1}_{d}$
$\Delta\vdash\Gamma,C\otimes\mathbf{1};$ $\Delta\vdash\Gamma;$
$\mathbf{1}_{g}$ $\Delta,\mathbf{1}\vdash\Gamma;$

(b) Multiplicative Group

$\Delta\vdash\Gamma,C_{i};$ $\oplus_{i}$ $\Delta\vdash\Gamma,C_{1}\oplus
C_{2};$ $\Delta\vdash\Gamma,C_{1};$ $\Delta\vdash\Gamma,C_{2};$ $\with$
$\Delta\vdash\Gamma,C_{1}\with C_{2};$ $\top$ $\Delta\vdash\Gamma,\top;$ No
rules for $0$.

(c) Additive Group

$\Delta_{1}\vdash\Gamma_{1},C_{1};$ $\Delta_{2}\vdash\Gamma_{2},C_{2};$ $\oc$
$\oc\Delta_{1},\Delta_{2},\oc\Gamma_{1}^{\simbot}\vdash\Gamma_{2},C_{1}\otimes\oc
C_{2};$ $\Delta,\oc A,\oc A\vdash\Gamma;$ ctr ($\Gamma\neq\emptyset$)
$\Delta,\oc A\vdash\Gamma;$ $\Delta\vdash\Gamma;$ weak $\Delta,N\vdash\Gamma;$

(d) Exponential Group

$\vdash\Gamma,C;$ $X\not\in\tt FV\rm(\Gamma)$ $\forall$ $\vdash\Gamma,\forall
X\leavevmode\nobreak\ C;$ $\vdash\Gamma,C[A/X];$ $\exists$
$\vdash\Gamma,\exists X\leavevmode\nobreak\ C;$

(e) Quantifier Group

Figure 19: Rules for the sequent calculus
$\textnormal{ELL}_{\textnormal{comp}}$

###  5.2 Truth

The notion of success is the natural generalization of the corresponding
notion on graphs [Sei12a, Sei14a]. The graphing of a successful project will
therefore be a disjoint union of ”transpositions”. Such a graphing can be
represented as a graph with a set of vertices that could be infinite, but
since we are working with equivalence classes of graphings one can always find
a simpler representation: a graphing with exactly two edges.

######  Definition .

A project $\mathfrak{a}=(a,A)$ is _successful_ when it is balanced, $a=0$ and
$A$ is a disjoint union of transpositions:

  * •

for all $e\in E^{A}$, $\omega^{A}_{e}=1$;

  * •

for all $e\in E^{A}$, $\exists e^{\ast}\in E^{A}$ such that
$\phi^{A}_{e^{\ast}}=(\phi_{e}^{A})^{-1}$ — in particular
$S_{e}^{A}=T_{e^{\ast}}^{A}$ and $T_{e}^{A}=S_{e^{\ast}}^{A}$;

  * •

for all $e,f\in E^{A}$ with $f\not\in\\{e,e^{\ast}\\}$, $S^{A}_{e}\cap
S^{A}_{f}$ and $T^{A}_{e}\cap T^{A}_{f}$ are of null measure;

A conduct $\mathbf{A}$ is _true_ when it contains a successful project.

The following results were shown in our previous paper [Sei14c]. They ensure
that the given definition of truth is coherent.

######  Proposition  (Consistency).

The conducts $\mathbf{A}$ and $\mathbf{A}^{\simbot}$ cannot be simultaneously
true.

###### Proof.

We suppose that $\mathfrak{a}=(0,A)$ and $\mathfrak{b}=(0,B)$ are successful
project in the conducts $\mathbf{A}$ and $\mathbf{A}^{\simbot}$ respectively.
Then:

$\mathopen{\ll}\mathfrak{a},\mathfrak{b}\mathclose{\gg}_{m}=\mathopen{\llbracket}A,B\mathclose{\rrbracket}_{m}$

If there exists a cycle whose support is of strictly positive measure between
$A$ and $B$, then $\mathopen{\llbracket}A,B\mathclose{\rrbracket}_{m}=\infty$.
Otherwise, $\mathopen{\llbracket}A,B\mathclose{\rrbracket}_{m}=0$. In both
cases we obtained a contradiction since $\mathfrak{a}$ and $\mathfrak{b}$
cannot be orthogonal. ∎

######  Proposition  (Compositionnality).

If $\mathbf{A}$ and $\mathbf{A\multimap B}$ are true, then $\mathbf{B}$ is
true.

###### Proof.

Let $\mathfrak{a}\in\mathbf{A}$ and $\mathfrak{f}\in\mathbf{A\multimap B}$ be
successful projects. Then:

  * •

If $\mathopen{\ll}\mathfrak{a},\mathfrak{f}\mathclose{\gg}_{m}=\infty$, the
conduct $\mathbf{B}$ is equal to $\mathbf{T}_{V^{B}}$, which is a true conduct
since it contains $(0,\emptyset)$;

  * •

Otherwise $\mathopen{\ll}\mathfrak{a},\mathfrak{f}\mathclose{\gg}_{m}=0$ (this
is shown in the same manner as in the preceding proof) and it is sufficient to
show that $F\mathop{\mathopen{:}\mathclose{:}}A$ is a disjoint union of
transpositions. But this is straightforward: to each path there corresponds an
opposite path and the weights of the paths are all equal to $1$, the
conditions on the source and target sets $S_{\pi}$ and $T_{\pi}$ are then
easily checked.

Finally, if $\mathbf{A}$ and $\mathbf{A\multimap B}$ are true, then
$\mathbf{B}$ is true. ∎

###  5.3 Interpretation of proofs

To prove soundness, we will follow the proof technique used in our previous
papers [Sei12a, Sei14a, Sei14c]. We will first define a localized sequent
calculus and show a result of full soundness for it. The soundness result for
the non-localized calculus is then obtained by noticing that one can always
_localize_ a derivation. We will consider here that the variables are defined
with the carrier equal to an interval in $\mathbf{R}$ of the form $[i,i+1[$.

######  Definition .

We fix a set $\mathcal{V}=\\{X_{i}(j)\\}_{i,j\in\mathbf{N}\times\mathbf{Z}}$
of _localized variables_. For $i\in\mathbf{N}$, the set
$X_{i}=\\{X_{i}(j)\\}_{j\in\mathbf{Z}}$ will be called the _variable name
$X_{i}$_, and an element of $X_{i}$ will be called a _variable of name
$X_{i}$_.

For $i,j\in\mathbf{N}\times\mathbf{Z}$ we define the _location_ $\sharp
X_{i}(j)$ of the variable $X_{i}(j)$ as the set

$\\{x\in\mathbf{R}\leavevmode\nobreak\ |\leavevmode\nobreak\
2^{i}(2j+1)\leqslant m<2^{i}(2j+1)+1\\}$

######  Definition  (Formulas of $\textnormal{locELL}_{\textnormal{comp}}$).

We inductively define the formulas of _localized polarized elementary linear
logic_ $\textnormal{locELL}_{\textnormal{comp}}$ as well as their _locations_
as follows:

  * •

Behaviors:

    * –

A variable $X_{i}(j)$ of name $X_{i}$ is a behavior whose location is defined
as $\sharp X_{i}(j)$;

    * –

If $X_{i}(j)$ is a variable of name $X_{i}$, then $(X_{i}(j))^{\simbot}$ is a
behavior whose location is $\sharp X_{i}(j)$.

    * –

The constants $\mathbf{T}_{\sharp\Gamma}$ are behaviors whose location is
defined as $\sharp\Gamma$;

    * –

The constants $\mathbf{0}_{\sharp\Gamma}$ are behaviors whose location is
defined as $\sharp\Gamma$.

    * –

If $A,B$ are behaviors with respective locations $X,Y$ such that $X\cap
Y=\emptyset$, then $A\otimes B$ (resp. $A\parr B$, resp. $A\with B$, resp.
$A\oplus B$) is a behavior whose location is $X\cup Y$;

    * –

If $X_{i}$ is a variable name, and $A(X_{i})$ is a behavior of location
$\sharp A$, then $\forall X_{i}\leavevmode\nobreak\ A(X_{i})$ and $\exists
X_{i}\leavevmode\nobreak\ A(X_{i})$ are behaviors of location $\sharp A$.

    * –

If $A$ is a perennial conduct with location $X$ and $B$ is a behavior whose
location is $Y$ such that $X\cap Y=\emptyset$, then $A\otimes B$ is a behavior
with location $X\cup Y$;

    * –

If $A$ is a co-perennial conduct whose location is $X$ and $B$ is a behavior
with location $Y$ such that $X\cap Y=\emptyset$, then $A\parr B$ is a behavior
and its location is $X\cup Y$;

  * •

Perennial conducts:

    * –

The constant $\mathbf{1}$ is a perennial conduct and its location is
$\emptyset$;

    * –

If $A$ is a behavior or a perennial conduct and its location is $X$, then $\oc
A$ is a perennial conduct and its location is $\Omega(X\times[0,1])$;

    * –

If $A,B$ are perennial conducts with respective locations $X,Y$ such that
$X\cap Y=\emptyset$, then $A\otimes B$ (resp. $A\oplus B$) is a perennial
conduct whose location is $X\cup Y$;

  * •

Co-perennial conducts:

    * –

The constant $\mathbf{\bot}$ is a co-perennial conduct;

    * –

If $A$ is a behavior or a co-perennial conduct and its location is $X$, then
$\wn A$ is a co-perennial conduct whose location is $\Omega(X\times[0,1])$;

    * –

If $A,B$ are co-perennial conducts with respective locations $X,Y$ such that
$X\cap Y=\emptyset$, then $A\parr B$ (resp. $A\with B$) is a co-perennial
conduct whose location is $X\cup Y$;

If $A$ is a formula, we will denote by $\sharp A$ the location of $A$. A
sequent $\Delta\vdash\Gamma;$ of $\textnormal{locELL}_{\textnormal{comp}}$
must satisfy the following conditions:

  * •

the formulas of $\Gamma\cup\Delta$ have pairwise disjoint locations;

  * •

the formulas of $\Delta$ are all perennial conducts;

  * •

$\Gamma$ is non-empty and contains only behaviors.

######  Definition  (Interpretations).

An _interpretation basis_ is a function $\Phi$ which associates to each
variable name $X_{i}$ a behavior of carrier $[0,1[$.

######  Definition  (Interpretation of
$\textnormal{locELL}_{\textnormal{comp}}$ formulas).

Let $\Phi$ be an interpretation basis. We define the interpretation
$I_{\Phi}(F)$ along $\Phi$ of a formula $F$ inductively:

  * •

If $F=X_{i}(j)$, then $I_{\Phi}(F)$ is the delocation (i.e. a behavior) of
$\Phi(X_{i})$ defined by the function $x\mapsto 2^{i}(2j+1)+x$;

  * •

If $F=(X_{i}(j))^{\simbot}$, we define the behavior
$I_{\Phi}(F)=(I_{\Phi}(X_{i}(j)))^{\simbot}$;

  * •

If $F=\mathbf{T}_{\sharp\Gamma}$ (resp. $F=\mathbf{0}_{\sharp\Gamma}$), we
define $I_{\Phi}(F)$ as the behavior $\mathbf{T}_{\sharp\Gamma}$ (resp.
$\mathbf{0}_{\sharp\Gamma}$);

  * •

If $F=\mathbf{1}$ (resp. $F=\mathbf{\bot}$), we define $I_{\Phi}(F)$ as the
behavior $\mathbf{1}$ (resp. $\mathbf{\bot}$);

  * •

If $F=A\otimes B$, we define the conduct $I_{\Phi}(F)=I_{\Phi}(A)\otimes
I_{\Phi}(B)$;

  * •

If $F=A\parr B$, we define the conduct $I_{\Phi}(F)=I_{\Phi}(A)\parr
I_{\Phi}(B)$;

  * •

If $F=A\oplus B$, we define the conduct $I_{\Phi}(F)=I_{\Phi}(A)\oplus
I_{\Phi}(B)$;

  * •

If $F=A\with B$, we define the conduct $I_{\Phi}(F)=I_{\Phi}(A)\with
I_{\Phi}(B)$;

  * •

If $F=\forall X_{i}A(X_{i})$, we define the conduct
$I_{\Phi}(F)=\mathbf{\forall X_{i}}I_{\Phi}(A(X_{i}))$;

  * •

If $F=\exists X_{i}A(X_{i})$, we define the conduct
$I_{\Phi}(F)=\mathbf{\exists X_{i}}I_{\Phi}(A(X_{i}))$.

  * •

If $F=\oc A$ (resp. $\wn A$), we define the conduct $I_{\Phi}(F)=\oc
I_{\Phi}(A)$ (resp. $\wn I_{\Phi}(A)$).

Moreover, a sequent $\Delta\vdash\Gamma;$ will be interpreted as the $\parr$
of formulas in $\Gamma$ and negations of formulas in $\Delta$, which will be
written $\bigparr\Delta^{\simbot}\parr\bigparr\Gamma$. This formulas can also
be written in the equivalent form $\bigotimes\Delta\multimap(\bigparr\Gamma)$.

######  Definition  (Interpretation of
$\textnormal{locELL}_{\textnormal{comp}}$ proofs).

Let $\Phi$ be an interpretation basis. We define the interpretation
$I_{\Phi}(\pi)$ — a project — of a proof $\pi$ inductively:

  * •

if $\pi$ is a single axiom rule introducing the sequent
$\vdash(X_{i}(j))^{\simbot},X_{i}(j^{\prime})$, we define $I_{\Phi}(\pi)$ as
the project $\mathfrak{Fax}$ defined by the translation $x\mapsto
2^{i}(2j^{\prime}-2j)+x$;

  * •

if $\pi$ is composed of a single rule $\mathbf{T}_{\sharp\Gamma}$, we define
$I_{\Phi}(\pi)=\mathfrak{0}_{\sharp\Gamma}$;

  * •

if $\pi$ is obtained from $\pi^{\prime}$ by using a $\parr$ rule, a