-
Extensional and Non-extensional Functions as Processes
Authors:
Ken Sakayori,
Davide Sangiorgi
Abstract:
Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure $λ$-calculus, the process representations yield (at best) non-extensional $λ$-theories (i.e., $β$ rule holds, whereas $η$ does not).
In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. U…
▽ More
Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure $λ$-calculus, the process representations yield (at best) non-extensional $λ$-theories (i.e., $β$ rule holds, whereas $η$ does not).
In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal $π$, $\mathrm{I}π$ (a subset of the $π$-calculus in which all outputs are bound), we develop a refinement of Milner's original encoding of functions as processes that is parametric on certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels. We show that when a few algebraic properties of wires hold, the encoding yields a $λ$-theory. Exploiting the symmetries and dualities of $\mathrm{I}π$, we isolate three main classes of wires. The first two have a sequential behaviour and are dual of each other; the third has a parallel behaviour and is the dual of itself. We show the adoption of the parallel wires yields an extensional $λ$-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite $η$. In contrast, the other two classes of wires yield non-extensional $λ$-theories whose equalities are those of the Lévy-Longo and Böhm trees.
△ Less
Submitted 6 May, 2024;
originally announced May 2024.
-
EXPRESSing Session Types
Authors:
Ilaria Castellani,
Ornela Dardha,
Luca Padovani,
Davide Sangiorgi
Abstract:
To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard $π$-calculus by means of a suitable encoding. The encoding allows one to reuse results about the $π$-calculus in the context of session-based communications, thus deepening the understanding of sessions and reducing redundancies in their theoretical…
▽ More
To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard $π$-calculus by means of a suitable encoding. The encoding allows one to reuse results about the $π$-calculus in the context of session-based communications, thus deepening the understanding of sessions and reducing redundancies in their theoretical foundations. Perhaps surprisingly, the encoding has practical implications as well, by enabling refined forms of deadlock analysis as well as allowing session type inference by means of a conventional type inference algorithm.
△ Less
Submitted 13 September, 2023;
originally announced September 2023.
-
Eager Functions as Processes (long version)
Authors:
Adrien Durier,
Daniel Hirschkoff,
Davide Sangiorgi
Abstract:
We study Milner's encoding of the call-by-value $λ$-calculus into the $π$-calculus. We show that, by tuning the encoding to two subcalculi of the $π$-calculus (Internal $π$ and Asynchronous Local $π$), the equivalence on $λ$-terms induced by the encoding coincides with Lassen's eager normalform bisimilarity, extended to handle $η$-equality. As behavioural equivalence in the $π$-calculus we conside…
▽ More
We study Milner's encoding of the call-by-value $λ$-calculus into the $π$-calculus. We show that, by tuning the encoding to two subcalculi of the $π$-calculus (Internal $π$ and Asynchronous Local $π$), the equivalence on $λ$-terms induced by the encoding coincides with Lassen's eager normalform bisimilarity, extended to handle $η$-equality. As behavioural equivalence in the $π$-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.
△ Less
Submitted 7 February, 2022;
originally announced February 2022.
-
Eager Functions as Processes
Authors:
Adrien Durier,
Daniel Hirschkoff,
Davide Sangiorgi
Abstract:
We study Milner's encoding of the call-by-value $λ$-calculus into the $π$-calculus. We show that, by tuning the encoding to two subcalculi of the $π$-calculus (Internal $π$ and Asynchronous Local $π$), the equivalence on $λ$-terms induced by the encoding coincides with Lassen's eager normal-form bisimilarity, extended to handle $η$-equality. As behavioural equivalence in the $π$-calculus we consid…
▽ More
We study Milner's encoding of the call-by-value $λ$-calculus into the $π$-calculus. We show that, by tuning the encoding to two subcalculi of the $π$-calculus (Internal $π$ and Asynchronous Local $π$), the equivalence on $λ$-terms induced by the encoding coincides with Lassen's eager normal-form bisimilarity, extended to handle $η$-equality. As behavioural equivalence in the $π$-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.
△ Less
Submitted 15 December, 2021; v1 submitted 6 December, 2021;
originally announced December 2021.
-
On sequentiality and well-bracketing in the $π$-calculus
Authors:
Daniel Hirschkoff,
Enguerrand Prebet,
Davide Sangiorgi
Abstract:
The $π$-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected. In this paper we focus on two such common disciplines: sequentiality, meaning that at any time there is a single thread of computation, and wel…
▽ More
The $π$-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected. In this paper we focus on two such common disciplines: sequentiality, meaning that at any time there is a single thread of computation, and well-bracketing, meaning that calls to external services obey a stack-like discipline. We formalise the disciplines by means of type systems. The main focus of the paper is on studying the consequence of the disciplines on behavioural equivalence. We define and study labelled bisimilarities for sequentiality and well-bracketing. These relations are coarser than ordinary bisimilarity. We prove that they are sound for the respective (contextual) barbed equivalence, and also complete under a certain technical condition. We show the usefulness of our techniques on a number of examples, that have mainly to do with the representation of functions and store.
△ Less
Submitted 13 December, 2021; v1 submitted 22 April, 2021;
originally announced April 2021.
-
Modular coinduction up-to for higher-order languages via first-order transition systems
Authors:
Jean-Marie Madiot,
Damien Pous,
Davide Sangiorgi
Abstract:
The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions.
We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-o…
▽ More
The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions.
We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.
△ Less
Submitted 16 September, 2021; v1 submitted 20 January, 2020;
originally announced January 2020.
-
Unique Solutions of Contractions, CCS, and their HOL Formalisation
Authors:
Chun Tian,
Davide Sangiorgi
Abstract:
The unique solution of contractions is a proof technique for bisimilarity that overcomes certain syntactic constraints of Milner's "unique solution of equations" technique. The paper presents an overview of a rather comprehensive formalisation of the core of the theory of CCS in the HOL theorem prover (HOL4), with a focus towards the theory of unique solutions of contractions. (The formalisation…
▽ More
The unique solution of contractions is a proof technique for bisimilarity that overcomes certain syntactic constraints of Milner's "unique solution of equations" technique. The paper presents an overview of a rather comprehensive formalisation of the core of the theory of CCS in the HOL theorem prover (HOL4), with a focus towards the theory of unique solutions of contractions. (The formalisation consists of about 20,000 lines of proof scripts in Standard ML.) Some refinements of the theory itself are obtained. In particular we remove the constraints on summation, which must be weakly-guarded, by moving to rooted contraction, that is, the coarsest precongruence contained in the contraction preorder.
△ Less
Submitted 26 August, 2018;
originally announced August 2018.
-
Divergence and unique solution of equations
Authors:
Adrien Durier,
Daniel Hirschkoff,
Davide Sangiorgi
Abstract:
We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS…
▽ More
We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the `up-to techniques'). Finally, we study the theorems in name-passing calculi such as the asynchronous $π$-calculus, and use them to revisit the completeness part of the proof of full abstraction of Milner's encoding of the $λ$-calculus into the $π$-calculus for Lévy-Longo Trees.
△ Less
Submitted 6 August, 2019; v1 submitted 29 June, 2018;
originally announced June 2018.
-
Trees from Functions as Processes
Authors:
Davide Sangiorgi,
Xian Xu
Abstract:
Levy-Longo Trees and Bohm Trees are the best known tree structures on the λ-calculus. We give general conditions under which an encoding of the λ-calculus into the π-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the call-by-name λ-calculus, showing how the two kinds of tree can be obtained by varying the behavioural equivalence adopted…
▽ More
Levy-Longo Trees and Bohm Trees are the best known tree structures on the λ-calculus. We give general conditions under which an encoding of the λ-calculus into the π-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the call-by-name λ-calculus, showing how the two kinds of tree can be obtained by varying the behavioural equivalence adopted in the π-calculus and/or the encoding.
△ Less
Submitted 24 August, 2018; v1 submitted 16 April, 2018;
originally announced April 2018.
-
On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version)
Authors:
Ugo Dal Lago,
Davide Sangiorgi,
Michele Alberti
Abstract:
We study bisimulation and context equivalence in a probabilistic $λ$-calculus. The contributions of this paper are threefold. Firstly we show a technique for proving congruence of probabilistic applicative bisimilarity. While the technique follows Howe's method, some of the technicalities are quite different, relying on non-trivial "disentangling" properties for sets of real numbers. Secondly we s…
▽ More
We study bisimulation and context equivalence in a probabilistic $λ$-calculus. The contributions of this paper are threefold. Firstly we show a technique for proving congruence of probabilistic applicative bisimilarity. While the technique follows Howe's method, some of the technicalities are quite different, relying on non-trivial "disentangling" properties for sets of real numbers. Secondly we show that, while bisimilarity is in general strictly finer than context equivalence, coincidence between the two relations is attained on pure $λ$-terms. The resulting equality is that induced by Levy-Longo trees, generally accepted as the finest extensional equivalence on pure $λ$-terms under a lazy regime. Finally, we derive a coinductive characterisation of context equivalence on the whole probabilistic language, via an extension in which terms akin to distributions may appear in redex position. Another motivation for the extension is that its operational semantics allows us to experiment with a different congruence technique, namely that of logical bisimilarity.
△ Less
Submitted 7 November, 2013;
originally announced November 2013.
-
Light Logics and Higher-Order Processes
Authors:
Ugo Dal Lago,
Simone Martini,
Davide Sangiorgi
Abstract:
We show that the techniques for resource control that have been developed in the so-called "light logics" can be fruitfully applied also to process algebras. In particular, we present a restriction of Higher-Order pi-calculus inspired by Soft Linear Logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that inter…
▽ More
We show that the techniques for resource control that have been developed in the so-called "light logics" can be fruitfully applied also to process algebras. In particular, we present a restriction of Higher-Order pi-calculus inspired by Soft Linear Logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.
△ Less
Submitted 29 November, 2010;
originally announced November 2010.
-
Separability in the Ambient Logic
Authors:
Daniel Hirschkoff,
Etienne Lozes,
Davide Sangiorgi
Abstract:
The \it{Ambient Logic} (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the discriminating power of AL, focusing on the equivalence on processes induced by the logic $(=_L>)$. As underlying calculi besides MA we consider a subcalculus in…
▽ More
The \it{Ambient Logic} (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the discriminating power of AL, focusing on the equivalence on processes induced by the logic $(=_L>)$. As underlying calculi besides MA we consider a subcalculus in which an image-finiteness condition holds and that we prove to be Turing complete. Synchronous variants of these calculi are studied as well. In these calculi, we provide two operational characterisations of $_=L$: a coinductive one (as a form of bisimilarity) and an inductive one (based on structual properties of processes). After showing $_=L$ to be stricly finer than barbed congruence, we establish axiomatisations of $_=L$ on the subcalculus of MA (both the asynchronous and the synchronous version), enabling us to relate $_=L$ to structural congruence. We also present some (un)decidability results that are related to the above separation properties for AL: the undecidability of $_=L$ on MA and its decidability on the subcalculus.
△ Less
Submitted 4 September, 2008; v1 submitted 24 June, 2008;
originally announced June 2008.
-
On the Expressiveness of the Ambient Logic
Authors:
Daniel Hirschkoff,
Etienne Lozes,
Davide Sangiorgi
Abstract:
The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. In this paper, we study the expressiveness of AL. We define formulas for capabilities and for communication in MA. We also derive some formulas that capture finitess of a term, name occurrences and persistence.…
▽ More
The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. In this paper, we study the expressiveness of AL. We define formulas for capabilities and for communication in MA. We also derive some formulas that capture finitess of a term, name occurrences and persistence. We study extensions of the calculus involving more complex forms of communications, and we define characteristic formulas for the equivalence induced by the logic on a subcalculus of MA. This subcalculus is defined by imposing an image-finiteness condition on the reducts of a MA process.
△ Less
Submitted 30 March, 2006; v1 submitted 4 October, 2005;
originally announced October 2005.
