Skip to main content
SpringerLink
Log in

Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB

  • Conference paper
Rewriting and Typed Lambda Calculi (RTA 2014, TLCA 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8560))

Abstract

Motivated by the question whether sound and expressive applicative similarities for program calculi with should-convergence exist, this paper investigates expressive applicative similarities for the untyped call-by-value lambda-calculus extended with McCarthy’s ambiguous choice operator amb. Soundness of the applicative similarities w.r.t. contextual equivalence based on may- and should-convergence is proved by adapting Howe’s method to should-convergence. As usual for nondeterministic calculi, similarity is not complete w.r.t. contextual equivalence which requires a rather complex counter example as a witness. Also the call-by-value lambda-calculus with the weaker nondeterministic construct erratic choice is analyzed and sound applicative similarities are provided. This justifies the expectation that also for more expressive and call-by-need higher-order calculi there are sound and powerful similarities for should-convergence.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky, S.: The lazy lambda calculus. In: Turner, D.A. (ed.) Research Topics in Functional Programming, pp. 65–116. Addison-Wesley (1990)

    Google Scholar 

  2. Broy, M.: A theory for nondeterminism, parallelism, communication, and concurrency. Theoret. Comput. Sci. 45, 1–61 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  3. Carayol, A., Hirschkoff, D., Sangiorgi, D.: On the representation of McCarthy’s amb in the pi-calculus. Theoret. Comput. Sci. 330(3), 439–473 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  4. Davey, B., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1992)

    Google Scholar 

  5. Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. J. Log. Algebr. Program. 63(1), 131–173 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  6. Gordon, A.D.: Bisimilarity as a theory of functional programming. Theoret. Comput. Sci. 228(1-2), 5–47 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  7. Howe, D.: Equality in lazy computation systems. In: 4th IEEE Symp. on Logic in Computer Science, pp. 198–203 (1989)

    Google Scholar 

  8. Howe, D.: Proving congruence of bisimulation in functional programming languages. Inform. and Comput. 124(2), 103–112 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  9. Laneve, C.: On testing equivalence: May and must testing in the join-calculus. Technical Report Technical Report UBLCS 96-04, University of Bologna (1996)

    Google Scholar 

  10. Lassen, S.B.: Normal form simulation for McCarthy’s amb. Electr. Notes Theor. Comput. Sci. 155, 445–465 (2006)

    Article  Google Scholar 

  11. Lassen, S.B., Moran, A.: Unique fixed point induction for McCarthy’s amb. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 198–208. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Lassen, S.B., Pitcher, C.S.: Similarity and bisimilarity for countable non-determinism and higher-order functions. Electron. Notes Theor. Comput. Sci. 10 (2000)

    Google Scholar 

  13. Lassen, S.B.: Relational Reasoning about Functions and Nondeterminism. PhD thesis, University of Aarhus (1998)

    Google Scholar 

  14. Levy, P.B.: Amb breaks well-pointedness, ground amb doesn’t. Electron. Notes Theor. Comput. Sci. 173(1), 221–239 (2007)

    Article  Google Scholar 

  15. Mann, M.: Congruence of bisimulation in a non-deterministic call-by-need lambda calculus. Electron. Notes Theor. Comput. Sci. 128(1), 81–101 (2005)

    Article  Google Scholar 

  16. Mann, M., Schmidt-Schauß, M.: Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi. Inform. and Comput. 208(3), 276–291 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  17. Mason, I., Talcott, C.L.: Equivalence in functional languages with effects. J. Funct. Programming 1(3), 287–327 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  18. McCarthy, J.: A Basis for a Mathematical Theory of Computation. In: Braffort, P., Hirschberg, D. (eds.) Computer Programming and Formal Systems, pp. 33–70. North-Holland, Amsterdam (1963)

    Chapter  Google Scholar 

  19. Moran, A.K.D.: Call-by-name, call-by-need, and McCarthy’s Amb. PhD thesis, Chalmers University, Sweden (1998)

    Google Scholar 

  20. Niehren, J., Sabel, D., Schmidt-Schauß, M., Schwinghammer, J.: Observational semantics for a concurrent lambda calculus with reference cells and futures. Electron. Notes Theor. Comput. Sci. 173, 313–337 (2007)

    Article  Google Scholar 

  21. Ong, C.H.L.: Non-determinism in a functional setting. In: Vardi, M.Y. (ed.) Proc. 8th IEEE Symposium on Logic in Computer Science, pp. 275–286. IEEE Computer Society Press (1993)

    Google Scholar 

  22. Pitts, A.M.: Howe’s method for higher-order languages. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction. Cambridge Tracts in Theoretical Computer Science, ch. 5, pp. 197–232. Cambridge University Press (2011)

    Google Scholar 

  23. Rensink, A., Vogler, W.: Fair testing. Inform. and Comput. 205(2), 125–198 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  24. Sabel, D., Schmidt-Schauß, M.: A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci. 18(3), 501–553 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  25. Sabel, D., Schmidt-Schauß, M.: A contextual semantics for Concurrent Haskell with futures. In: Schneider-Kamp, P., Hanus, M. (eds.) Proc. 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pp. 101–112. ACM (2011)

    Google Scholar 

  26. Sabel, D., Schmidt-Schauß, M.: Conservative concurrency in Haskell. In: Dershowitz, N. (ed.) Proc. 27th ACM/IEEE Symposium on Logic in Computer Science (LICS 2012), pp. 561–570. IEEE Computer Society (2012)

    Google Scholar 

  27. Schmidt-Schauß, M., Sabel, D.: Correctness of an STM Haskell implementation. In: Morrisett, G., Uustalu, T. (eds.) Proc. 18th ACM SIGPLAN International Conference on Functional Programming, pp. 161–172. ACM (2013)

    Google Scholar 

  28. Schmidt-Schauß, M., Sabel, D.: Applicative may- and should-simulation in the call-by-value lambda calculus with amb. Frank report 54. Inst. f. Informatik, Goethe-University, Frankfurt (2014), http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-54.pdf

  29. Schmidt-Schauß, M., Sabel, D., Machkasova, E.: Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec. Inf. Process. Lett. 111(14), 711–716 (2011)

    Article  MATH  Google Scholar 

  30. Koutavas, V., Levy, P.B., Sumii, E.: Limitations of applicative bisimulation. In: Modelling, Controlling and Reasoning about State. Dagstuhl Seminar Proceedings, vol. 10351 (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Goethe University, Frankfurt, Germany

    Manfred Schmidt-Schauß & David Sabel

Authors
  1. Manfred Schmidt-Schauß
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Sabel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Inria, 23 avenue d’Italie, CS 81321, 75214, Paris Cedex 13, France

    Gilles Dowek

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Schmidt-Schauß, M., Sabel, D. (2014). Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08918-8_26

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08917-1

  • Online ISBN: 978-3-319-08918-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation