| Issue |
RAIRO-Theor. Inf. Appl.
Volume 53, Number 3-4, July–December 2019
|
|
|---|---|---|
| Page(s) | 153 - 206 | |
| DOI | https://doi.org/10.1051/ita/2019005 | |
| Published online | 10 January 2020 | |
Parameterizing higher-order processes on names and processes*,**
East China University of Science and Technology,
Shanghai
200237, PR China.
*** Corresponding author: xuxian2004@gmail.com
Received:
23
August
2018
Accepted:
15
November
2019
Parameterization extends higher-order processes with the capability of abstraction and application (like those in lambda-calculus). As is well-known, this extension is strict, meaning that higher-order processes equipped with parameterization are strictly more expressive than those without parameterization. This paper studies strictly higher-order processes (i.e., no name-passing) with two kinds of parameterization: one on names and the other on processes themselves. We present two main results. One is that in presence of parameterization, higher-order processes can interpret first-order (name-passing) processes in a quite elegant fashion, in contrast to the fact that higher-order processes without parameterization cannot encode first-order processes at all. We present two such encodings and analyze their properties in depth, particularly full abstraction. In the other result, we provide a simpler characterization of the standard context bisimilarity for higher-order processes with parameterization, in terms of the normal bisimilarity that stems from the well-known normal characterization for higher-order calculus. As a spinoff, we show that the bisimulation up-to context technique is sound in the higher-order setting with parameterization.
Mathematics Subject Classification: 68Q05 / 68Q10 / 68Q85
Key words: Parameterization / encoding / context bisimulation / normal bisimulation / higher-order / first-order / processes
A preliminary version of this work was presented at EXPRESS/SOS 2016. This paper revises and extends that version with full-fledged proofs and more refined discussions (at least more than half new materials), and moreover, the detailed analysis of a variant encoding of interest. This encoding, mentioned only as a further direction in the preliminary version, is given thorough examination in this work.
© EDP Sciences, 2020
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.