Skip to main content
SpringerLink
Log in

Streams of Approximations, Equivalence of Recursive Effectful Programs

  • Conference paper
  • First Online:
Mathematics of Program Construction (MPC 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13544))

Included in the following conference series:

  • 371 Accesses

Abstract

Behavioural equivalence for functional languages with algebraic effects and general recursion is often difficult to formalize. When modelling the behaviour of higher-order programs, one often needs to employ multiple coinductive structures simultaneously. In this paper, we aim to simplify the issue with a single external stream monad dealing with recursion, and deal with the structures for modelling higher-order types in a purely inductive (finite) manner. We take a page from classical domain theory, modelling recursive programs as limits of increasing sequences of “finite” denotational elements. We carry around a single relation which contains all relevant information of behaviour: self-related elements are considered correct according to the denotational semantics, and two elements that are related both ways are considered equivalent. We implement equivalence of effectful programs using a relation lifting, creating a notion of behavioural equivalence for approximations. This is lifted to behavioural equivalence for recursive programs modelled by sequences of approximations, using a relator implementing a notion of weak similarity. We apply this to a fragment of call-by-push-value lambda calculus with algebraic effects, and establish a denotational equivalence which is sound with respect to an operational semantics, and sound with respect to contextual equivalence.

The authors were supported by the ESF funded Estonian IT Academy research measure (project 2014–2020.4.05.19–0001). Veltri was also supported by the Estonian Research Council grant PSG749.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 49.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 64.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    In [11] these would be called inductive relators for \(T_S\), though in our case without the inductive property requiring closure under limits since our approximation spaces are not closed under limits. To avoid confusion, we would like to use the word “sufficient”, which is not a technical term. It simply encapsulates a collection of properties that are sufficient for achieving the results presented later in the paper.

