Abstract
This paper exhibits accurate encodings of the λ-calculus in the π-calculus. The former is canonical for calculation with functions, while the latter is a recent step (Milner et al. 1989) towards a canonical treatment of concurrent processes. With quite simple encodings, two λ-calculus reduction strategies are simulated very closely; each reduction in λ-calculus is mimicked by a short sequence of reductions in π-calculus. Abramsky's precongruence of applicative bisimulation (Abramsky 1989) over λ-calculus is compared with that induced by the encoding of the lazy λ calculus into π-calculus; a similar comparison is made for call-by-value λ-calculus.
| Original language | English |
|---|---|
| Pages (from-to) | 119-141 |
| Number of pages | 23 |
| Journal | Mathematical Structures in Computer Science |
| Volume | 2 |
| Issue number | 2 |
| DOIs | |
| Publication status | Published - Jun 1992 |