Hostname: page-component-74656f9884-8r8nv Total loading time: 0 Render date: 2026-11-09T01:24:05.477Z Has data issue: false hasContentIssue false
  • English
  • Français

The category of implicative algebras and realizability

Published online by Cambridge University Press:  16 September 2019

Walter Ferrer Santos  and
Octavio Malherbe
Walter Ferrer Santos
Affiliation:
Facultad de Ciencias, Udelar, Iguá 4225, 11400 Montevideo, Uruguay Departamento de matemática, Centro Universitario de la región este, Udelar, Tacuarembó, 20100 Punta del Este, Uruguay, Email: wrferrer@cure.edu.uy
Octavio Malherbe*
Affiliation:
Departamento de matemática, Centro Universitario de la región este, Udelar, Tacuarembó, 20100 Punta del Este, Uruguay, Email: wrferrer@cure.edu.uy Facultad de Ingeniería, Udelar J. Herrera y Reissig 565, 11300 Montevideo, Uruguay
*
*Corresponding author. Email: malherbe@fing.edu.uy
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

In this paper, we continue with the algebraic study of Krivine’s realizability, completing and generalizing some of the authors’ previous constructions by introducing two categories with objects the abstract Krivine structures and the implicative algebras, respectively. These categories are related by an adjunction whose existence clarifies many aspects of the theory previously established. We also revisit, reinterpret, and generalize in categorical terms, some of the results of our previous work such as: the bullet construction, the equivalence of Krivine’s, Streicher’s, and bullet triposes and also the fact that these triposes can be obtained – up to equivalence – from implicative algebras or implicative ordered combinatory algebras.

Keywords

Realizabilityapplicative morphismscomputationally dense morphismscombinatory algebrasabstract Krivine’s structures

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 29 , Issue 10 , November 2019 , pp. 1575 - 1606
Copyright
© Cambridge University Press 2019 

References

Birkhoff, G. (1995). Lattice Theory, third edition, vol. 25, American Mathematical Society, Colloquium Publications.Google Scholar
Borceux, F. (2008). Handbook of Categorical Algebra Volume 1. Basic Category Theory (Encyclopedia of Mathematics and its Applications, 50). Cambridge University Press, Cambridge.Google Scholar
Borceux, F. (2008). Handbook of Categorical Algebra Volume 2. Categories and Structures (Encyclopedia of Mathematics and its Applications, 51). Cambridge University Press, Cambridge.Google Scholar
Ferrer Santos, W., Guillermo, M. and Malherbe, O. (2013). A Report on Realizability, https://arxiv.org/abs/1309.0706v3 [math.LO], 1–25.Google Scholar
Ferrer Santos, W., Frey, J., Guillermo, M. Malherbe, O. and Miquel, A. (2015). Ordered combinatory algebras and realizability. Mathematical Structures in Computer Science (Cambridge University Press) 1–31.Google Scholar
Ferrer Santos, W., Guillermo, M. and Malherbe, O. (2019). Realizability in ordered combinatory algebras with adjunction. Mathematical Structures in Computer Science (Cambridge University Press) 29(3) 430–464. doi:10.1017/S0960129518000075.CrossRefGoogle Scholar
Grätzer, G. (1978). General Lattice Theory, Mathematische Reihe Lehrbücher und Monographien aus dem Gebiete der Exakten Wissenschaften 52, Birkhäuser, Basel.Google Scholar
Hofstra, P.J. and van Oosten, J. (2003). Ordered partial combinatory algebras. Mathematical Proceedings of the Cambridge Philosophical Society 134 445–463.CrossRefGoogle Scholar
Hofstra, P. (2006). All realizability is relative, Mathematical Proceedings of the Cambridge Philosophical Society 141(2) 239–264.CrossRefGoogle Scholar
Hofstra, P. (2008). Iterated realizability as a comma construction, Mathematical Proceedings of the Cambridge Philosophical Society 144, no.1, pp. 39–51.CrossRefGoogle Scholar
Hyland, J.M.E. (1982). The effective topos. In: Proceedings of The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout 1981), North Holland, 165–216.CrossRefGoogle Scholar
Hyland, J.M.E., Johnstone, P.T. and Pitts, A.M. (1980). Tripos theory, Mathematical Proceedings of the Cambridge Philosophical Society 88 205–232.CrossRefGoogle Scholar
Krivine, J.-L. (2001). Types lambda-calculus inclassical Zermelo–Fraenkel set theory. Archive for Mathematical Logic 40(3) 189–205.CrossRefGoogle Scholar
Krivine, J.-L. (2003). Dependent choice, ‘quote’ and the clock. Theoretical Computer Science 308 259–276.CrossRefGoogle Scholar
Krivine, J.-L. (2008). Structures de réalisabilité, RAM et ultrafiltre sur ,. http://www.pps.jussieu.fr/krivine/Ultrafiltre.pdf.Google Scholar
Krivine, J.-L. (2009). Realizability in classical logic in interactive models of computation and program behaviour. Panoramas et synthèses 27, SMF.Google Scholar
Mac Lane, S. (1971). Categories for the working mathematician. In: Graduate Texts in Mathematics, vol. 5, Springer.CrossRefGoogle Scholar
Miquel, A. (2014). Implicative algebras for non commutative forcing. In: Workshop. Mathematical Structures in Computation, Lyon. //smc2014.univ-lyon1.fr/lib/exe/fetch.php?media=miquel.pdfGoogle Scholar
Miquel, A. (2016). Implicative algebras: a new foundation for forcing and realizability. In: Workshop. Realizability in Uruguay, Piriapolis. //www.pédrot.fr/montevideo2016/miquel-slides.pdfGoogle Scholar
Miquel, A. (February 2018). Implicative algebras: a new foundation for forcing and realizability. https://arxiv.org/abs/1802.00528.Google Scholar
Miquey, E. (2017). Réalisabilité classique et effets de bords. http://www.theses.fr/s180391.Google Scholar
Street, R. (1972). The formal theory of monads. Journal of Pure and Applied Algebra (North-Holland Publishing Company), vol. 2, 149–168.CrossRefGoogle Scholar
Streicher, T. (2013). Krivine’s classical realizability from a categorical perspective. Mathematical Structures in Computer Science 23(6).CrossRefGoogle Scholar
van Oosten, J. (2008). Realizability, An Introduction to its Categorical Side, Elsevier.Google Scholar
van Oosten, J. and Zou, T. (2016). Classical and relative realizability. Theory and Applications of Categories 31 (22) (571–593).Google Scholar