Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Imperative process algebra and models of computation

C. A. Middelburg

TL;DR

The paper investigates whether the imperative process algebra $\textup{ACP}_{\epsilon}^{\tau}$-[2]I can serve as a precise framework for models of computation. It develops RAM-inspired models—RAMP, APRAMP, and SPRAMP—within this algebra, including a probabilistic variant (PrRAMP), and formulates rigorous RAM conditions and complexity measures. It proves that RAMPs align with RAM/Turing computerability, that SPRAMPs satisfy a parallel computation thesis, and that probabilistic models capture complexity classes such as $\mathbf{P}$, $\mathbf{PP}$ and $\mathbf{BPP}$, all within a unified, algebraic formalism. The work delivers a formal, verifiable, process-algebraic lens on computability and complexity for sequential, parallel, and probabilistic computation, enabling rigorous reasoning about computation under data, recursion, and synchronization constraints.

Abstract

Studies of issues related to computability and computational complexity involve the use of a model of computation. Pivotal to such a model are the computational processes considered. Processes of this kind can be described using an imperative process algebra based on ACP (Algebra of Communicating Processes). In this paper, it is investigated whether the imperative process algebra concerned can play a role in the field of models of computation.It is demonstrated that the process algebra is suitable to describe in a mathematically precise way models of computation corresponding to existing models based on sequential, asynchronous parallel, and synchronous parallel random access machines as well as time and work complexity measures for those models. A probabilistic variant of the model based on sequential random access machines and complexity measures for it are also described.

Imperative process algebra and models of computation

TL;DR

The paper investigates whether the imperative process algebra -[2]I can serve as a precise framework for models of computation. It develops RAM-inspired models—RAMP, APRAMP, and SPRAMP—within this algebra, including a probabilistic variant (PrRAMP), and formulates rigorous RAM conditions and complexity measures. It proves that RAMPs align with RAM/Turing computerability, that SPRAMPs satisfy a parallel computation thesis, and that probabilistic models capture complexity classes such as , and , all within a unified, algebraic formalism. The work delivers a formal, verifiable, process-algebraic lens on computability and complexity for sequential, parallel, and probabilistic computation, enabling rigorous reasoning about computation under data, recursion, and synchronization constraints.

Abstract

Studies of issues related to computability and computational complexity involve the use of a model of computation. Pivotal to such a model are the computational processes considered. Processes of this kind can be described using an imperative process algebra based on ACP (Algebra of Communicating Processes). In this paper, it is investigated whether the imperative process algebra concerned can play a role in the field of models of computation.It is demonstrated that the process algebra is suitable to describe in a mathematically precise way models of computation corresponding to existing models based on sequential, asynchronous parallel, and synchronous parallel random access machines as well as time and work complexity measures for those models. A probabilistic variant of the model based on sequential random access machines and complexity measures for it are also described.
Paper Structure (24 sections, 23 theorems, 42 equations, 5 tables)

This paper contains 24 sections, 23 theorems, 42 equations, 5 tables.

Table of Contents

  1. Introduction
  2. The Imperative Process Algebra $\textup{ACP}_\epsilon^\tau$-⁠[2]I
  3. $\textup{ACP}$ with Empty Process and Silent Step
  4. Imperative $\textup{ACP}_\epsilon^\tau$
  5. $\textup{ACP}_\epsilon^\tau$-⁠[2]I with Recursion
  6. Soundness and Completeness Results
  7. Results about the Evaluation Operators
  8. Extensions
  9. Computation and the RAM Conditions
  10. The RAM Conditions
  11. Computing Partial Functions from $(\{ 0,1 \}^*)^n$ to $\{ 0,1 \}^*$
  12. The RAMP Model of Computation
  13. Operators for the RAMP Model
  14. Interpretation of the Operators for the RAMP Model
  15. RAMP Terms and the RAMP Model of Computation
  16. ...and 9 more sections

Key Result

theorem thmcountertheorem

For all terms $t,t' \in \mathcal{P}_\mathsf{rec}$, $t = t'$ is derivable from the axioms of $\textup{ACP}_\epsilon^\tau$-⁠[2]I+ REC+ CFAR only if $t \mathrel{\raisebox{.3ex}{$\underline{\space{\leftrightarrow}\space} _{\space\mathsf{rb}}$}{}} t'$.

Theorems & Definitions (41)

  • theorem thmcountertheorem: Soundness
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • theorem thmcountertheorem: Semi-completeness I
  • theorem thmcountertheorem: Semi-completeness II
  • lemma thmcounterlemma
  • proof
  • theorem thmcountertheorem
  • proof
  • lemma thmcounterlemma
  • ...and 31 more