In a well-known and influential paper [17] Palamidessi has shown that the expressive power of the Asynchronous π -calculus is strictly less than that of the full (synchronous) π -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 λ -calculus into the π -calculus. We actually adopt the Local Asynchronous π -calculus, that has even sharper semantic properties. We exploit such properties to prove some instances of validity of β -reduction (meaning that the source and target terms of a β -reduction are mapped onto behaviourally equivalent processes). Nearly all results would fail in the ordinary synchronous π -calculus. We show that however the full β -reduction is not valid. We also consider a refined encoding in which some further instances of β -validity hold. We conclude with a few questions for future work.

Asynchronous π -calculus at Work: The Call-by-Need Strategy

Sangiorgi D.
2019

Abstract

In a well-known and influential paper [17] Palamidessi has shown that the expressive power of the Asynchronous π -calculus is strictly less than that of the full (synchronous) π -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 λ -calculus into the π -calculus. We actually adopt the Local Asynchronous π -calculus, that has even sharper semantic properties. We exploit such properties to prove some instances of validity of β -reduction (meaning that the source and target terms of a β -reduction are mapped onto behaviourally equivalent processes). Nearly all results would fail in the ordinary synchronous π -calculus. We show that however the full β -reduction is not valid. We also consider a refined encoding in which some further instances of β -validity hold. We conclude with a few questions for future work.
The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday.
33
49
Sangiorgi D.
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 360 kB
Formato Adobe PDF
360 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11585/707530
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact