License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2018.15
URN: urn:nbn:de:0030-drops-96828
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9682/
Go to the corresponding LIPIcs Volume Portal

Chouquet, Jules ; Vaux Auclair, Lionel

An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets

pdf-format:
LIPIcs-CSL-2018-15.pdf (0.6 MB)

Abstract

We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose some constraint on switching paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction.
Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative exponential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfy our constraints.
In the present work, we stick to the unit-free and weakening-free fragment of linear logic, which is rich enough to showcase our techniques, while allowing for a very simple kind of constraint: a bound on the number of cuts that are crossed by any switching path.

BibTeX - Entry

@InProceedings{chouquet_et_al:LIPIcs:2018:9682,
  author =	{Jules Chouquet and Lionel Vaux Auclair},
  title =	{{An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic  (CSL 2018)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Dan Ghica and Achim Jung},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9682},
  URN =		{urn:nbn:de:0030-drops-96828},
  doi =		{10.4230/LIPIcs.CSL.2018.15},
  annote =	{Keywords: linear logic, proof nets, cut elimination, differential linear logic}
}

Keywords: linear logic, proof nets, cut elimination, differential linear logic
Collection: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
Issue Date: 2018
Date of publication: 29.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI