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.2016.40
URN: urn:nbn:de:0030-drops-65807
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6580/
Go to the corresponding LIPIcs Volume Portal

Baillot, Patrick ; Das, Anupam

Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic

pdf-format:
LIPIcs-CSL-2016-40.pdf (0.6 MB)

Abstract

We prove a general form of 'free-cut elimination' for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing theorem for a fragment of this arithmetic via the `witness function method', showing that the provably convergent functions are precisely the polynomial-time functions. The programs extracted are implemented in the framework of 'safe' recursive functions, due to Bellantoni and Cook, where the ! modality of linear logic corresponds to normal inputs of a safe recursive program.

BibTeX - Entry

@InProceedings{baillot_et_al:LIPIcs:2016:6580,
  author =	{Patrick Baillot and Anupam Das},
  title =	{{Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{40:1--40:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Jean-Marc Talbot and Laurent Regnier},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6580},
  URN =		{urn:nbn:de:0030-drops-65807},
  doi =		{10.4230/LIPIcs.CSL.2016.40},
  annote =	{Keywords: proof theory, linear logic, bounded arithmetic, polynomial time computation, implicit computational complexity}
}

Keywords: proof theory, linear logic, bounded arithmetic, polynomial time computation, implicit computational complexity
Collection: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Issue Date: 2016
Date of publication: 29.08.2016

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