Document Open Access Logo

Recursion and Sequentiality in Categories of Sheaves

Authors Cristina Matache, Sean Moss, Sam Staton

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2021.25.pdf
  • Filesize: 0.74 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Categorical semantics
Keywords
  • Denotational semantics
  • Full abstraction
  • Recursion
  • Sheaf toposes
  • CPOs

Metrics

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

Abstract

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.

Cite As Get BibTex

Cristina Matache, Sean Moss, and Sam Staton. Recursion and Sequentiality in Categories of Sheaves. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSCD.2021.25

Author Details

Cristina Matache
  • University of Oxford, UK
Sean Moss
  • University of Oxford, UK
Sam Staton
  • University of Oxford, UK

Funding

  • Matache, Cristina: Research supported by an EPSRC studentship and Balliol College and Clarendon Fund scholarships.
  • Moss, Sean: Research supported by a Junior Research Fellowship at University College, Oxford.
  • Staton, Sam: Research supported by a Royal Society University Research Fellowship and the ERC BLAST grant.

References

  1. Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. In Proc. TYPES 2013, 2013. Google Scholar
  2. P Borthelle, T Hirschowitz, and A Lafont. A cellular Howe theorem. In Proc. LICS 2020, 2020. Google Scholar
  3. Anna Bucalo, Carsten Führmann, and Alex Simpson. An equational notion of lifting monad. Theoret. Comput. Sci., 294:31-60, 2003. Google Scholar
  4. J.R.B. Cockett and Stephen Lack. Restriction categories I: categories of partial maps. Theoret. Comput. Sci., 270(1):223-259, 2002. Google Scholar
  5. J.R.B. Cockett and Stephen Lack. Restriction categories II: partial map classification. Theoret. Comput. Sci., 294(1):61-102, 2003. Google Scholar
  6. Roy L Crole and Andrew M Pitts. New foundations for fixpoint combinators. In Proc. LICS 1990, 1990. Google Scholar
  7. 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. Google Scholar
  8. Roy Dyckhoff and Walter Tholen. Exponentiable morphisms, partial products and pullback complements. J. Pure Appl. Algebra, 49(1-2):103-116, 1987. Google Scholar
  9. M Fiore and G Plotkin. An extension of models of axiomatic domain theory to models of synthetic domain theory. In Proc. CSL 1996, 1997. Google Scholar
  10. M. Fiore, G. Plotkin, and J. Power. Complete cuboidal sets in axiomatic domain theory. In Proc. LICS 1997, pages 268-279, 1997. Google Scholar
  11. M. P. Fiore and A. K. Simpson. Lambda definability with sums via Grothendieck logical relations. In TLCA'99, 1999. Google Scholar
  12. Marcelo Fiore. Enrichment and representation theorems for categories of domains and continuous functions. Available at the author’s website, 1996. Google Scholar
  13. Marcelo P Fiore and Giuseppe Rosolini. Two models of synthetic domain theory. J. Pure Appl. Algebra, 116:151-162, 1997. Google Scholar
  14. Marcelo P Fiore and Giuseppe Rosolini. Domains in H. Theoret. Comput. Sci., 264:171-193, 2001. Google Scholar
  15. Richard Garner and Daniel Lin. Cocompletion of restriction categories. Theory Appl. Categ., 35(22):809-844, 2020. Google Scholar
  16. C Heunen, O Kammar, S Staton, and H Yang. A convenient category for higher-order probability theory. In Proc. LICS 2017, 2017. Google Scholar
  17. Gérard Huet. Formal Structures in Computation and Deduction. Unpublished, 1986. Google Scholar
  18. M Huot, S Staton, and M Vákár. Correctness of automatic differentiation via diffeologies and categorical gluing. In Proc. FOSSACS 2020, 2020. Google Scholar
  19. J M E Hyland. First steps in synthetic domain theory. In Proc. Category Theory, Como, Lect. Notes Math., pages 131-156. Springer, 1990. Google Scholar
  20. P. T. Johnstone. Sketches of an elephant: a Topos theory compendium. Oxford logic guides. Oxford Univ. Press, 2002. Google Scholar
  21. 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.
  22. 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. Google Scholar
  23. Ohad Kammar, Shinya Katsumata, and Philip Saville. Full abstraction à la O'Hearn & Riecke for call-by-value with sums and effects. Manuscript, January 2021. Google Scholar
  24. Paul B Levy. Amb breaks well-pointedness, ground amb doesn't. In Proc. MFPS 2007, 2007. Google Scholar
  25. Paul B Levy, J Power, and H Thielecke. Modelling environments in call-by-value programming languages. Inform. Comput., 185(2):182-210, 2003. Google Scholar
  26. Daniel Lin. Presheaves over a join restriction category. Applied Categorical Structures, 27(3):289-310, 2019. Google Scholar
  27. B Lindenhovius, M Mislove, and V Zamdzhiev. Mixed linear and non-linear recursive types. In Proc. ICFP 2019, 2019. Google Scholar
  28. 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. Google Scholar
  29. M. Marz. A Fully Abstract Model for Sequential Computation. PhD thesis, Technische Universität Darmstadt, 2000. Google Scholar
  30. Michael Marz. A fully abstract model for sequential computation. Electronic Notes in Theoretical Computer Science, 35:133-152, 2000. Workshop on Domains IV. Google Scholar
  31. Robin Milner. Fully abstract models of typed λ-calculi. Theoret. Comput. Sci., 4(1):1-22, 1977. Google Scholar
  32. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93:55-92, 1991. Google Scholar
  33. Philip S. Mulry. Monads and algebras in the semantics of partial data types. Theoretical Computer Science, 99(1):141-155, 1992. Google Scholar
  34. Philip S. Mulry. Partial map classifiers and partial cartesian closed categories. Theoretical Computer Science, 136(1):109-123, 1994. Google Scholar
  35. Jaap van OostenOosten and Alex K Simpson. Axioms and (counter)examples in synthetic domain theory. Annals Pure Appl. Logic, 104:233-278, 2000. Google Scholar
  36. P. W. O'Hearn and J. G. Riecke. Kripke logical relations and PCF. Inf. Comput., 120(1):107-116, 1995. Google Scholar
  37. A M Pitts. Polymorphism is set theoretic, constructively. In Proc. CTCS 1987, volume 283 of LNCS. Springer, 1987. Google Scholar
  38. Bernhard Reus and Thomas Streicher. General synthetic domain theory - a logical approach. Math. Struct. Comput. Sci., 9(2):177-223, 1999. Google Scholar
  39. J. G. Riecke and A. Sandholm. A relational account of call-by-value sequentiality. Inf. Comput., 179(2):296-331, 2002. Google Scholar
  40. Giuseppe Rosolini. Continuity and effectiveness in topoi. PhD thesis, University of Oxford, 1986. Google Scholar
  41. 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. Google Scholar
  42. B Sherman, J Michel, and M Carbin. λ_s: Computable semantics for differentiable programming with higher-order functions and datatypes. In Proc. POPL 2021, 2021. Google Scholar
  43. 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. Google Scholar
  44. Alex Simpson and Giuseppe Rosolini. Using synthetic domain theory to prove operational properties of a polymorphic programming language based on strictness. Unpublished, 2004. Google Scholar
  45. 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. Google Scholar
  46. T. Streicher. Domain-theoretic foundations of functional programming. World Scientific, 2006. Google Scholar
  47. Paul Taylor. The fixed point property in synthetic domain theory. In Proc. LICS 1991, 1991. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact