A process calculus with finitary comprehended terms

TL;DR

This paper introduces a new process calculus based on ACP that incorporates meadow-enriched data handling with variable-binding operators, enabling simplified and more compact process representations.

Contribution

It defines meadow enriched ACP process algebras and introduces variable-binding operators for comprehended terms, which can be eliminated to simplify process calculus.

Findings

Variable-binding operators can be eliminated from terms.

The calculus can be interpreted in all meadow enriched ACP process algebras.

Use of variable-binding operators can significantly reduce term size.

Abstract

We introduce the notion of an ACP process algebra and the notion of a meadow enriched ACP process algebra. The former notion originates from the models of the axiom system ACP. The latter notion is a simple generalization of the former notion to processes in which data are involved, the mathematical structure of data being a meadow. Moreover, for all associative operators from the signature of meadow enriched ACP process algebras that are not of an auxiliary nature, we introduce variable-binding operators as generalizations. These variable-binding operators, which give rise to comprehended terms, have the property that they can always be eliminated. Thus, we obtain a process calculus whose terms can be interpreted in all meadow enriched ACP process algebras. Use of the variable-binding operators can have a major impact on the size of terms.