Document Open Access Logo

The Functional Machine Calculus II: Semantics

Authors Chris Barrett, Willem Heijltjes, Guy McCusker

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.10.pdf
  • Filesize: 0.67 MB
  • 18 pages

Document Identifiers

Author Details

Chris Barrett
  • Department of Computer Science, University of Bath, UK
Willem Heijltjes
  • Department of Computer Science, University of Bath, UK
Guy McCusker
  • Department of Computer Science, University of Bath, UK

Funding

  • Heijltjes, Willem: EPSRC Grant EP/R029121/1 Typed lambda-calculi with sharing and unsharing.

Acknowledgements

Pierre Clairambault, Ugo Dal Lago, Anupam Das, Giulio Guerrieri, Jim Laird, Paul Levy, Simon Peyton Jones, John Power, Alex Simpson, Vincent van Oostrom.

Cite AsGet BibTex

Chris Barrett, Willem Heijltjes, and Guy McCusker. The Functional Machine Calculus II: Semantics. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.10

Abstract

The Functional Machine Calculus (FMC), recently introduced by the second author, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects. In this paper, we explore the denotational semantics of the FMC. We have three main contributions: first, we argue that its syntax - in which both effects and lambda-calculus are realised using the same syntactic constructs - is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambda-calculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • lambda-calculus
  • computational effects
  • denotational semantics
  • strong normalization

Metrics

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

Related Versions

References

  1. Mario Alvarez-Picallo, Dan R. Ghica, David Sprunger, and Fabio Zanasi. Functorial string diagrams for reverse-mode automatic differentiation. Computer Science Logic (CSL) 2023, 2023. URL: http://arxiv.org/abs/2107.13433.
  2. Roel de Vrijer. Exactly estimating functionals and strong normalization. Indagationes Mathematicae (Proceedings), 90(4):479-493, 1987. Google Scholar
  3. Robin Gandy. Proofs of strong normalization. In Jonathan P. Seldin and J. Roger Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457-477. Academic Press, 1980. Google Scholar
  4. Inge Gørtz, Signe Reuss, and Morten Sørensen. Strong normalization from weak normalization by translation into the Lambda-I-calculus. Higher-Order and Symbolic Computation, 16:253-285, 2003. URL: https://doi.org/10.1023/A:1025693307470.
  5. Masahito Hasegawa. Decomposing typed lambda-calculus into a couple of categorical programming languages. In International Conference on Category Theory and Computer Science, 1995. Google Scholar
  6. Willem Heijltjes. The functional machine calculus. To appear in Mathematical Foundations of Programming Semantics (MFPS 2022). Preprint available at http://people.bath.ac.uk/wbh22/index.html#FMC2022, 2022.
  7. Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, 20:199-207, 2007. URL: https://doi.org/10.1007/s10990-007-9018-9.
  8. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Information and Computation, 185:182-210, 2003. Google Scholar
  9. Robin Milner. Action calculi, or syntactic action structures. In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS'93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings, volume 711 of Lecture Notes in Computer Science, pages 105-121. Springer, 1993. URL: https://doi.org/10.1007/3-540-57182-5_7.
  10. Slava Pestov, Daniel Ehrenberg, and Joe Groff. Factor: A dynamic stack-based programming language. ACM SIGPLAN Notices, 45(12):43-58, 2010. Google Scholar
  11. Andrew Pitts. Relational properties of domains. Information and Computation, 127:66-90, 1996. Google Scholar
  12. Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. In Higher order operational techniques in semantics, pages 227-273. Isaac Newton Institute for Mathematical Sciences, 1998. Google Scholar
  13. Gordon Plotkin and John Power. Notions of computation determine monads. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), pages 342-356. Springer, Berlin, Heidelberg, 2002. Google Scholar
  14. Jaco van de Pol. Two different strong normalization proofs? In Selected Papers from the Second International Workshop on Higher Order Algebra, Logic, and Term Rewriting (HOA '95), volume 1074 of LNCS, pages 201-220, 1995. URL: https://doi.org/10.1007/3-540-61254-8_27.
  15. Jaco van de Pol and Helmut Schwichtenberg. Strict functionals for termination proofs. In Proceedings of the Second International Conference on Typed Lambda Calculi and Applications (TLCA '95), pages 350-364. Springer-Verlag, 1995. Google Scholar
  16. John Power and Edmund Robinson. Premonoidal categories and notions of computation. Mathematical Structures in Computer Science, 7:453-468, 1997. Google Scholar
  17. John Power and Hayo Thielecke. Closed Freyd- and κ-categories. In International Colloquium on Automata, Languages, and Programming (ICALP), volume 1644 of LNCS, pages 625-634. Springer, 1999. Google Scholar
  18. Helmut Schwichtenberg. Complexity of normalization in the pure typed lambda-calculus. In Anne Sjerp Troelstra and Dirk van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 453-457. Elsevier, 1982. Google Scholar
  19. Thomas Streicher and Bernhard Reus. Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8(6):543-572, 1998. Google Scholar
  20. Glynn Winskel. The formal semantics of programming languages: An introduction. MIT Press, Cambridge, Massachusetts, 1993. 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