System T and the Product of Selection Functions

Authors Martin Escardo, Paulo Oliva, Thomas Powell



PDF
Thumbnail PDF

File

LIPIcs.CSL.2011.233.pdf
  • Filesize: 0.53 MB
  • 15 pages

Document Identifiers

Author Details

Martin Escardo
Paulo Oliva
Thomas Powell

Cite AsGet BibTex

Martin Escardo, Paulo Oliva, and Thomas Powell. System T and the Product of Selection Functions. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 233-247, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
https://doi.org/10.4230/LIPIcs.CSL.2011.233

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.
Keywords
  • primitive recursion
  • product of selection functions
  • finite choice
  • dialectica interpretation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail