Higher-order Processes with Parameterization over Names and Processes

TL;DR

This paper explores higher-order processes extended with parameterization over names and processes, demonstrating increased expressiveness and providing simpler behavioral equivalence characterizations.

Contribution

It introduces parameterization in higher-order processes, enabling encoding of first-order processes and simplifying bisimulation characterization.

Findings

Higher-order processes with parameterization can encode first-order processes.

A simpler normal bisimulation characterization is provided.

Parameterization enhances expressiveness and behavioral analysis.

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.