Eager Functions as Processes (long version)

TL;DR

This paper explores how specific encodings of the call-by-value lambda calculus into the pi-calculus can align behavioral equivalences, using advanced techniques like unique solutions of equations to analyze expressiveness.

Contribution

It demonstrates that tuning the encoding to certain pi-calculus variants aligns lambda calculus equivalences with pi-calculus behavioral equivalences, extending the technique of unique solutions of equations.

Findings

Encoding tuning aligns lambda and pi-calculus equivalences.

Extended the technique of unique solutions of equations.

Provided a case study on the technique's applicability.

Abstract

We study Milner's encoding of the call-by-value $\lambda$-calculus into the $\pi$-calculus. We show that, by tuning the encoding to two subcalculi of the $\pi$-calculus (Internal $\pi$ and Asynchronous Local $\pi$), the equivalence on $\lambda$-terms induced by the encoding coincides with Lassen's eager normalform bisimilarity, extended to handle $\eta$-equality. As behavioural equivalence in the $\pi$-calculus we consider contextual equivalence and barbed congruence. We also extend the results to preorders. A crucial technical ingredient in the proofs is the recently-introduced technique of unique solutions of equations, further developed in this paper. In this respect, the paper also intends to be an extended case study on the applicability and expressiveness of the technique.