No CrossRef data available.
Article contents
Realizability in ordered combinatory algebras with adjunction
Published online by Cambridge University Press: 26 April 2018
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 work, we continue our consideration of the constructions presented in the paper Krivine's Classical Realizability from a Categorical Perspective by Thomas Streicher. Therein, the author points towards the interpretation of the classical realizability of Krivine as an instance of the categorical approach started by Hyland. The present paper continues with the study of the basic algebraic set-up underlying the categorical aspects of the theory. Motivated by the search of a full adjunction, we introduce a new closure operator on the subsets of the stacks of an abstract Krivine structure that yields an adjunction between the corresponding application and implication operations. We show that all the constructions from ordered combinatory algebras to triposes presented in our previous work can be implemented, mutatis mutandis, in the new situation and that all the associated triposes are equivalent. We finish by proving that the whole theory can be developed using the ordered combinatory algebras with full adjunction or strong abstract Krivine structures as the basic set-up.
Information
- Type
- Paper
- Information
- Copyright
- Copyright © Cambridge University Press 2018
References
Birkhoff, G. (1995). Lattice Theory, Colloquium Publications, vol. 25, 3rd edition, American Mathematical Society.Google Scholar
Borceux, F. (2008). Handbook of Categorical Algebra Volume 1. Basic Category Theory, Encyclopedia of Mathematics and its Applications, vol. 50, Cambridge Univ. Press, Cambridge.Google Scholar
Borceux, F. (2008). Handbook of Categorical Algebra Volume 2. Categories and Structures, Encyclopedia of Mathematics and its Applications, vol. 51, Cambridge Univ. Press, Cambridge.Google Scholar
Curry, H. and Feys, R. (1958). Combinatory Logic, vol. 1, North Holland Publishing Co., Amsterdam.Google Scholar
Ferrer Santos, W., Guillermo, M. and Malherbe, O. (2013). A Report on Realizability, arXiv:1309.0706v2 [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, Camb. Univ. Press, 1–31.Google Scholar
Griffin, T. G. (1990). A Formulæ-as-Types Notion of Control, In: Proceedings of the Conference Record of the 17th Annual ACM Symposium on Principles of Programming Languages.Google Scholar
Hofstra, P. and van Oosten, J. (2004). Ordered partial combinatory algebras. Mathematical Proceedings of the Cambridge Philosophical Society 134 (3) 445–463.Google Scholar
Hofstra, P. (2006). All realizability is relative. Mathematical Proceedings of the Cambridge Philosophical Society 141 (2) 239–264.Google 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.Google 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.Google Scholar
Krivine, J.-L. (2001). Typed lambda-calculus in classical Zermelo-Fraenkel set theory. Archive for Mathematical Logic 40 (3) 189–205.Google Scholar
Krivine, J.-L. (2003). Dependent choice, quote and the clock. Theoretical Computer Science 308 259–276.Google Scholar
Krivine, J.-L. (2004). Realizability in Classical Logic, Lessons in Marseille-Lumini, (revised in 2005), 1–29. Available at https://hal-univ-diderot.archives-ouvertes.fr/hal-00154500/documentGoogle Scholar
Krivine, J.-L. (2008). Structures de réalisabilité, RAM et ultrafiltre sur ℕ, Available at 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, vol. 27, SMF.Google Scholar
Krivine, J.-L. Realizability Algebras: A Program to Well Order R, Logical Methods in Computer Science, vol. 7, Issue 3, 2.Google Scholar
Krivine, J.-L. (2012). Realizability algebras II : New models of ZF + DC, Logical Methods in Computer Science, vol. 8, Issue 1, 10.Google Scholar
Krivine, J.-L. (2016). Realizability Algebras III: Some Examples, Mathematical Structures in Computer Science, Cambridge University Press 1–32.Google Scholar
MacLane, S. (1997). Categories for the Working Mathematician, Graduate Texts in Mathematics, vol. 5, 2nd edition, Springer-Verlag, New York.Google Scholar
Miquel, A. (2014). Implicative Algebras for Noncommutative Forcing, Available at http://smc2014.univ-lyon1.fr/lib/exe/fetch.php?media=miquel.pdf?Google Scholar
Miquel, A. (2016). Implicative Algebras: A New Foundation for Forcing and Realizability, Available at https://www.pedrot.fr/montevideo2016/miquel-slides.pdfGoogle Scholar
Paré, R. and Schumacher, D. (1978). Abstract Families and the Adjoint Functor Theorems. Lectures Notes in Mathematics, vol. 661.Google Scholar
Streicher, T. (2013). Krivine's Classical Realizability From a Categorical Perspective, Mathematical Structures in Computer Science 23 (6) 1234–1256.Google Scholar
van Oosten, J. (2008). Realizability, an Introduction to its Categorical Side, Elsevier.Google Scholar
You have
Access
- 1
- Cited by