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.2017.23
URN: urn:nbn:de:0030-drops-77040
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7704/
Go to the corresponding LIPIcs Volume Portal

Gérard, Ulysse ; Miller, Dale

Separating Functional Computation from Relations

pdf-format:
LIPIcs-CSL-2017-23.pdf (0.5 MB)

Abstract

The logical foundation of arithmetic generally starts with a
quantificational logic over relations. Of course, one often wishes to have a formal treatment of functions within this setting. Both
Hilbert and Church added choice operators (such as the epsilon
operator) to logic in order to coerce relations that happen to encode functions into actual functions. Others have extended the term language with confluent term rewriting in order to encode functional computation as rewriting to a normal form. We take a different approach that does not extend the underlying logic with either choice principles or with an equality theory. Instead, we use the familiar two-phase construction of focused proofs and capture functional computation entirely within one of these phases. As a result, our logic remains purely relational even when it is computing functions.

BibTeX - Entry

@InProceedings{grard_et_al:LIPIcs:2017:7704,
  author =	{Ulysse G{\'e}rard and Dale Miller},
  title =	{{Separating Functional Computation from Relations}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Valentin Goranko and Mads Dam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7704},
  URN =		{urn:nbn:de:0030-drops-77040},
  doi =		{10.4230/LIPIcs.CSL.2017.23},
  annote =	{Keywords: focused proof systems, fixed points, computation and deduction}
}

Keywords: focused proof systems, fixed points, computation and deduction
Collection: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Issue Date: 2017
Date of publication: 16.08.2017

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