Document Open Access Logo

Partial Elements and Recursion via Dominances in Univalent Type Theory

Authors Martín H. Escardó, Cory M. Knapp

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.21.pdf
  • Filesize: 443 kB
  • 16 pages

Document Identifiers

Author Details

Martín H. Escardó
Cory M. Knapp

Cite As Get BibTex

Martín H. Escardó and Cory M. Knapp. Partial Elements and Recursion via Dominances in Univalent Type Theory. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CSL.2017.21

Abstract

We begin by revisiting partiality in univalent type theory via the notion of dominance. We then perform first steps in constructive computability theory, discussing the consequences of working with computability as property or structure, without assuming countable choice or Markov’s principle. A guiding question is what, if any, notion of partial function allows the proposition “all partial functions on natural numbers are Turing computable” to be consistent.

Subject Classification

Keywords
  • univalent type theory
  • homotopy type theory
  • partial function
  • dominance
  • recursion theory
  • computability theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. Google Scholar
  2. Andrej Bauer and Davorin Lešnik. Metric spaces in synthetic topology. Annals of Pure and Applied Logic, 163(2):87-100, 2012. Third Workshop on Formal Topology. URL: http://dx.doi.org/10.1016/j.apal.2011.06.017.
  3. Ana Bove. General Recursion in Type Theory, pages 39-58. Springer, 2003. Google Scholar
  4. Ana Bove and Venanzio Capretta. Nested General Recursion and Partiality in Type Theory, pages 121-125. Springer, 2001. Google Scholar
  5. Ana Bove and Venanzio Capretta. A Type of Partial Recursive Functions, pages 102-117. Springer, Berlin, Heidelberg, 2008. Google Scholar
  6. Douglas Bridges and Fred Richman. Varieties of constructive mathematics, volume 97 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1987. Google Scholar
  7. Venancio Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 15:1-28, 2005. Google Scholar
  8. James Chapman, Tarmo Uustalu, and Niccolò Veltri. Quotienting the Delay Monad by Weak Bisimilarity, pages 110-125. Springer, Cham, 2015. Google Scholar
  9. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. arXiv, November 2016. URL: https://arxiv.org/abs/1611.02108.
  10. Thierry Coquand, Bassel Mannaa, and Fabian Ruch. Stack semantics of type theory. arXiv, 2017. URL: https://arxiv.org/abs/1701.02571.
  11. J. Martin E. Hyland. The effective topos. Studies in Logic and the Foundations of Mathematics, 110:165-216, 1982. Google Scholar
  12. J. M. E. Hyland. First steps in synthetic domain theory, pages 131-156. Springer, 1991. Google Scholar
  13. S. Kleene. Introduction to Metamathematics, 1952. Google Scholar
  14. N. Kraus, M. H. Escardó, T. Coquand, and T. Altenkirch. Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science, 2017. Google Scholar
  15. Piergiorgio Odifreddi. Classical Recursion Theory. Elsevier, 1989. Google Scholar
  16. B. Reus and Th. Streicher. General synthetic domain theory - A logical approach (extended abstract), pages 293-313. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997. URL: http://dx.doi.org/10.1007/BFb0026995.
  17. Egbert Rijke. Homotopy type theory. Master’s thesis, Utrecht University, 2012. URL: https://hottheory.files.wordpress.com/2012/08/hott2.pdf.
  18. Egbert Rijke. The join contruction. arXiv:1701.07538, Jan 2017. URL: https://arxiv.org/abs/1701.07538.
  19. H. Rogers, Jr. Theory of Recursive Functions and Effective Computability. MIT Press, 1987. Google Scholar
  20. G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986. URL: ftp://ftp.disi.unige.it/person/RosoliniG/papers/coneit.ps.gz.
  21. Nils Anders Danielsson Thorsten Altenkirch and Nicolai Kraus. Partiality, revisited: The partiality monad as a quotient inductive-inductive type. In FoSSaCS Proceedings, 2017. Google Scholar
  22. A. S. Troelstra. A note on non-extensional operations in connection with continuity and recursiveness. Indag. Math., 39(5):455-462, 1977. Google Scholar
  23. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  24. Jaap van Oosten and Alex K. Simpson. Axioms and (counter)examples in synthetic domain theory. Annals of Pure and Applied Logic, 104(1):233-278, 2000. URL: http://dx.doi.org/10.1016/S0168-0072(00)00014-2.
  25. V. Voevodsky. Resizing rules. Invited talk at Types'2011, Bergen, September 2011. URL: http://www.math.ias.edu/vladimir/files/2011_Bergen.pdf.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact