Document Open Access Logo

Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models

Author Étienne Miquey

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.30.pdf
  • Filesize: 0.59 MB
  • 18 pages

Document Identifiers

Author Details

Étienne Miquey
  • Équipe Gallinette, INRIA, LS2N, Université de Nantes, France

Funding

This research was partially funded by the ANII research project FCE_1_2014_1_104800.

Acknowledgements

The author would like to thank Alexandre Miquel to which several ideas in this paper, especially the definition of conjunctive separators, should be credited.

Cite AsGet BibTex

Étienne Miquey. Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CSL.2020.30

Abstract

In an impressive series of papers, Krivine showed at the edge of the last decade how classical realizability provides a surprising technique to build models for classical theories. In particular, he proved that classical realizability subsumes Cohen’s forcing, and even more, gives rise to unexpected models of set theories. Pursuing the algebraic analysis of these models that was first undertaken by Streicher, Miquel recently proposed to lay the algebraic foundation of classical realizability and forcing within new structures which he called implicative algebras. These structures are a generalization of Boolean algebras based on an internal law representing the implication. Notably, implicative algebras allow for the adequate interpretation of both programs (i.e. proofs) and their types (i.e. formulas) in the same structure. The very definition of implicative algebras takes position on a presentation of logic through universal quantification and the implication and, computationally, relies on the call-by-name λ-calculus. In this paper, we investigate the relevance of this choice, by introducing two similar structures. On the one hand, we define disjunctive algebras, which rely on internal laws for the negation and the disjunction and which we show to be particular cases of implicative algebras. On the other hand, we introduce conjunctive algebras, which rather put the focus on conjunctions and on the call-by-value evaluation strategy. We finally show how disjunctive and conjunctive algebras algebraically reflect the well-known duality of computation between call-by-name and call-by-value.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Proof theory
  • Theory of computation → Type theory
Keywords
  • realizability
  • model theory
  • forcing
  • proofs-as-programs
  • λ-calculus
  • classical logic
  • duality
  • call-by-value
  • call-by-name
  • lattices
  • tripos

Metrics

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

Related Versions

References

  1. John L. Bell. Set Theory: Boolean-Valued Models and Independence Proofs. Oxford: Clarendon Press, 2005. Google Scholar
  2. P. Bernays. Axiomatische Untersuchung des Aussagen-Kalküls der "Principia Mathematica". Mathematische Zeitschrift, 25:305-320, 1926. Google Scholar
  3. Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of system F with subtyping, pages 750-770. Springer Berlin Heidelberg, Berlin, Heidelberg, 1991. URL: https://doi.org/10.1007/3-540-54415-1_73.
  4. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of ICFP 2000, SIGPLAN Notices 35(9), pages 233-243. ACM, 2000. URL: https://doi.org/10.1145/351240.351262.
  5. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. LKQ and LKT : Sequent calculi for second order logic based upon dual linear decompositions of classical implication. In Advances in Linear Logic, 1995. Google Scholar
  6. W. Ferrer and O. Malherbe. The category of implicative algebras and realizability. ArXiv e-prints, December 2017. URL: http://arxiv.org/abs/1712.06043.
  7. W. Ferrer Santos, M. Guillermo, and O. Malherbe. A Report on Realizability. ArXiv e-prints, 2013. URL: http://arxiv.org/abs/1309.0706.
  8. W. Ferrer Santos, M. Guillermo, and O. Malherbe. Realizability in OCAs and AKSs. ArXiv e-prints, 2015. URL: http://arxiv.org/abs/1512.07879.
  9. Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo, Octavio Malherbe, and Alexandre Miquel. Ordered combinatory algebras and realizability. Mathematical Structures in Computer Science, 27(3):428–458, 2017. URL: https://doi.org/10.1017/S0960129515000432.
  10. Jonas Frey. Realizability Toposes from Specifications. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 196-210, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.196.
  11. Jonas Frey. Classical Realizability in the CPS Target Language. Electronic Notes in Theoretical Computer Science, 325(Supplement C):111-126, 2016. The Thirty-second Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII). URL: https://doi.org/10.1016/j.entcs.2016.09.034.
  12. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  13. Timothy G. Griffin. A Formulae-as-type Notion of Control. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '90, pages 47-58, New York, NY, USA, 1990. ACM. URL: https://doi.org/10.1145/96709.96714.
  14. Hugo Herbelin. An Intuitionistic Logic that Proves Markov’s Principle. In LICS 2010, Proceedings, 2010. URL: https://doi.org/10.1109/LICS.2010.49.
  15. Hugo Herbelin. A Constructive Proof of Dependent Choice, Compatible with Classical Logic. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 365-374. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.47.
  16. Pieter Hofstra and Jaap Van Oosten. Ordered partial combinatory algebras. Mathematical Proceedings of the Cambridge Philosophical Society, 134(3):445–463, 2003. URL: https://doi.org/10.1017/S0305004102006424.
  17. Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, and Nicolas Tabareau. The Definitional Side of the Forcing. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 367-376, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2933575.2935320.
  18. Guilhem Jaber, Nicolas Tabareau, and Matthieu Sozeau. Extending Type Theory with Forcing. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, LICS '12, pages 395-404, Washington, DC, USA, 2012. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2012.49.
  19. J.-L. Krivine. Dependent choice, `quote' and the clock. Th. Comp. Sc., 308:259-276, 2003. Google Scholar
  20. J.-L. Krivine. Realizability in classical logic. In Interactive models of computation and program behaviour. Panoramas et synthèses, 27, 2009. Google Scholar
  21. J.-L. Krivine. Realizability algebras: a program to well order R. Logical Methods in Computer Science, 7(3), 2011. URL: https://doi.org/10.2168/LMCS-7(3:2)2011.
  22. J.-L. Krivine. Realizability algebras II : new models of ZF + DC. Logical Methods in Computer Science, 8(1):10, February 2012. 28 p. URL: https://doi.org/10.2168/LMCS-8(1:10)2012.
  23. J.-L. Krivine. Quelques propriétés des modèles de réalisabilité de ZF, February 2014. URL: http://hal.archives-ouvertes.fr/hal-00940254.
  24. Jean-Louis Krivine. On the Structure of Classical Realizability Models of ZF. In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors, 20th International Conference on Types for Proofs and Programs (TYPES 2014), volume 39 of Leibniz International Proceedings in Informatics (LIPIcs), pages 146-161, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2014.146.
  25. Jean-Louis Krivine. Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:11, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.25.
  26. Olivier Laurent. A study of polarization in logic. PhD thesis, Université de la Méditerranée - Aix-Marseille II, March 2002. URL: https://tel.archives-ouvertes.fr/tel-00007884.
  27. Rodolphe Lepigre. A Classical Realizability Model for a Semantical Value Restriction. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 476-502. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_19.
  28. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004. URL: https://doi.org/10.1007/978-94-007-0954-6.
  29. A. Miquel. Forcing as a Program Transformation. In LICS, pages 197-206. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.47.
  30. Alexandre Miquel. Existential witness extraction in classical realizability and via a negative translation. Logical Methods in Computer Science, 7(2):188-202, 2011. URL: https://doi.org/10.2168/LMCS-7(2:2)2011.
  31. Alexandre Miquel. Implicative algebras: a new foundation for realizability and forcing. ArXiv e-prints, 2018. URL: http://arxiv.org/abs/1802.00528.
  32. Étienne Miquey. Classical realizability and side-effects. Ph.D. thesis, Université Paris Diderot ; Universidad de la República, Uruguay, November 2017. URL: https://hal.inria.fr/tel-01653733.
  33. Étienne Miquey. A Sequent Calculus with Dependent Types for Classical Arithmetic. In LICS 2018, pages 720-729. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209199.
  34. Étienne Miquey. Formalizing Implicative Algebras in Coq. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving, pages 459-476. Springer International Publishing, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_27.
  35. Guillaume Munch-Maccagnoni. Focalisation and Classical Realisability. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic '09, volume 5771 of Lecture Notes in Computer Science, pages 409-423. Springer, Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-04027-6_30.
  36. P. Oliva and T. Streicher. On Krivine’s Realizability Interpretation of Classical Second-Order Arithmetic. Fundam. Inform., 84(2):207-220, 2008. URL: http://iospress.metapress.com/content/f51774wm73404583/.
  37. Andrew M. Pitts. Tripos theory in retrospect. Mathematical Structures in Computer Science, 12(3):265–279, 2002. URL: https://doi.org/10.1017/S096012950200364X.
  38. Thomas Streicher. Krivine’s classical realisability from a categorical perspective. Mathematical Structures in Computer Science, 23(6):1234–1256, 2013. URL: https://doi.org/10.1017/S0960129512000989.
  39. Jaap van Oosten. Studies in Logic and the Foundations of Mathematics. In Realizability: An Introduction to its Categorical Side, volume 152 of Studies in Logic and the Foundations of Mathematics, pages ii-. Elsevier, 2008. URL: https://doi.org/10.1016/S0049-237X(13)72046-9.
  40. Jaap van Oosten and Zou Tingxiang. Classical and Relative Realizability. Theory and Applications of Categories, 31:571-593, March 2016. Google Scholar
  41. Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge University Press, 1925-1927. Google Scholar
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