References

  1. Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Log. 51(1–2), 1–77 (1991). https://doi.org/10.1016/0168-0072(91)90065-T

    Article  MathSciNet  MATH  Google Scholar 

  2. Altenkirch, T., Danielsson, N.A., Kraus, N.: Partiality, Revisited. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 534–549. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_31

    Chapter  Google Scholar 

  3. Bahr, P., Grathwohl, H.B., Møgelberg, R.E.: The clocks are ticking: no more delays! In: Proceedings of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pp. 1–12. IEEE Computer Society (2017). https://doi.org/10.1109/LICS.2017.8005097

  4. Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded dependent type theory with coinductive types. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 20–35. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49630-5_2

    Chapter  Google Scholar 

  5. Capretta, V.: General recursion via coinductive types. Log. Methods Comput. Sci. 1(2) (2005). https://doi.org/10.2168/LMCS-1(2:1)2005

  6. Chapman, J., Uustalu, T., Veltri, N.: Quotienting the delay monad by weak bisimilarity. Math. Struct. Comput. Sci. 29(1), 67–92 (2019). https://doi.org/10.1017/S0960129517000184

    Article  MathSciNet  MATH  Google Scholar 

  7. Danielsson, N.A.: Up-to techniques using sized types. Proc. ACM Program. Lang. 2(POPL), 1–28 (2018). https://doi.org/10.1145/3158131

  8. Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103, 235–271 (1992). https://doi.org/10.1016/0304-3975(92)90014-7

    Article  MathSciNet  MATH  Google Scholar 

  9. Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J., Mislove, M., Scott, D.S.: Continuous Lattices and Domains. Cambridge University Press, Cambridge (2003)

    Book  Google Scholar 

  10. Hyland, M., Ong, L.: On full abstraction for PCF: I II and III. Inf. Comput. 163(2), 285–408 (2000). https://doi.org/10.1006/inco.2000.2917

    Article  MathSciNet  MATH  Google Scholar 

  11. Lago, U.D., Gavazzo, F., Levy, P.B.: Effectful applicative bisimilarity: monads, relators, and Howe’s method. In: Proceedings of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pp. 1–12. IEEE Computer Society (2017). https://doi.org/10.1109/LICS.2017.8005117

  12. Levy, P.: Call-by-push-value: decomposing call-by-value and call-by-name. Higher-Order Symb. Comput. 19, 377–414 (2006). https://doi.org/10.1007/s10990-006-0480-6

    Article  MATH  Google Scholar 

  13. Levy, P.B.: Similarity quotients as final coalgebras. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 27–41. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19805-2_3

    Chapter  Google Scholar 

  14. Levy, P., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182–210 (2003). https://doi.org/10.1016/S0890-5401(03)00088-9

    Article  MathSciNet  MATH  Google Scholar 

  15. Milner, R.: Fully abstract models of typed lambda-calculi. Theor. Comput. Sci. 4, 1–22 (1977). https://doi.org/10.1016/0304-3975(77)90053-6

    Article  MATH  Google Scholar 

  16. Møgelberg, R.E., Vezzosi, A.: Two guarded recursive powerdomains for applicative simulation. In: Sokolova, A. (ed.) Proceedings of 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021. Electron. Proceedings in Theoretical Computer Science, vol. 351, pp. 200–217 (2021). https://doi.org/10.4204/EPTCS.351.13

  17. Morris, J.H.: Lambda-calculus models of programming languages, Ph.D. thesis, Massachusetts Institute of Technology (1969). https://dspace.mit.edu/handle/1721.1/64850

  18. Plotkin, G.D.: A powerdomain construction. Siam J. Comput. 5(3), 452–487 (1976). https://doi.org/10.1137/0205035

    Article  MathSciNet  MATH  Google Scholar 

  19. Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223–255 (1977). https://doi.org/10.1016/0304-3975(77)90044-5

    Article  MathSciNet  MATH  Google Scholar 

  20. Plotkin, G.D.: Lambda-definability in the full type hierarchy. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 363–374. Academic Press (1980)

    Google Scholar 

  21. Plotkin, G.D., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001, LNCS, vol. 2030, pp. 1–24 (2001). https://doi.org/10.1007/3-540-45315-6_1

  22. Plotkin, G.D., Pretnar, M.: Handling algebraic effects. Log. Methods Comput. Sci. 9(4), 1–36 (2013). https://doi.org/10.2168/lmcs-9(4:23)2013

  23. Simpson, A., Voorneveld, N.: Behavioural equivalence via modalities for algebraic effects. ACM Trans. Program. Lang. Syst. 42(1), 1–45 (2020). https://doi.org/10.1145/3363518

  24. Thijs, A.M.: Simulation and fixpoint semantics, Ph.D. thesis, University of Groningen (1996). https://research.rug.nl/en/publications/simulation-and-fixpoint-semantics

  25. Uustalu, T.: Stateful runners of effectful computations. Electron. Notes Theor. Comput. Sci. 319, 403–421 (2015). https://doi.org/10.1016/j.entcs.2015.12.024

    Article  MathSciNet  MATH  Google Scholar 

  26. Uustalu, T., Veltri, N.: The delay monad and restriction categories. In: Hung, D.V., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580, pp. 32–50. Springer (2017). https://doi.org/10.1007/978-3-319-67729-3_3

  27. Veltri, N., Vezzosi, A.: Formalizing \(\pi \)-calculus in Guarded Cubical Agda. In: Blanchette, J., Hritcu, C. (eds.) Proceedings of 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 270–283. ACM (2020). https://doi.org/10.1145/3372885.3373814

  28. Veltri, N., Voorneveld, N.F.W.: Inductive and coinductive predicate liftings for effectful programs. In: Sokolova, A. (ed.) Proceedings of 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021. Electronic Proceedings in Theoretical Computer Science, vol. 351, pp. 260–277 (2021). https://doi.org/10.4204/EPTCS.351.16

  29. Veltri, N., van der Weide, N.: Guarded recursion in Agda via sized types. In: Geuvers, H. (ed.) Proceedings of 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019. LIPIcs, vol. 131, pp. 1–19. Dagstuhl Publishing (2019). https://doi.org/10.4230/LIPIcs.FSCD.2019.32

  30. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994). https://doi.org/10.1006/inco.1994.1093

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Software Science, Tallinn University of Technology, Tallinn, Estonia

    Niccoló Veltri & Niels Voorneveld

Authors
  1. Niccoló Veltri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Niels Voorneveld
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Niels Voorneveld .

Editor information

Editors and Affiliations

  1. School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, UK

    Ekaterina Komendantskaya

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Veltri, N., Voorneveld, N. (2022). Streams of Approximations, Equivalence of Recursive Effectful Programs. In: Komendantskaya, E. (eds) Mathematics of Program Construction. MPC 2022. Lecture Notes in Computer Science, vol 13544. Springer, Cham. https://doi.org/10.1007/978-3-031-16912-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-16912-0_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-16911-3

  • Online ISBN: 978-3-031-16912-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation