Document Open Access Logo

Gardening with the Pythia A Model of Continuity in a Dependent Setting

Authors Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.5.pdf
  • Filesize: 0.79 MB
  • 18 pages

Document Identifiers

Author Details

Martin Baillon
  • INRIA and LS2N, Nantes, France
Assia Mahboubi
  • INRIA and LS2N, Nantes, France
Pierre-Marie Pédrot
  • INRIA and LS2N, Nantes, France

Cite AsGet BibTex

Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. Gardening with the Pythia A Model of Continuity in a Dependent Setting. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.5

Abstract

We generalize to a rich dependent type theory a proof originally developed by Escardó that all System 𝚃 functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory, a type theory where dependent elimination must be strict, into the Calculus of Inductive Constructions. The model is given by three translations: the axiom translation, that adds an oracle to the context; the branching translation, based on the dialogue monad, turning every type into a tree; and finally, a layer of algebraic binary parametricity, binding together the two translations. In the resulting type theory, every function f : (ℕ → ℕ) → ℕ is externally continuous.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Type theory
  • continuity
  • syntactic model

Metrics

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

Supplementary Materials

References

  1. Danel Ahman. Handling fibred algebraic effects. Proc. ACM Program. Lang., 2(POPL):7:1-7:29, 2018. URL: https://doi.org/10.1145/3158095.
  2. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 293-310. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_16.
  3. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, pages 18-29. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837638.
  4. Michael Beeson. Foundations of Constructive Mathematics: Metamathematical Studies. Number 6 in Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer, Berlin Heidelberg New York Tokyo, 1985. Google Scholar
  5. Jean-Philippe Bernardy and Marc Lasson. Realizability and parametricity in pure type systems. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 108-122. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_8.
  6. Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli. Computability beyond Church-Turing via choice sequences. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 245-254. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209200.
  7. Simon Boulier. Extending type theory with syntactic models. Logic in Computer Science [cs.LO]. École nationale supérieure Mines-Télécom Atlantique, 2018. URL: https://tel.archives-ouvertes.fr/tel-02007839.
  8. Thierry Coquand and Guilhem Jaber. A note on forcing and type theory. Fundam. Informaticae, 100(1-4):43-52, 2010. URL: https://doi.org/10.3233/FI-2010-262.
  9. Thierry Coquand and Guilhem Jaber. A computational interpretation of forcing in type theory. In Peter Dybjer, Sten Lindström, Erik Palmgren, and Göran Sundholm, editors, Epistemology versus Ontology - Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, volume 27 of Logic, Epistemology, and the Unity of Science, pages 203-213. Springer, 2012. URL: https://doi.org/10.1007/978-94-007-4435-6_10.
  10. Martín Escardó and Chuangjie Xu. A constructive manifestation of the Kleene-Kreisel continuous functionals. Ann. Pure Appl. Log., 167(9):770-793, 2016. URL: https://doi.org/10.1016/j.apal.2016.04.011.
  11. Martin Hötzel Escardó. Continuity of Gödel’s System T definable functionals via effectful forcing. Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2013, New Orleans, LA, USA, June 23-25, 2013. URL: https://doi.org/10.1016/j.entcs.2013.09.010.
  12. Martin Hötzel Escardó and Chuangjie Xu. The inconsistency of a brouwerian continuity principle with the Curry-Howard interpretation. 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, Warsaw, Poland, July 1-3, 2015. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.153.
  13. Martin Hofmann. Extensional constructs in intensional type theory. CPHC/BCS distinguished dissertations. Springer, 1997. Google Scholar
  14. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: i, ii, and III. Inf. Comput., 163(2):285-408, 2000. URL: https://doi.org/10.1006/inco.2000.2917.
  15. Ambrus Kaposi, András Kovács, and Nicolai Kraus. Shallow embedding of type theory is morally correct. In Graham Hutton, editor, Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, volume 11825 of Lecture Notes in Computer Science, pages 329-365. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-33636-3_12.
  16. Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. In Ben Lippmeier, editor, Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, pages 94-105. ACM, 2015. URL: https://doi.org/10.1145/2804302.2804319.
  17. S.C. Kleene. Recursive functionals and quantifiers of finite types revisited I. In J.E. Fenstad, R.O. Gandy, and G.E. Sacks, editors, Generalized Recursion Theory II, volume 94 of Studies in Logic and the Foundations of Mathematics, pages 185-222. Elsevier, 1978. URL: https://doi.org/10.1016/S0049-237X(08)70933-9.
  18. G. Kreisel, D. Lacombe, and J.R. Shoenfield. Partial recursive functionals and effective operations. In A. Heyting, editor, Constructivity in Mathematics, Studies in Logic and the Foundations of Mathematics, pages 290-297, Amsterdam, 1959. North-Holland. Proc. Colloq., Amsterdam, Aug. 26-31, 1957. Google Scholar
  19. Jean-Louis Krivine. Opérateurs de mise en mémoire et traduction de Gödel. Arch. Math. Log., 30(4):241-267, 1990. URL: https://doi.org/10.1007/BF01792986.
  20. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004. Google Scholar
  21. John Longley and Dag Normann. Higher-Order Computability. Theory and Applications of Computability. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47992-6.
  22. Conor McBride. Turing-completeness totally free. In Ralf Hinze and Janis Voigtländer, editors, Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, June 29 - July 1, 2015. Proceedings, volume 9129 of Lecture Notes in Computer Science, pages 257-275. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19797-5_13.
  23. Christine Paulin-Mohring. Définitions Inductives en Théorie des Types. Habilitation à diriger des recherches, Université Claude Bernard - Lyon I, December 1996. URL: https://tel.archives-ouvertes.fr/tel-00431817.
  24. Pierre-Marie Pédrot. Russian constructivism in a prefascist theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 782-794. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394740.
  25. Pierre-Marie Pédrot and Nicolas Tabareau. The fire triangle: how to mix substitution, dependent elimination, and effects. Proc. ACM Program. Lang., 4(POPL):58:1-58:28, 2020. URL: https://doi.org/10.1145/3371126.
  26. Maciej Piróg and Jeremy Gibbons. The coinductive resumption monad. In Bart Jacobs, Alexandra Silva, and Sam Staton, editors, Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2014, Ithaca, NY, USA, June 12-15, 2014, volume 308 of Electronic Notes in Theoretical Computer Science, pages 273-288. Elsevier, 2014. URL: https://doi.org/10.1016/j.entcs.2014.10.015.
  27. Gordon D. Plotkin and Matija Pretnar. Handling algebraic effects. Log. Methods Comput. Sci., 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:23)2013.
  28. Pierre-Marie Pédrot and Nicolas Tabareau. An effectful way to eliminate addiction to dependence. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. URL: https://doi.org/10.1109/LICS.2017.8005113.
  29. Pierre-Marie Pédrot and Nicolas Tabareau. Failure is not an option an exceptional type theory. ESOP 2018 - 27th European Symposium on Programming, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_9.
  30. Vincent Rahli and Mark Bickford. Validating Brouwer’s continuity principle for numbers using named exceptions. Math. Struct. Comput. Sci., 28(6):942-990, 2018. URL: https://doi.org/10.1017/S0960129517000172.
  31. Vincent Rahli, Mark Bickford, Liron Cohen, and Robert L. Constable. Bar induction is compatible with constructive type theory. J. ACM, 66(2):13:1-13:35, 2019. URL: https://doi.org/10.1145/3305261.
  32. Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. URL: https://doi.org/10.23638/LMCS-16(1:2)2020.
  33. Pierre-Marie Pédrot Simon Boulier and Nicolas Tabareau. The next 700 syntactical models of type theory. Certified Programs and Proofs (CPP 2017), Jan 2017, Paris, France. pp.182-194, 2017. URL: https://doi.org/10.1145/3018610.3018620.
  34. Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in Coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 499-514. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_32.
  35. Jonathan Sterling. Higher order functions and Brouwer’s thesis. Journal of Functional Programming, 31:e11, 2021. Bob Harper Festschrift Collection. URL: https://doi.org/10.1017/S0956796821000095.
  36. Wouter Swierstra. Data types à la carte. J. Funct. Program., 18(4):423-436, 2008. URL: https://doi.org/10.1017/S0956796808006758.
  37. G. S. Tseitin. Algorithmic operators in constructive metric spaces. In Problems of the constructive direction in mathematics. Part 2. Constructive mathematical analysis, volume 67, pages 295-361, Moscow-Leningrad, 1962. USSR Academy of Sciences. Google Scholar
  38. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  39. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in coq. Proc. ACM Program. Lang., 4(POPL):51:1-51:32, 2020. URL: https://doi.org/10.1145/3371119.
  40. Chuangjie Xu and Martín Hötzel Escardó. A constructive model of uniform continuity. In Masahito Hasegawa, editor, Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings, volume 7941 of Lecture Notes in Computer Science, pages 236-249. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38946-7_18.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact