Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn Decidability of the Bisimilarity on Higher-order Processes with Parameterization
129
0
0.0
(
0
)
Added by
EPTCS
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Higher-order processes with parameterization are capable of abstraction and application (migrated from the lambda-calculus), and thus are computationally more expressive. For the minimal higher-order concurrency, it is well-known that the strong bisimilarity (i.e., the strong bisimulation equality) is decidable in absence of parameterization. By contrast, whether the strong bisimilarity is still decidable for parameterized higher-order processes remains unclear. In this paper, we focus on this issue. There are basically two kinds of parameterization: one on names and the other on processes. We show that the strong bisimilarity is indeed decidable for higher-order processes equipped with both kinds of parameterization. Then we demonstrate how to adapt the decision approach to build an axiom system for the strong bisimilarity. On top of these results, we provide an algorithm for the bisimilarity checking.
rate research
Read More
Parameterization extends higher-order processes with the capability of abstraction (akin to that in lambda-calculus), and is known to be able to enhance the expressiveness. This paper focuses on the parameterization of names, i.e. a construct that maps a name to a process, in the higher-order setting. We provide two results concerning its computation capacity. First, name parameterization brings up a complete model, in the sense that it can express an elementary interactive model with built-in recursive functions. Second, we compare name parameterization with the well-known pi-calculus, and provide two encodings between them.
Parameterization extends higher-order processes with the capability of abstraction and application (like those in lambda-calculus). This extension is strict, i.e., higher-order processes equipped with parameterization is computationally more powerful. This paper studies higher-order processes with two kinds of parameterization: one on names and the other on processes themselves. We present two results. One is that in presence of parameterization, higher-order processes can encode first-order (name-passing) processes in a quite neat fashion, in contrast to the fact that higher-order processes without parameterization cannot encode first-order processes at all. In the other result, we provide a simpler characterization of the (standard) context bisimulation for higher-order processes with parameterization, in terms of the normal bisimulation that stems from the well-known normal characterization for higher-order calculus. These two results demonstrate more essence of the parameterization method in the higher-order paradigm toward expressiveness and behavioural equivalence.
This paper studies context bisimulation for higher-order processes, in the presence of parameterization (viz. abstraction). We show that the extension of higher-order processes with process parameterization retains the characterization of context bisimulation by a much simpler form of bisimulation called normal bisimulation (viz. they are coincident), in which universal quantifiers are eliminated; whereas it is not the same with name parameterization. These results clarify further the bisimulation theory of higher-order processes, and also shed light on the essential distinction between the two kinds of parameterization.
Classical Processes (CP) is a calculus where the proof theory of classical linear logic types communicating processes with mobile channels, a la pi-calculus. Its construction builds on a recent propositions as types correspondence between session types and propositions in linear logic. Desirable properties such as type preservation under reductions and progress come for free from the metatheory of linear logic. We contribute to this research line by extending CP with code mobility. We generalise classical linear logic to capture higher-order (linear) reasoning on proofs, which yields a logical reconstruction of (a variant of) the Higher-Order pi-calculus (HOpi). The resulting calculus is called Classical Higher-Order Processes (CHOP). We explore the metatheory of CHOP, proving that its semantics enjoys type preservation and progress (terms do not get stuck). We also illustrate the expressivity of CHOP through examples, derivable syntax sugar, and an extension to multiparty sessions. Lastly, we define a translation from CHOP to CP, which encodes mobility of process code into reference passing.
Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky in 1990. Howe (1989) gave a direct proof that it is a congruence. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name and call-by-value $lambda$-calculus, as well as in a simple non-deterministic variant.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
