Proof-Net as Graph, Taylor Expansion as Pullback

We introduce a new graphical representation for multiplicative and exponential linear logic proof-structures, based only on standard labelled oriented graphs and standard notions of graph theory. The inductive structure of boxes is handled by means of a box-tree. Our proof-structures are canonical and allows for an elegant definition of their Taylor expansion by means of pullbacks.

1. 1.

   The folklore attributes the definition of graphs with half-edges to Kontsevitch and Manin, but the idea can actually be traced back to Grothendieck’s dessins d’enfant.

2. 2.

   This implies that \(\mathsf {c}(i_j) = \mathsf {c}(i_k)\) for all \(1 \leqslant j,k \leqslant n\).

3. 3.

   The structured graph |R| of R is more structured (it is also labeled, colored, ordered) than an oriented graph such as \(\mathcal {A}^{\circlearrowleft }\). When we talk of a morphism between two structured graphs where one of the two, say \(\tau \), is less structured than the other, say \(\sigma \), we mean that \(\tau \) must be only considered with the same structure as \(\sigma \). Thus, in this case, \(\mathsf {box}\) is a morphism from \((||R ||, \mathsf {o}_{R})\)—discarding \(\mathsf {\ell }_{R}\), \(\mathsf {c}_{R}\), \(<_{R}\)—to \(\mathcal {A}^{\circlearrowleft }\).

4. 4.

   This means that for any input flag \(f'\) in \(\mathcal {A}\) there is exactly one input f of some vertex of type in |R| such that \(\mathsf {box}_F(f) = f'\); but \(\mathsf {box}_{F}(f)\) need not be an input flag in \(\mathcal {A}\) for any input f of some vertex of type in |R| (by definition of morphism, \(\mathsf {box}_{F}(f)\) is necessarily an input flag in \(\mathcal {A}^{\circlearrowleft }\)). Intuitively, a vertex v of type represents a generalized co-contraction (in particular, a co-weakening if it has no inputs), and a box is associated with (and only with) each input f of v such that \(\mathsf {box}_{F}(f)\) is an input flag in \(\mathcal {A}\) (and not only in \(\mathcal {A}^{\circlearrowleft }\)): f represents the principal door (in the border) of such a box (note that for \(f' \in F_{||R ||}\), if \(f' \ne f\) then \(\mathsf {box}_{F}(f') \ne \mathsf {box}_{F}(f)\) and that \(\mathsf {box}_V(\partial _{||R ||}\circ j_{||R ||}(f)) \ne \mathsf {box}_V(\partial _{||R ||}(f))\) for such a f).

5. 5.

   Roughly, it says that the border of a box is made of (inputs of) vertices of type or .

6. 6.

   According to the constraints on \(\mathsf {box}_{R}\), this condition can be fulfilled only by inputs of a cell of type (a -cell, for short) in |R|, and an input of a -cell need not fulfill it; in particular, if R is a \(\mathsf {ME}\mathsf {LL} \) proof-structure, then this condition is fulfilled by all and only the inputs of -cells (and such an input is unique for any -cell) in |R|; but if R is a \(\mathsf {Di}\mathsf {LL} _0\) proof-structure, then this condition is not fulfilled by any flag in |R| (since \(\mathcal {A}_{R}\) has no inputs) and so \(\mathsf {box}_{R}\) is a graph morphism associating the root of \(\mathcal {A}_{R}\) with any vertex of |R|. Therefore, in a \(\mathsf {Di}\mathsf {LL} _0\) proof-structure \(\rho = (|\rho |,\mathcal {A}_{\rho },\mathsf {box}_{\rho })\), \(\mathcal {A}_{\rho }\) and \(\mathsf {box}_{\rho }\) do not induce any structure on \(|\rho |\): \(\rho \) can be identified with \(|\rho |\).

7. 7.

   We write only the graph \(|R_\pi |\) of \(R_\pi \), because its box-tree \(\mathcal {A}_{R_\pi }\) and its box-function \(\mathsf {box}_{R_\pi }\) are trivial (see Footnote 6).

8. 8.

   This means that \(\tau _t^{\circlearrowleft }\) and \(\mathcal {A}_{R}^\circlearrowleft \) are considered as (unoriented) graphs, see also Footnote 3.

Authors and Affiliations

1. Department of Computer Science, University of Bath, Bath, UK

   Giulio Guerrieri

2. IRIF, Université Paris Diderot, Paris, France

   Luc Pellissier

3. Dipartimento di Matematica e Fisica, Università Roma Tre, Rome, Italy

   Lorenzo Tortora de Falco

Corresponding author

Correspondence to Luc Pellissier .

Editors and Affiliations

1. Department of Philosophy and Religious Studies, Utrecht University, Utrecht, The Netherlands

   Rosalie Iemhoff

2. Utrecht Institute of Linguistics OTS, Utrecht University, Utrecht, The Netherlands

   Michael Moortgat

3. Centro de Informática, Universidade Federal de Pernambuco (UFPE), Recife, Brazil

   Ruy de Queiroz

Technical Appendix

A Computing a Pullback in the Category of Graphs

The category of graphs has all pullbacks, a fact that we use extensively. We recall here all the definitions and facts that are packed in that affirmation.

Definition 11

(pullback). Let \(\mathcal {C}\) be a category. Let \(X\), \(Y\), and \(Z\) be three objects of \(\mathcal {C}\) and \(f:X\rightarrow Z\) and \(g:Y\rightarrow Z\) be two arrows of \(\mathcal {C}\).

The pullback of \(X\) and \(Y\) along \(f\) and \(g\) is the triple such that the diagram

commutes and, for every other \((B,h : B \rightarrow X,k : B \rightarrow Y)\) making the same diagram commute, there exists a unique arrow \(p:B \rightarrow A\) such that:

It is unique (up to unique isomorphism), and it is customary to write \(X \times _{Z} Y\) a pullback of \(X\) and \(Y\) over \(Z\) (leaving \(f\) and \(g\) implicit) and a pullback diagram with a corner:

All pullbacks exist in the category of graphs. Explicitely, let \(\tau = (F_{\tau }, V_{\tau }, \partial _{\tau }, j_{\tau })\), \(\sigma = (F_{\sigma }, V_{\sigma }, \partial _{\sigma }, j_{\sigma })\) and \(\rho = (F_{\rho }, V_{\rho }, \partial _{\rho }, j_{\rho })\) be three graphs and \(g: \sigma \rightarrow \tau \), \(h : \rho \rightarrow \tau \) be two graph morphisms. Consider the two sets

They are both equiped with two projections, which we will write \(\pi _{\sigma }^F, \pi _{\rho }^F, \pi _{\sigma }^V, \pi _{\rho }^V\). Let \(f\in F\).

Hence, we can define \(\partial : F \rightarrow V\) by \(\partial (f) = (\partial _{\sigma }\circ \pi _{\sigma }^F (f), \partial _{\rho } \circ \pi _{\rho }^F(f)) \). In the same way, we define \(j : F \rightarrow F\) by \(j(f) = (j_{\sigma } \circ \pi _{\sigma }^F(f), j_{\rho } \circ \pi _{\rho }^F(f))\), and check that it is an involution.

Hence \(\sigma \times _{\tau } \rho = (F,V,\partial ,j)\) is a graph and \(\pi _{\sigma } = (\pi _{\sigma }^F, \pi _{\sigma }^V) : \sigma \times _{\tau } \rho \rightarrow \sigma \) and \(\pi _{\rho } = (\pi _{\rho }^F, \pi _{\rho }^V) : \sigma \times _{\tau } \rho \rightarrow \rho \) are graph morphisms.

Consider now any \(\mu = (F_{\mu },V_{\mu },\partial _{\mu },j_{\mu })\) such that the diagram

commutes. For \(f\in F_{\mu }\), let \(r_F(f) = (p_F(f),q_F(f))\) and for \(v\in V_{\mu }\), let \(r_V(v) = (p_V(v),q_V(v))\). We check that it defines a graph morphism \(r:\mu \rightarrow \sigma \times _{\tau } \rho \) and it factorises \(p\) and \(q\).

Reprints and permissions

© 2019 Springer-Verlag GmbH Germany, part of Springer Nature

Policies and ethics