Advertisement

Asynchronous \(\pi \)-calculus at Work: The Call-by-Need Strategy

  • Davide SangiorgiEmail author
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11760)

Abstract

In a well-known and influential paper [17] Palamidessi has shown that the expressive power of the Asynchronous \(\pi \)-calculus is strictly less than that of the full (synchronous) \(\pi \)-calculus. This gap in expressiveness has a correspondence, however, in sharper semantic properties for the former calculus, notably concerning algebraic laws. This paper substantiates this, taking, as a case study, the encoding of call-by-need \(\lambda \)-calculus into the \(\pi \)-calculus. We actually adopt the Local Asynchronous \(\pi \)-calculus, that has even sharper semantic properties. We exploit such properties to prove some instances of validity of \(\beta \)-reduction (meaning that the source and target terms of a \(\beta \)-reduction are mapped onto behaviourally equivalent processes). Nearly all results would fail in the ordinary synchronous \(\pi \)-calculus. We show that however the full \(\beta \)-reduction is not valid. We also consider a refined encoding in which some further instances of \(\beta \)-validity hold. We conclude with a few questions for future work.

Notes

Acknowledgments

Thanks to the reviewers for their careful reading of the paper and their suggestions. Research partly supported by the H2020-MSCA-RISE project ID 778233 “Behavioural Application Program Interfaces (BEHAPI)”.

References

  1. 1.
    Amadio, R., Castellani, I., Sangiorgi, D.: On bisimulations for the asynchronous \(\pi \)-calculus. Theoret. Comput. Sci. 195, 291–324 (1998)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Ariola, Z., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need \(\lambda \)-calculus. In: Proceedings of the 22th POPL. ACM Press (1995)Google Scholar
  3. 3.
    Boreale, M., Sangiorgi, D.: Some congruence properties for \(\pi \)-calculus bisimilarities. Theoret. Comput. Sci. 198, 159–176 (1998)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Boudol, G.: Some chemical abstract machines. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803, pp. 92–123. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58043-3_18CrossRefGoogle Scholar
  5. 5.
    Brock, S., Ostheimer, G.: Process semantics of graph reduction. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 471–485. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60218-6_36CrossRefGoogle Scholar
  6. 6.
    Durier, A., Hirschkoff, D., Sangiorgi, D.: Eager functions as processes. In: 33nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. IEEE Computer Society (2018)Google Scholar
  7. 7.
    Fournet, C., Gonthier, G.: The join calculus: a language for distributed mobile programming. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 268–332. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45699-6_6CrossRefGoogle Scholar
  8. 8.
    Jeffrey, A.: A chemical abstract machine for graph reduction extended abstract. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 293–303. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58027-1_14CrossRefGoogle Scholar
  9. 9.
    Kobayashi, N., Pierce, B., Turner, D.: Linearity and the pi-calculus. TOPLAS 21(5), 914–947 (1999). Preliminary summary appeared in Proceedings of POPL’96CrossRefGoogle Scholar
  10. 10.
    Lassen, S.B.: Eager normal form bisimulation. In: Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, 26–29 June 2005, pp. 345–354 (2005)Google Scholar
  11. 11.
    Launchbury, J.: A natural semantics for lazy evaluation. In: Proceedings of the 20th POPL. ACM Press (1993)Google Scholar
  12. 12.
    Merro, M., Sangiorgi, D.: On asynchrony in name-passing calculi. J. Math. Struct. Comput. Sci. 14(5), 715–767 (2004)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Milner, R.: The polyadic \(\pi \)-calculus: a tutorial. Technical report, ECS-LFCS-91-180, LFCS, Department of Computer Science, Edinburgh University, October 1991. Also in Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification. Springer, Heidelberg (1991)Google Scholar
  14. 14.
    Milner, R.: Functions as processes. J. Math. Struct. Comput. Sci. 2(2), 119–141 (1992)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Niehren, J.: Functional computation as concurrent computation. In: Proceedings of the 23th POPL. ACM Press (1996)Google Scholar
  16. 16.
    Ostheimer, G., Davie, A.: \(\pi \)-calculus characterisations of some practical \(\lambda \)-calculus reductions strategies. Technical report, CS/93/14, St. Andrews (1993)Google Scholar
  17. 17.
    Palamidessi, C.: Comparing the expressive power of the synchronous and asynchronous pi-calculi. J. Math. Struct. Comput. Sci. 13(5), 685–719 (2003)CrossRefGoogle Scholar
  18. 18.
    Pierce, B.C., Turner, D.N.: Pict: a programming language based on the pi-calculus. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, Cambridge (2000)Google Scholar
  19. 19.
    Plotkin, G.: Call by name, call by value and the \(\lambda \)-calculus. Theoret. Comput. Sci. 1, 125–159 (1975)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Purushothaman, S., Seaman, J.: An adequate operational semantics of sharing in lazy evaluation. In: Krieg-Brückner, B. (ed.) ESOP 1992. LNCS, vol. 582, pp. 435–450. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55253-7_26CrossRefGoogle Scholar
  21. 21.
    Sangiorgi, D.: An investigation into functions as processes. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 143–159. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58027-1_7CrossRefGoogle Scholar
  22. 22.
    Sangiorgi, D.: From \(\lambda \) to \(\pi \), or: Rediscovering continuations. J. Math. Struct. Comput. Sci. 9(4), 367–401 (1999). Special Issue on “Lambda-Calculus and Logic” in Honour of Roger HindleyMathSciNetCrossRefGoogle Scholar
  23. 23.
    Sangiorgi, D.: Lazy functions and mobile processes. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, Cambridge (2000)Google Scholar
  24. 24.
    Sangiorgi, D., Walker, D.: The \(\pi \)-calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  25. 25.
    Sangiorgi, D.: Typed pi-calculus at work: a correctness proof of Jones’s parallelisation transformation on concurrent objects. TAPOS 5(1), 25–33 (1999)Google Scholar
  26. 26.
    Turner, N.: The polymorphic pi-calculus: theory and implementation. Ph.D. thesis, Department of Computer Science, University of Edinburgh (1996)Google Scholar
  27. 27.
    Vasconcelos, V.T.: Lambda and pi calculi, CAM and SECD machines. J. Funct. Program. 15(1), 101–127 (2005)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Wadsworth, C.P.: Semantics and pragmatics of the lambda calculus. Ph.D. thesis, University of Oxford (1971)Google Scholar
  29. 29.
    Yoshida, N.: Optimal reduction in weak lambda-calculus with shared environments. In: Proceedings of the FPCA 1993, Functional Programming and Computer Architecture, pp. 243–252 (1993)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Focus TeamUniversity of Bologna and InriaBolognaItaly

Personalised recommendations