License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2011.233
URN: urn:nbn:de:0030-drops-32341
URL: http://drops.dagstuhl.de/opus/volltexte/2011/3234/
Go to the corresponding LIPIcs Volume Portal


Escardo, Martin ; Oliva, Paulo ; Powell, Thomas

System T and the Product of Selection Functions

pdf-format:
Document 1.pdf (544 KB)


Abstract

We show that the finite product of selection functions (for all finite types) is primitive recursively equivalent to Goedel's higher-type recursor (for all finite types). The correspondence is shown to hold for similar restricted fragments of both systems: The recursor for type level n+1 is primitive recursively equivalent to the finite product of selection functions of type level n. Whereas the recursor directly interprets induction, we show that other classical arithmetical principles such as bounded collection and finite choice are more naturally interpreted via the product of selection functions.

BibTeX - Entry

@InProceedings{escardo_et_al:LIPIcs:2011:3234,
  author =	{Martin Escardo and Paulo Oliva and Thomas Powell},
  title =	{{System T and the Product of Selection Functions}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{233--247},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Marc Bezem},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3234},
  URN =		{urn:nbn:de:0030-drops-32341},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.CSL.2011.233},
  annote =	{Keywords: primitive recursion, product of selection functions, finite choice, dialectica interpretation}
}

Keywords: primitive recursion, product of selection functions, finite choice, dialectica interpretation
Seminar: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
Issue Date: 2011
Date of publication: 31.08.2011


DROPS-Home | Fulltext Search | Imprint Published by LZI