Document Open Access Logo

Domain Theory in Constructive and Predicative Univalent Foundations

Authors Tom de Jong , Martín Hötzel Escardó

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.28.pdf
  • Filesize: 0.57 MB
  • 18 pages

Document Identifiers

Author Details

Tom de Jong
  • University of Birmingham, UK
Martín Hötzel Escardó
  • University of Birmingham, UK

Cite AsGet BibTex

Tom de Jong and Martín Hötzel Escardó. Domain Theory in Constructive and Predicative Univalent Foundations. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.28

Abstract

We develop domain theory in constructive univalent foundations without Voevodsky’s resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and proved its computational adequacy, based on directed complete posets (dcpos). Here we further consider algebraic and continuous dcpos, and construct Scott’s D_∞ model of the untyped λ-calculus. A common approach to deal with size issues in a predicative foundation is to work with information systems or abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. Here we instead accept that dcpos may be large and work with type universes to account for this. For instance, in the Scott model of PCF, the dcpos have carriers in the second universe U₁ and suprema of directed families with indexing type in the first universe U₀. Seeing a poset as a category in the usual way, we can say that these dcpos are large, but locally small, and have small filtered colimits. In the case of algebraic dcpos, in order to deal with size issues, we proceed mimicking the definition of accessible category. With such a definition, our construction of Scott’s D_∞ again gives a large, locally small, algebraic dcpo with small directed suprema.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
Keywords
  • domain theory
  • constructivity
  • predicativity
  • univalent foundations

Metrics

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

Related Versions

