Advertisement

A Metalanguage for Guarded Iteration

  • Sergey Goncharov
  • Christoph Rauch
  • Lutz Schröder
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)

Abstract

Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. In recent work, we have introduced an axiomatic notion of guardedness in symmetric monoidal categories, which serves as a unifying framework for various examples from program semantics, process algebra, and beyond. In the present paper, we propose a generic metalanguage for guarded iteration based on combining this notion with the fine-grain call-by-value paradigm, which we intend as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. We give a generic (categorical) semantics of this language over a suitable class of strong monads supporting guarded iteration, and show it to be in touch with the standard operational behaviour of iteration by giving a concrete big-step operational semantics for a certain specific instance of the metalanguage and establishing adequacy for this case.

References

  1. 1.
    Abramsky, S.: Intensionality, definability and computation. In: Baltag, A., Smets, S. (eds.) Johan van Benthem on Logic and Information Dynamics, pp. 121–142. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-06025-5_5CrossRefGoogle Scholar
  2. 2.
    Appel, A.W., Melliès, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: Proceedings of 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 2007, January 2007, Nice, pp. 109–122. ACM Press, New York (2007).  https://doi.org/10.1145/1190216.1190235
  3. 3.
    Benton, N., Kennedy, A.: Exceptional syntax. J. Funct. Program. 11(4), 395–410 (2001).  https://doi.org/10.1017/s0956796801004099MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bergstra, J., Ponse, A., Smolka, S. (eds.): Handbook of Process Algebra. Elsevier, New York City (2001).  https://doi.org/10.1016/b978-0-444-82830-9.x5017-6CrossRefzbMATHGoogle Scholar
  5. 5.
    Birkedal, L., Møgelberg, R., Schwinghammer, J., Støvring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci. 8(4), 1 (2012).  https://doi.org/10.2168/lmcs-8(4:1)2012MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bloom, S., Ésik, Z.: Iteration Theories: The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1993).  https://doi.org/10.1007/978-3-642-78034-9CrossRefzbMATHGoogle Scholar
  7. 7.
    Brookes, S., Van Stone, K.: Monads and comonads in intensional semantics. Technical report CMU-CS-93-140, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA (1993)Google Scholar
  8. 8.
    Carboni, A., Lack, S., Walters, R.: Introduction to extensive and distributive categories. J. Pure. Appl. Algebra 84, 145–158 (1993).  https://doi.org/10.1016/0022-4049(93)90035-rMathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types. Log. Methods Comput. Sci. 12(3), 7 (2016).  https://doi.org/10.2168/lmcs-12(3:7)2016MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Cockett, J.R.B.: Introduction to distributive categories. Math. Struct. Comput. Sci. 3(3), 277–307 (1993).  https://doi.org/10.1017/s0960129500000232MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58085-9_72CrossRefGoogle Scholar
  12. 12.
    Escardó, M.: A metric model of PCF. Paper Presented at Workshop on Realizability Semantics and Applications, June–July 1999, Trento (1999). http://www.cs.bham.ac.uk/~mhe/papers/metricpcf.pdf
  13. 13.
    Geron, B., Levy, P.B.: Iteration and labelled iteration. Electron. Notes Theor. Comput. Sci. 325, 127–146 (2016).  https://doi.org/10.1016/j.entcs.2016.09.035MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Giménez, E.: Codifying guarded definitions with recursive schemes. In: Dybjer, P., Nordström, B., Smith, J. (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60579-7_3CrossRefGoogle Scholar
  15. 15.
    Giménez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 397–408. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0055070CrossRefGoogle Scholar
  16. 16.
    Goncharov, S., Milius, S., Rauch, C.: Complete Elgot monads and coalgebraic resumptions. Electron. Notes Theor. Comput. Sci. 325, 147–168 (2016).  https://doi.org/10.1016/j.entcs.2016.09.036MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Goncharov, S., Rauch, C., Schröder, L.: Unguarded recursion on coinductive resumptions. Electron. Notes Theor. Comput. Sci. 319, 183–198 (2015).  https://doi.org/10.1016/j.entcs.2015.12.012MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Goncharov, S., Schröder, L.: Guarded traced categories. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 313–330. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89366-2_17CrossRefGoogle Scholar
  19. 19.
    Goncharov, S., Schröder, L., Rauch, C., Piróg, M.: Unifying guarded and unguarded iteration. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 517–533. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54458-7_30CrossRefzbMATHGoogle Scholar
  20. 20.
    Hancock, P., Setzer, A.: Guarded induction and weakly final coalgebras in dependent type theory. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics. Oxford Logic Guides, vol. 48, pp. 115–134. Clarendon Press, Oxford (2005)Google Scholar
  21. 21.
    Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1–3), 70–99 (2006).  https://doi.org/10.1016/j.tcs.2006.03.013MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Jones, S.P., et al.: Haskell 98: a non-strict, purely functional language (1999)Google Scholar
  23. 23.
    Krishnaswami, K., Benton, N.: Ultrametric semantics of reactive programs. In: Proceedings of 26th Annual IEEE Symposium on Logic in Computer Science. LICS 2011, June 2011, Toronto, ON, pp. 257–266. IEEE CS Press, Washington, DC (2011).  https://doi.org/10.1109/lics.2011.38
  24. 24.
    Levy, P.B., 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-9MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, New York (1971).  https://doi.org/10.1007/978-1-4612-9839-7CrossRefzbMATHGoogle Scholar
  26. 26.
    Milius, S.: Completely iterative algebras and completely iterative monads. Inf. Comput. 196(1), 1–41 (2005).  https://doi.org/10.1016/j.ic.2004.05.003MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  28. 28.
    Moggi, E.: A modular approach to denotational semantics. In: Pitt, D.H., Curien, P.-L., Abramsky, S., Pitts, A.M., Poigné, A., Rydeheard, D.E. (eds.) CTCS 1991. LNCS, vol. 530, pp. 138–139. Springer, Heidelberg (1991).  https://doi.org/10.1007/BFb0013462CrossRefGoogle Scholar
  29. 29.
    Nakano, H.: A modality for recursion. In: Proceedings of 15th Annual IEEE Symposium on Logic in Computer Science. LICS 2000, June 2000, Santa Barbara, CA, pp. 255–266. IEEE CS Press, Washington, DC (2000).  https://doi.org/10.1109/lics.2000.855774
  30. 30.
    Nakata, K.: Resumption-based big-step and small-step interpreters for While with interactive I/O. In: Danvy, O., Shan, C. (eds.) Proceedings of IFIP Working Conference on Domain-Specific Languages. DSL 2011, Electronic Proceedings in Theoretical Computer Science, September 2011, Bordeaux, vol. 66, pp. 226–235. Open Publishing Association, Sydney (2011).  https://doi.org/10.4204/eptcs.66.12CrossRefGoogle Scholar
  31. 31.
    Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 488–506. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-11957-6_26CrossRefGoogle Scholar
  32. 32.
    Nakata, K., Uustalu, T.: Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction. In: Aceto, L., Sobocinski, P. (eds.) Proceedings of 7th Workshop on Structural Operational Semantics. SOS 2010, Electronic Proceedings in Theoretical Computer Science, August 2010, Paris. vol. 32, pp. 57–75. Open Publishing Association, Sydney (2010).  https://doi.org/10.4204/eptcs.32.5CrossRefGoogle Scholar
  33. 33.
    Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. Log. Methods Comput. Sci. 11(1), 1 (2015).  https://doi.org/10.2168/lmcs-11(1:1)2015MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Plotkin, G., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 1–24. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45315-6_1CrossRefGoogle Scholar
  35. 35.
    Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symb. Log. 32(2), 198–212 (1967).  https://doi.org/10.2307/2271658MathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Proceedings of 12th Annual IEEE Symposium on Logic in Computer Science. LICS 1997, June–July 1997, Warsaw, pp. 280–291. IEEE CS Press, Washington, DC (1997).  https://doi.org/10.1109/lics.1997.614955
  37. 37.
    Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Sergey Goncharov
    • 1
  • Christoph Rauch
    • 1
  • Lutz Schröder
    • 1
  1. 1.Dept. InformatikFriedrich-Alexander-Universität Erlangen-NürnbergErlangenGermany

Personalised recommendations