Asynchronous \(\pi \)-calculus at Work: The Call-by-Need Strategy
In a well-known and influential paper  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.
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)”.
- 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
- 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
- 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.Launchbury, J.: A natural semantics for lazy evaluation. In: Proceedings of the 20th POPL. ACM Press (1993)Google Scholar
- 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
- 15.Niehren, J.: Functional computation as concurrent computation. In: Proceedings of the 23th POPL. ACM Press (1996)Google Scholar
- 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
- 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
- 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
- 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.Turner, N.: The polymorphic pi-calculus: theory and implementation. Ph.D. thesis, Department of Computer Science, University of Edinburgh (1996)Google Scholar
- 28.Wadsworth, C.P.: Semantics and pragmatics of the lambda calculus. Ph.D. thesis, University of Oxford (1971)Google Scholar
- 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