References

  1. S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1-168. Clarendon Press, 1994. Google Scholar
  2. Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories, volume 189 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. URL: https://doi.org/10.1017/CBO9780511600579.
  3. Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9780511983504.
  4. Andrej Bauer and Iztok Kavkler. A constructive theory of continuous domains suitable for implementation. Annals of Pure and Applied Logic, 159(3):251-267, 2009. URL: https://doi.org/10.1016/j.apal.2008.09.025.
  5. Nick Benton, Andrew Kennedy, and Carsten Varming. Some domain theory and denotational semantics in Coq. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics (TPHOLs 2009), volume 5674 of Lecture Notes in Computer Science, pages 115-130. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_10.
  6. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  7. The Agda community. Agda wiki. URL: https://wiki.portal.chalmers.se/agda/pmwiki.php.
  8. Thierry Coquand, Simon Huber, and Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 255-264. Association for Computing Machinery, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  9. Thierry Coquand, Giovanni Sambin, Jan Smith, and Silvio Valentini. Inductively generated formal topologies. Annals of Pure and Applied Logic, 124(1-3):71-106, 2003. URL: https://doi.org/10.1016/s0168-0072(03)00052-6.
  10. Tom de Jong. The Scott model of PCF in univalent type theory, November 2019. URL: http://arxiv.org/abs/1904.09810.
  11. Tom de Jong. Domain theory in predicative Univalent Foundations. Abstract for a talk at HoTT/UF 2020 on 7 July, 2020. URL: https://hott-uf.github.io/2020/HoTTUF_2020_paper_14.pdf.
  12. Tom de Jong. Formalisation of domain theory in constructive and predicative univalent foundations. https://github.com/tomdjong/TypeTopology, June 2020. Agda development.
  13. Robert Dockins. Formalized, Effective Domain Theory in Coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving (ITP 2014), volume 8558 of Lecture Notes in Computer Science, pages 209-225. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_14.
  14. Martín H. Escardó. The proof of the interpolation property of the way-below relation of a continuous poset. 18 March, 2000. URL: https://www.cs.bham.ac.uk/~mhe/papers/interpolation.pdf.
  15. Martín H. Escardó and Cory M. Knapp. Partial Elements and Recursion via Dominances in Univalent Type Theory. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:16. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.21.
  16. Martín Hötzel Escardó. Introduction to Univalent Foundations of Mathematics with Agda, February 2020. URL: http://arxiv.org/abs/1911.00580.
  17. Martín Hötzel Escardó. Various new theorems in constructive univalent mathematics written in Agda. https://github.com/martinescardo/TypeTopology, June 2020. Agda development.
  18. G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2003. URL: https://doi.org/10.1017/CBO9780511542725.
  19. Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael W. Mislove, and Dana S. Scott. A Compendium of Continuous Lattices. Springer Berlin Heidelberg, 1980. URL: https://doi.org/10.1007/978-3-642-67678-9.
  20. Brendan Hart. Investigating Properties of PCF in Agda. MSci project, School of Computer Science, University of Birmingham, 2020. Report and Agda code available at URL: https://github.com/BrendanHart/Investigating-Properties-of-PCF.
  21. Michael Hedberg. A type-theoretic interpretation of constructive domain theory. Journal of Automated Reasoning, 16(3):369-425, 1996. URL: https://doi.org/10.1007/BF00252182.
  22. J. M. E. Hyland. First steps in synthetic domain theory. In A. Carboni, M. C. Peddicchio, and G. Rosolini, editors, Category Theory, volume 1488 of Lecture Notes in Mathematics, pages 131-156. Springer, 1991. URL: https://doi.org/10.1007/bfb0084217.
  23. Peter Johnstone and André Joyal. Continuous categories and exponentiable toposes. Journal of Pure and Applied Algebra, 25(3):255-296, 1982. URL: https://doi.org/10.1016/0022-4049(82)90083-4.
  24. Tatsuji Kawai. Predicative theories of continuous lattices, June 2020. URL: http://arxiv.org/abs/2006.05642.
  25. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of Anonymous Existence in Martin-Löf Type Theory. Logical Methods in Computer Science, 13(1), 2017. URL: https://doi.org/10.23638/LMCS-13(1:15)2017.
  26. David Lidell. Formalizing domain models of the typed and the untyped lambda calculus in Agda. Master’s thesis, Chalmers University of Technology and University of Gothenburg, 2020. Final version in preparation. Agda code available at URL: https://github.com/DoppeD/ConsistentCwfsOfDomains.
  27. John Longley and Dag Normann. Higher-Order Computability. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47992-6.
  28. Maria Emilia Maietti and Silvio Valentini. Exponentiation of Scott formal topologies. In A. Jung M. Escardó, editor, Proceedings of the Workshop on Domains VI, volume 73, pages 111-131, 2004. URL: https://doi.org/10.1016/j.entcs.2004.08.005.
  29. Michael Makkai and Robert Paré. Accessible categories: the foundations of categorical model theory, volume 104 of Contemporary Mathematics. American Mathematical Society, 1989. URL: https://doi.org/10.1090/conm/104.
  30. Sara Negri. Continuous lattices in formal topology. In Eduardo Giménez and Christine Paulin-Mohring, editors, Types for Proofs and Programs (TYPES 1996), volume 1512 of Lecture Notes in Computer Science, pages 333-353. Springer, 1998. URL: https://doi.org/10.1007/BFb0097800.
  31. Sara Negri. Continuous domains as formal spaces. Mathematical Structures in Computer Science, 12(1):19-52, 2002. URL: https://doi.org/10.1017/S0960129501003450.
  32. Dirk Pattinson and Mina Mohammadian. Constructive Domains with Classical Witnesses, June 2020. URL: http://arxiv.org/abs/1910.04948.
  33. G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223-255, 1977. URL: https://doi.org/10.1016/0304-3975(77)90044-5.
  34. Bernhard Reus. Formalizing synthetic domain theory - the basic definitions. Journal of Automated Reasoning, 23(3-4):411-444, 1999. URL: https://doi.org/10.1023/A:1006258506401.
  35. Bernhard Reus and Thomas Streicher. General synthetic domain theory - a logical approach. Mathematical Structures in Computer Science, 9(2):177–-223, 1999. URL: https://doi.org/10.1017/S096012959900273X.
  36. G. Rosolini. Categories and effective computations. In David H. Pitt, Axel Poigné, and David E. Rydeheard, editors, Category Theory and Computer Science, volume 283 of Lecture Notes in Computer Science, pages 1-11. Springer, 1987. Google Scholar
  37. Giuseppe Rosolini. Continuity and effectiveness in topoi. PhD thesis, University of Oxford, 1986. Google Scholar
  38. Giovanni Sambin. Intuitionistic formal spaces - a first communication. In Mathematical logic and its applications, pages 187-204. Springer, 1987. URL: https://doi.org/10.1007/978-1-4613-0897-3_12.
  39. Giovanni Sambin, Silvio Valentini, and Paolo Virgili. Constructive domain theory as a branch of intuitionistic pointfree topology. Theoretical Computer Science, 159(2):319-341, 1996. URL: https://doi.org/10.1016/0304-3975(95)00169-7.
  40. Dana S. Scott. Continuous lattices. In F.W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97-136. Springer, 1972. URL: https://doi.org/10.1007/BFB0073967.
  41. Dana S. Scott. Lectures on a mathematical theory of computation. In Manfred Broy and Gunther Schmidt, editors, Theoretical Foundations of Programming Methodology: Lecture Notes of an International Summer School, directed by F. L. Bauer, E. W. Dijkstra and C. A. R. Hoare, volume 91 of NATO Advanced Study Institutes Series, pages 145-292. Springer, 1982. URL: https://doi.org/10.1007/978-94-009-7893-5_9.
  42. Dana S. Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121(1):411-440, 1993. URL: https://doi.org/10.1016/0304-3975(93)90095-B.
  43. Andrew W. Swan. Choice, collection and covering in cubical sets. Talk in the electronic HoTTEST seminar, 6 November. Slides at https://www.uwo.ca/math/faculty/kapulkin/seminars/hottestfiles/Swan-2019-11-06-HoTTEST.pdf. Video recording at https://www.youtube.com/watch?v=r9KbEOzyr1g, 2019.
  44. Ayberk Tosun. Formal Topology in Univalent Foundations. Master’s thesis, Chalmers University of Technology and University of Gothenburg, 2020. Agda code available at: https://github.com/ayberkt/formal-topology-in-UF. URL: https://doi.org/20.500.12380/301098.
  45. Taichi Uemura. Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing. In Peter Dybjer, José Espírito Santo, and Luís Pinto, editors, 24th International Conference on Types for Proofs and Programs (TYPES 2018), volume 130 of Leibniz International Proceedings in Informatics (LIPIcs), pages 7:1-7:20. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.TYPES.2018.7.
  46. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  47. Vladimir Voevodsky. Resizing rules - their use and semantic justification. Slides from a talk at TYPES, Bergen, 11 September, 2011. URL: https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2011_Bergen.pdf.
  48. Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5):1278-1294, 2015. Google Scholar
  49. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. Available at URL: https://github.com/UniMath/UniMath.
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 Imprint Privacy Contact