Building a (sort of) GoI
from denotational semantics:
an improvisation
Damiano Mazza
Laboratoire d’Informatique de Paris Nord
CNRS – Université Paris 13
Workshop on Geometry of Interaction,
Traced Monoidal Categories,
and Implicit Complexity,
Kyoto, 26 August 2009

Denotational semantics vs. GoI
In synthesis:• denotational semantics is cut-as-composition;• the geometry of interaction is cut-as-trace.
We know how to go from the GoI view to the denotational semantics view:
we use the Int construction.
The question we address here is: can we go the other way?
In other words, can we build a “cut-as-trace” interpretation of proofs
starting from a more traditional, “cut-as-composition” interpretation?
One possible motivation: fix the mismatch between GoI execution andsyntactical cut-elimination.
1

Previous work
We have illustrious predecessors: Abramsky and Jagadeesan followed asimilar path in their “New Foundations” paper (1993).
Some comparison:• Motivations and rationale: very similar.
• Methodology: quite different.
• Results: there is arguably some overlap, but also some importantdifferences. . . ? (To be honest, I don’t know exactly.)2

Some background ideas• Denotational semantics:– proofs are vectors;– a proof of A⊥, B is a vector of A∗ ⊗ B, i.e., a matrix;– cut is composition, i.e., matrix product.
• GoI:– proofs are operators;– a proof of A⊥, B is a linear operator on A∗ ⊗ B;
– composition is trace.
• The two should be related in a “nice” way, e.g., the denotationalsemantics should appear as a sum of eigenvectors of the GoI operator(an extension of Regnier’s conjecture).
3

Back to reality
It’s going to be tough to make it work:• negation must be involutive;• at the same time, the exponential modalities force considering infinitedimensional vector spaces;• consequence: topological vector spaces are needed.
• That is far from trivial (Ehrhard 2005).
• Additional problem: the category is ∗-autonomous, not compact closed:
what is the trace?
4

A low-profile setting
The category Rel of sets and relations.
• It hosts a model of linear logic: tensor is Cartesian product (nota categorical product in Rel), the comonad is given by the freecommutative monoid construction (finite multisets), negation is identity.
• A set X can be seen as the basis of a “free” vector space over. . .
something which is not a field (or even a ring), but never mind. In fact,(℘(X), ∪, ∅) is a monoid (that’s close enough to a vector space. . . ).
• Given another set Y , it makes sense to define ℘(X) ⊗ ℘(Y ) ∼= ℘(X × Y ),and a monoid endomorphism can play the role of linear operators.
• Rel also hosts a model of differential interaction nets, which will turnout to be useful. . .
5

The Lafont double cover of a net• A standard construction in topology (the orientable double cover of anon-orientable surface), specialized to a standard construction on graphs,
the bipartite double cover of an undirected graph G, defined as G × K2.
• Applied for the first time by Lafont (1995) to nets of interaction
combinators. We denote it by (·)±.
• It is the essence of the GoI!
• In the multiplicative case, it is easy; in the exponential case, one must
define the Lafont double cover of a box. Girard’s proposal unfortunately
does not work perfectly.

6Differential interaction nets and the Taylor expansion• Twenty years after Girard’s first proposal, and sixteen years after
Abramsky and Jagadeesan work, we have “much newer foundations”:
differential interaction nets (Ehrhard-Regnier 2006).
• Exponential boxes of linear logic proof nets can be expressed in differential
interaction nets by means of the Taylor-Ehrhard expansion, denoted by
T (·).
• In fact, differential interaction nets are an extremely useful bridge between
syntax and denotational semantics.
• (Technical note: in what follows, to avoid treading on dangerous soil, we
drop additive connectives, and we consider only atomic axioms.)
7

Entanglement• Defining the Lafont double cover α± of a differential interaction net α istrivial. Then, given a proof net π of conclusions A1, . . . , An, we have
JT (π)±K ⊆ (A1 × · · · × An) × (A1 × · · · × An),
where J·K denotes interpretation in Rel. This is precisely a monoid
endomorphism (i.e., an “operator”) of ℘(A1) ⊗ · · · ⊗ ℘(An). Perfect!
• Actually, not so perfect. . . It is easy to see that this is too naive, it
won’t model cut-elimination: “wrong” nets emerge in the simulation.
• Intriguingly, the solution requires handling a phenomen of entanglement.
To deal with it, we formally do just as in quantum mechanics (the mathis morally the same).
8Entangled experiments• Experiments are an extremely useful tool for concretely computing theinterpretation of a proof net in “webbed” models (like Rel).
• Let α be a differential interaction net. Given a port p of α±, we canalways define its twin p.
• An experiment e of α± is strongly entangled iff, for all ports p, q of α±,e(p) = e(q) implies e(p) = e(q).
Lemma 1. An experiment is strongly entangled iff the above condition isverified by all atomic ports of α±.
• If an experiment satisfies the above condition only on the premises ofexponential cells, we call it weakly entangled, or simply entangled.
9The GoI interpretation• If α is a differential interaction net, we denote by Lα±M (resp. Lα±Ms) theset of the results of all entangled (resp. strongly entangled) experiments
on α±.
• We denote by α• the “cut-free” version of α. We define the GoI
interpretation of a proof net π as[[±Lα• M(and GoIsπ =Lα•±Ms).
GoI π =α∈T (π)α∈T (π)• Cut-elimination is modeled by the usual trace in Rel. In particular,
thanks to the definition of experiment, we have
S±Lemma 2. Tr(GoI α) = Lα M, and hence Tr(GoI π) = α∈T (π)Lα±M.
10Soundness• We have the following fundamental result:Lemma 3. α → β implies Lα±M = Lβ ±M.
• Then, thanks to the soundness of the Taylor-Ehrhard expansion (i.e.,π → π 0 implies T (π) →∗ T (π 0)), and to Lemma 2 and Lemma 3, wehave
Theorem 4. [Soundness] π → π 0 implies Tr(GoI π) = Tr(GoI π 0).
• Note that, just like in “New Foundations” GoI, there is no restriction on
the validity of soundness.
• All of the above also hold when we replace entangled semantics withstrongly entangled semantics.
11Retrieving denotational semantics?
Remember that denotational semantics should appear as a sort of “sum ofeigenvectors”. This is the closest approximation we get in our framework:
Lemma 5. Let α be a cut-free differential interaction net. Then,GoIsα(JαK) = JαK.
(Probably JαK is the biggest set with such property, we don’t know. . . ).
If α1, α2 are different summands of the Taylor-Ehrhard expansion of acut-free proof net π of conclusion A, then GoIsα1 and GoIsα2 should have“disjoint domains”, i.e., there exist disjoint subsets A1, A2 of A such thatthe only sets not in the “kernel” of GoIsαi are included in Ai.
SThen, the union α∈T (π) GoIsα is actually a “direct sum”, which should
be enough to guarantee the following
Conjecture 6. Let π be a proof net. Then, GoIsπ(JπK) = JπK.
12

To do. . .
• Strong entanglement is. . . too strong. Fortunately, weak entanglement
is enough for soundness; we keep hoping that it is also enough to get
Conjecture 6.
• Speaking of Conjecture 6, note that this fails in general: if α, β are
arbitray differential interaction nets, Jα + βK = JαK ∪ JβK will not ingeneral be a fixpoint of GoIsα ∪ GoIsβ. This suggests that there
are perhaps two sums/unions of nets: one “uniform”, and one “nonuniform”, maybe in analogy with pure states and mixed-states?
• What about paths?
Clearly this is not “particle-style” GoI, butmaybe “wave-style”, or better, particles moving according to quantum
mechanical “trajectories”?
• This is a bit ad hoc. Can one find a more abstract formulation?
13