DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2013.248

Cuts for circular proofs: semantics and cut-elimination

Authors: Jérôme Fortier and Luigi Santocanale

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract

One of the authors introduced in [Santocanale, FoSSaCS, 2002] a calculus of circular proofs for studying the computability arising from the following categorical operations: finite products, finite coproducts, initial algebras, final coalgebras. The calculus presented [Santocanale, FoSSaCS, 2002] is cut-free; even if sound and complete for provability, it lacked an important property for the semantics of proofs, namely fullness w.r.t. the class of intended categorical models (called mu-bicomplete categories in [Santocanale, ITA, 2002]). In this paper we fix this problem by adding the cut rule to the calculus and by modifying accordingly the syntactical constraint ensuring soundness of proofs. The enhanced proof system fully represents arrows of the canonical model (a free mu-bicomplete category). We also describe a cut-elimination procedure as a a model of computation arising from the above mentioned categorical operations. The procedure constructs a cut-free proof-tree with possibly infinite branches out of a finite circular proof with cuts.

Cite as

Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 248-262, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fortier_et_al:LIPIcs.CSL.2013.248,
  author =	{Fortier, J\'{e}r\^{o}me and Santocanale, Luigi},
  title =	{{Cuts for circular proofs: semantics and cut-elimination}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{248--262},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.248},
  URN =		{urn:nbn:de:0030-drops-42019},
  doi =		{10.4230/LIPIcs.CSL.2013.248},
  annote =	{Keywords: categorical proof-theory, fixpoints, initial and final (co)algebras, inductive and coinductive types}
}

Search Results

Documents authored by Fortier, Jérôme

Cuts for circular proofs: semantics and cut-elimination

Abstract

Cite as

Thanks for your feedback!

Could not send message