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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abramsky, S.: The lazy lambda calculus. In: Turner, D.A. (ed.) Research Topics in Functional Programming, pp. 65–116. Addison-Wesley (1990)
Broy, M.: A theory for nondeterminism, parallelism, communication, and concurrency. Theoret. Comput. Sci. 45, 1–61 (1986)
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)
Davey, B., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1992)
Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. J. Log. Algebr. Program. 63(1), 131–173 (2005)
Gordon, A.D.: Bisimilarity as a theory of functional programming. Theoret. Comput. Sci. 228(1-2), 5–47 (1999)
Howe, D.: Equality in lazy computation systems. In: 4th IEEE Symp. on Logic in Computer Science, pp. 198–203 (1989)
Howe, D.: Proving congruence of bisimulation in functional programming languages. Inform. and Comput. 124(2), 103–112 (1996)
Laneve, C.: On testing equivalence: May and must testing in the join-calculus. Technical Report Technical Report UBLCS 96-04, University of Bologna (1996)
Lassen, S.B.: Normal form simulation for McCarthy’s amb. Electr. Notes Theor. Comput. Sci. 155, 445–465 (2006)
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)
Lassen, S.B., Pitcher, C.S.: Similarity and bisimilarity for countable non-determinism and higher-order functions. Electron. Notes Theor. Comput. Sci. 10 (2000)
Lassen, S.B.: Relational Reasoning about Functions and Nondeterminism. PhD thesis, University of Aarhus (1998)
Levy, P.B.: Amb breaks well-pointedness, ground amb doesn’t. Electron. Notes Theor. Comput. Sci. 173(1), 221–239 (2007)
Mann, M.: Congruence of bisimulation in a non-deterministic call-by-need lambda calculus. Electron. Notes Theor. Comput. Sci. 128(1), 81–101 (2005)
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)
Mason, I., Talcott, C.L.: Equivalence in functional languages with effects. J. Funct. Programming 1(3), 287–327 (1991)
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)
Moran, A.K.D.: Call-by-name, call-by-need, and McCarthy’s Amb. PhD thesis, Chalmers University, Sweden (1998)
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)
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)
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)
Rensink, A., Vogler, W.: Fair testing. Inform. and Comput. 205(2), 125–198 (2007)
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)
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)
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)
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)
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
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)
Koutavas, V., Levy, P.B., Sumii, E.: Limitations of applicative bisimulation. In: Modelling, Controlling and Reasoning about State. Dagstuhl Seminar Proceedings, vol. 10351 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)