The Value-Passing Calculus

摘要

A value-passing calculus is a process calculus in which the contents of communications are values chosen from some data domain, and the propositions appearing in the conditionals are formulas constructed from a logic. Previous studies treat the domain models, as well as the logic theories, as unspecified oracles. The open-ended approach leaves open some fundamental issues unanswered. The paper provides a more formal account of the value-passing calculi. The new treatment is self-contained in that the logic theory a value-passing calculus refers to is formally defined. A value-passing calculus consists of a complete first order theory with an operational model that makes use of the terms and the boolean expressions of the theory. A systematic investigation into the theory of the value-passing calculi is carried out. A particular value-passing calculus, VPC, is shown to be the least expressive among all Turing complete value-passing calculi.