Recursion and Sequentiality in Categories of Sheaves
We present a fully abstract model of a call-by-value language with higher-order functions, recursion and natural numbers, as an exponential ideal in a topos. Our model is inspired by the fully abstract models of O'Hearn, Riecke and Sandholm, and Marz and Streicher. In contrast with semantics based on cpo’s, we treat recursion as just one feature in a model built by combining a choice of modular components.
Denotational semantics
Full abstraction
Recursion
Sheaf toposes
CPOs
Theory of computation~Denotational semantics
Theory of computation~Categorical semantics
25:1-25:22
Regular Paper
Cristina
Matache
Cristina Matache
University of Oxford, UK
Research supported by an EPSRC studentship and Balliol College and Clarendon Fund scholarships.
Sean
Moss
Sean Moss
University of Oxford, UK
Research supported by a Junior Research Fellowship at University College, Oxford.
Sam
Staton
Sam Staton
University of Oxford, UK
Research supported by a Royal Society University Research Fellowship and the ERC BLAST grant.
10.4230/LIPIcs.FSCD.2021.25
Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. In Proc. TYPES 2013, 2013.
P Borthelle, T Hirschowitz, and A Lafont. A cellular Howe theorem. In Proc. LICS 2020, 2020.
Anna Bucalo, Carsten Führmann, and Alex Simpson. An equational notion of lifting monad. Theoret. Comput. Sci., 294:31-60, 2003.
J.R.B. Cockett and Stephen Lack. Restriction categories I: categories of partial maps. Theoret. Comput. Sci., 270(1):223-259, 2002.
J.R.B. Cockett and Stephen Lack. Restriction categories II: partial map classification. Theoret. Comput. Sci., 294(1):61-102, 2003.
Roy L Crole and Andrew M Pitts. New foundations for fixpoint combinators. In Proc. LICS 1990, 1990.
Eduardo J. Dubuc. Concrete quasitopoi. In Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9-21, 1977, pages 239-254. Springer Berlin Heidelberg, 1979.
Roy Dyckhoff and Walter Tholen. Exponentiable morphisms, partial products and pullback complements. J. Pure Appl. Algebra, 49(1-2):103-116, 1987.
M Fiore and G Plotkin. An extension of models of axiomatic domain theory to models of synthetic domain theory. In Proc. CSL 1996, 1997.
M. Fiore, G. Plotkin, and J. Power. Complete cuboidal sets in axiomatic domain theory. In Proc. LICS 1997, pages 268-279, 1997.
M. P. Fiore and A. K. Simpson. Lambda definability with sums via Grothendieck logical relations. In TLCA'99, 1999.
Marcelo Fiore. Enrichment and representation theorems for categories of domains and continuous functions. Available at the author’s website, 1996.
Marcelo P Fiore and Giuseppe Rosolini. Two models of synthetic domain theory. J. Pure Appl. Algebra, 116:151-162, 1997.
Marcelo P Fiore and Giuseppe Rosolini. Domains in H. Theoret. Comput. Sci., 264:171-193, 2001.
Richard Garner and Daniel Lin. Cocompletion of restriction categories. Theory Appl. Categ., 35(22):809-844, 2020.
C Heunen, O Kammar, S Staton, and H Yang. A convenient category for higher-order probability theory. In Proc. LICS 2017, 2017.
Gérard Huet. Formal Structures in Computation and Deduction. Unpublished, 1986.
M Huot, S Staton, and M Vákár. Correctness of automatic differentiation via diffeologies and categorical gluing. In Proc. FOSSACS 2020, 2020.
J M E Hyland. First steps in synthetic domain theory. In Proc. Category Theory, Como, Lect. Notes Math., pages 131-156. Springer, 1990.
P. T. Johnstone. Sketches of an elephant: a Topos theory compendium. Oxford logic guides. Oxford Univ. Press, 2002.
Achim Jung and Jerzy Tiuryn. A new characterization of lambda definability. In Marc Bezem and Jan Friso Groote, editors, Proc. TLCA'93, volume 664 of Lecture Notes in Computer Science, pages 245-257. Springer, 1993. URL: https://doi.org/10.1007/BFb0037110.
https://doi.org/10.1007/BFb0037110
O. Kammar and S. Katsumata. A modern perspective on the O'Hearn-Riecke model. Workshop on Syntax and Semantics of Low-Level Languages (LOLA), 2019.
Ohad Kammar, Shinya Katsumata, and Philip Saville. Full abstraction à la O'Hearn & Riecke for call-by-value with sums and effects. Manuscript, January 2021.
Paul B Levy. Amb breaks well-pointedness, ground amb doesn't. In Proc. MFPS 2007, 2007.
Paul B Levy, J Power, and H Thielecke. Modelling environments in call-by-value programming languages. Inform. Comput., 185(2):182-210, 2003.
Daniel Lin. Presheaves over a join restriction category. Applied Categorical Structures, 27(3):289-310, 2019.
B Lindenhovius, M Mislove, and V Zamdzhiev. Mixed linear and non-linear recursive types. In Proc. ICFP 2019, 2019.
John R Longley and Alex K Simpson. A uniform approach to domain theory in realizability models. Math. Struct. Comput. Sci., 7(5):469-505, 1997.
M. Marz. A Fully Abstract Model for Sequential Computation. PhD thesis, Technische Universität Darmstadt, 2000.
Michael Marz. A fully abstract model for sequential computation. Electronic Notes in Theoretical Computer Science, 35:133-152, 2000. Workshop on Domains IV.
Robin Milner. Fully abstract models of typed λ-calculi. Theoret. Comput. Sci., 4(1):1-22, 1977.
Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93:55-92, 1991.
Philip S. Mulry. Monads and algebras in the semantics of partial data types. Theoretical Computer Science, 99(1):141-155, 1992.
Philip S. Mulry. Partial map classifiers and partial cartesian closed categories. Theoretical Computer Science, 136(1):109-123, 1994.
Jaap van OostenOosten and Alex K Simpson. Axioms and (counter)examples in synthetic domain theory. Annals Pure Appl. Logic, 104:233-278, 2000.
P. W. O'Hearn and J. G. Riecke. Kripke logical relations and PCF. Inf. Comput., 120(1):107-116, 1995.
A M Pitts. Polymorphism is set theoretic, constructively. In Proc. CTCS 1987, volume 283 of LNCS. Springer, 1987.
Bernhard Reus and Thomas Streicher. General synthetic domain theory - a logical approach. Math. Struct. Comput. Sci., 9(2):177-223, 1999.
J. G. Riecke and A. Sandholm. A relational account of call-by-value sequentiality. Inf. Comput., 179(2):296-331, 2002.
Giuseppe Rosolini. Continuity and effectiveness in topoi. PhD thesis, University of Oxford, 1986.
Dana S Scott. Relating theories of the λ-calculus. In To H B Curry: essays in combinatory logic, lambda calculus and formalisms, pages 403-450. Academic Press, 1980.
B Sherman, J Michel, and M Carbin. λ_s: Computable semantics for differentiable programming with higher-order functions and datatypes. In Proc. POPL 2021, 2021.
K. Sieber. Reasoning about sequential functions via logical relations. In Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991, London Mathematical Society Lecture Note Series, page 258–269. Cambridge University Press, 1992.
Alex Simpson and Giuseppe Rosolini. Using synthetic domain theory to prove operational properties of a polymorphic programming language based on strictness. Unpublished, 2004.
Alex K. Simpson. Computational adequacy in an elementary topos. In Georg Gottlob, Etienne Grandjean, and Katrin Seyr, editors, Computer Science Logic, pages 323-342, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg.
T. Streicher. Domain-theoretic foundations of functional programming. World Scientific, 2006.
Paul Taylor. The fixed point property in synthetic domain theory. In Proc. LICS 1991, 1991.
Cristina Matache, Sean Moss, and Sam Staton
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode