Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userHigher-order Processes with Parameterization over Names and Processes
88
0
0.0
(
0
)
Added by
EPTCS
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Authors
Xian Xu
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
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.
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.
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.
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.
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.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
