Advertisement

A Complete, Co-inductive Syntactic Theory of Sequential Control and State

  • Kristian Støvring
  • Soren B. Lassen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5700)

Abstract

We present a co-inductive syntactic theory, eager normal form bisimilarity, for the untyped call-by-value lambda calculus extended with continuations and mutable references.

We demonstrate that the associated bisimulation proof principle is easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs.

The theory is modular in the sense that eager normal form bisimilarity for each of the calculi extended with continuations and/or mutable references is a fully abstract extension of eager normal form bisimilarity for its sub-calculi. For each calculus, we prove that eager normal form bisimilarity is a congruence and is sound with respect to contextual equivalence. Furthermore, for the calculus with both continuations and mutable references, we show that eager normal form bisimilarity is complete: it coincides with contextual equivalence.

Eager normal form bisimilarity is inspired by Böhm-tree equivalence in the pure lambda calculus. We clarify the associated proof principle by reviewing properties of Böhm trees and surveying previous work on normal form bisimulation.

Keywords

Normal Form Sequential Control Annual IEEE Symposium Syntactic Theory Lambda Calculus 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abramsky, S.: The lazy lambda calculus. In: Turner, D. (ed.) Research Topics in Functional Programming, pp. 65–116. Addison-Wesley, Reading (1990)Google Scholar
  2. 2.
    Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: Pratt, V. (ed.) Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, June 1998, pp. 334–344. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  3. 3.
    Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the Thirty-Sixth Annual ACM Symposium on Principles of Programming Languages, pp. 340–353. ACM Press, New York (2009)Google Scholar
  4. 4.
    Ahmed, A.J.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft [56], pp. 69–83Google Scholar
  5. 5.
    Appel, A.W., McAllester, D.A.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems 23(5), 657–683 (2001)CrossRefGoogle Scholar
  6. 6.
    Ariola, Z.M., Herbelin, H.: Minimal classical logic and control operators. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 871–885. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundation of Mathematics, vol. 103. North-Holland, Amsterdam (1984) (revised edn.)zbMATHGoogle Scholar
  8. 8.
    Bierman, G.M.: A computational interpretation of the λμ-calculus. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 336–345. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 9.
    Boudol, G.: On the semantics of the call-by-name CPS transform. Theoretical Computer Science 234(1–2), 309–321 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Research Report BRICS RS-04-26, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark (November 2004); A preliminary version appears in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science, vol. 59.4Google Scholar
  11. 11.
    David, R., Py, W.: λμ-calculus and Böhm’s theorem. Journal of Symbolic Logic 66(1), 407–413 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    de Groote, P.: On the relation between the lambda-mu-calculus and the syntactic theory of sequential control. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 31–43. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  13. 13.
    Egidi, L., Honsell, F., Ronchi della Rocca, S.: Operational, denotational and logical descriptions: a case study. Fundamenta Informaticae 16(2), 149–169 (1992)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Felleisen, M.: λ-v-CS: An extended λ-calculus for scheme. In: Proceedings of the 1988 ACM Conference on LISP and Functional Programming, pp. 72–85 (1988)Google Scholar
  15. 15.
    Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science 103, 235–271 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Friedman, D.P., Haynes, C.T.: Constraining control. In: Deusen, M.S.V., Galil, Z. (eds.) Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, January 1985, pp. 245–254. ACM Press, New York (1985)Google Scholar
  17. 17.
    Gordon, A.D.: Bisimilarity as a theory of functional programming. Theoretical Computer Science 228(1–2), 5–47 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Gordon, A.D., Pitts, A.M. (eds.): Higher Order Operational Techniques in Semantics. Publications of the Newton Institute, Cambridge University Press (1998)Google Scholar
  19. 19.
    Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Information and Computation 124(2), 103–112 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bulletin of the European Association for Theoretical Computer Science 62, 222–259 (1997)zbMATHGoogle Scholar
  21. 21.
    Jagadeesan, R., Pitcher, C., Riely, J.: Open bisimulation for aspects (2009) (Long version, to appear)Google Scholar
  22. 22.
    Kelsey, R., Clinger, W., Rees, J. (eds.): Revised5 report on the algorithmic language Scheme. Higher-Order and Symbolic Computation 11(1), 7–105 (1998)CrossRefGoogle Scholar
  23. 23.
    Koutavas, V., Wand, M.: Bisimulations for untyped imperative objects. In: Sestoft [56], pp. 146–161Google Scholar
  24. 24.
    Koutavas, V., Wand, M.: Reasoning about class behavior. In: FOOL/WOOD 2007 Workshop (January 2007)Google Scholar
  25. 25.
    Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: Peyton Jones, S. (ed.) Proceedings of the Thirty-Third Annual ACM Symposium on Principles of Programming Languages, Charleston, South Carolina, January 2006. SIGPLAN Notices, vol. 41(1), pp. 141–152. ACM Press, New York (2006)Google Scholar
  26. 26.
    Laird, J.: Full abstraction for functional languages with control. In: Winskel, G. (ed.) Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 1997, pp. 58–67. IEEE Computer Society Press, Los Alamitos (1997)CrossRefGoogle Scholar
  27. 27.
    Laird, J.: A fully abstract trace semantics for general references. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 667–679. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  28. 28.
    Landin, P.J.: The mechanical evaluation of expressions. The Computer Journal 6(4), 308–320 (1964)CrossRefzbMATHGoogle Scholar
  29. 29.
    Lassen, S.B.: Bisimulation up to context for imperative lambda calculus. Unpublished note. Presented at The Semantic Challenge of Object-Oriented Programming, Schloss Dagstuhl (1998)Google Scholar
  30. 30.
    Lassen, S.B.: Eager normal form bisimulation. In: Panangaden, P. (ed.) Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science, June 2005, pp. 345–354. IEEE Computer Society Press, Los Alamitos (2005)Google Scholar
  31. 31.
    Lassen, S.B.: Normal form simulation for McCarty’s amb. In: Escardó, M., Jung, A., Mislove, M. (eds.) Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), May 2005. Electronic Notes in Theoretical Computer Science, vol. 155, pp. 445–465. Elsevier Science Publishers, Amsterdam (2005)Google Scholar
  32. 32.
    Lassen, S.B.: Head normal form bisimulation for pairs and the λμ-calculus (extended abstract). In: Alur, R. (ed.) Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science, August 2006, pp. 297–306. IEEE Computer Society Press, Los Alamitos (2006)Google Scholar
  33. 33.
    Lassen, S.B.: Relational reasoning about contexts. In: Gordon and Pitts [18], pp. 91–135Google Scholar
  34. 34.
    Lassen, S.B.: Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. In: Brookes, S., Jung, A., Mislove, M., Scedrov, A. (eds.) Proceedings of the 15th Annual Conference on Mathematical Foundations of Programming Semantics, April 1999. Electronic Notes in Theoretical Computer Science, vol. 20, pp. 346–374. Elsevier Science Publishers, Amsterdam (1999)Google Scholar
  35. 35.
    Lassen, S.B., Levy, P.B.: Typed normal form bisimulation. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 283–297. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  36. 36.
    Lassen, S.B., Levy, P.B.: Typed normal form bisimulation for parametric polymorphism. In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, pp. 341–352. IEEE Computer Society Press, Los Alamitos (2008)Google Scholar
  37. 37.
    Levy, P.B.: Game semantics using function inventories. Talk given at Geometry of Computation 2006, Marseille (2006)Google Scholar
  38. 38.
    Mason, I.A., Talcott, C.L.: Equivalence in functional languages with effects. Journal of Functional Programming 1(3), 297–327 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  39. 39.
    Merro, M., Biasi, C.: On the observational theory of the CPS-calculus (extended abstract). In: Brookes, S., Mislove, M. (eds.) Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXII), May 2006. Electronic Notes in Theoretical Computer Science, vol. 158, pp. 307–330. Elsevier Science Publishers, Amsterdam (2006)Google Scholar
  40. 40.
    Meyer, A.R., Sieber, K.: Towards fully abstract semantics for local variables: Preliminary report. In: Ferrante, J., Mager, P. (eds.) Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, January 1988, pp. 157–169. ACM Press, New York (1988)Google Scholar
  41. 41.
    Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press, Cambridge (1997)Google Scholar
  42. 42.
    Mosses, P.D.: Component-based description of programming languages. In: Visions of Computer Science, Proc. BCS International Academic Research Conference, pp. 275–286. BCS, London (2008)Google Scholar
  43. 43.
    Mosses, P.D.: Action Semantics. Cambridge Tracts in Theoretical Computer Science, vol. (26). Cambridge University Press, Cambridge (1992)CrossRefzbMATHGoogle Scholar
  44. 44.
    Mosses, P.D.: Theory and practice of action semantics. In: Penczek, W., Szałas, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 37–61. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  45. 45.
    Parigot, M.: λμ-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  46. 46.
    Perez, R.P.: An extensional partial combinatory algebra based on λ-terms. In: Tarlecki, A. (ed.) MFCS 1991. LNCS, vol. 520, pp. 387–396. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  47. 47.
    Pitts, A.M.: Reasoning about local variables with operationally-based logical relations. In: O’Hearn, P.W., Tennent, R.D. (eds.) Algol-Like Languages, ch. 17, vol. 2, pp. 173–193. Birkhauser, Basel (1997); Reprinted from Proceedings Eleventh Annual IEEE Symposium on Logic in Computer Science, pp. 152–163 (1996)Google Scholar
  48. 48.
    Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Gordon and Pitts [18], pp. 227–273Google Scholar
  49. 49.
    Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 125–159 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  50. 50.
    Ritter, E., Pitts, A.M.: A fully abstract translation between a λ-calculus with reference types and Standard ML. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 397–413. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  51. 51.
    Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh (1992); LFCS report ECS-LFCS-93-266 (also published as CST-99-93)Google Scholar
  52. 52.
    Sangiorgi, D.: A theory of bisimulation for the pi-calculus. Acta Informatica 33, 69–97 (1996), ftp://ftp-sop.inria.fr/mimosa/personnel/davides/sub.ps.gz MathSciNetCrossRefzbMATHGoogle Scholar
  53. 53.
    Sangiorgi, D.: Lazy functions and mobile processes. In: Proof, language, and interaction: essays in honour of Robin Milner, pp. 691–720. MIT Press, Cambridge (2000)Google Scholar
  54. 54.
    Sangiorgi, D.: The lazy lambda calculus in a concurrency scenario. Information and Computation 111(1), 120–153 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  55. 55.
    Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: Ong, C.L. (ed.) Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science, Wroclaw, Poland, July 2007, pp. 293–302. IEEE Computer Society Press, Los Alamitos (2007)Google Scholar
  56. 56.
    Sestoft, P. (ed.): ESOP 2006. LNCS, vol. 3924. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  57. 57.
    Støvring, K.: On Reasoning Equationally: Lambda Calculi and Programs with Computational Effects. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (August 2007)Google Scholar
  58. 58.
    Støvring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequential control and state. In: Felleisen, M. (ed.) Proceedings of the Thirty-Fourth Annual ACM Symposium on Principles of Programming Languages, Nice, France, January 2007. SIGPLAN Notices, vol. 42(1), pp. 161–172. ACM Press, New York (2007)Google Scholar
  59. 59.
    Sumii, E.: A theory of non-monotone memory (or: Contexts for free). In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 237–251. Springer, Heidelberg (2009)Google Scholar
  60. 60.
    Sumii, E.: A complete characterization of observational equivalence in polymorphic lambda-calculus with general references (manuscript) (January 2009)Google Scholar
  61. 61.
    Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. In: Abadí, M. (ed.) Proceedings of the Thirty-Second Annual ACM Symposium on Principles of Programming Languages, Long Beach, California, January 2005. SIGPLAN Notices, vol. 40(1), pp. 63–74. ACM Press, New York (2005)Google Scholar
  62. 62.
    Talcott, C.: Reasoning about functions with effects. In: Gordon and Pitts [18], pp. 347–390Google Scholar
  63. 63.
    Vytiniotis, D., Koutavas, V.: Relating step-indexed logical relations and bisimulations. Technical Report MSR-TR-2009-25, Microsoft Research, Cambridge (March 2009)Google Scholar
  64. 64.
    Wand, M., Sullivan, G.T.: Denotational semantics using an operationally-based term model. In: Jones, N.D. (ed.) Proceedings of the Twenty-Fourth Annual ACM Symposium on Principles of Programming Languages, France, January 1997, pp. 386–399. ACM Press, New York (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Kristian Støvring
    • 1
  • Soren B. Lassen
    • 2
  1. 1.IT University of CopenhagenDenmark
  2. 2.Google Inc.Mountain ViewUSA

Personalised recommendations