The π-calculus as a theory in linear logic: Preliminary results

Abstract

The agent expressions of the π-calculus can be translated into a theory of linear logic in such a way that the reflective and transitive closure of π-calculus (unlabeled) reduction is identified with “entailedby”. Under this translation, parallel composition is mapped to the multiplicative disjunct (“par”) and restriction is mapped to universal quantification. Prefixing, non-deterministic choice (+), replication (!), and the match guard are all represented using non-logical constants, which are specified using a simple form of axiom, called here a process clause. These process clauses resemble Horn clauses except that they may have multiple conclusions; that is, their heads may be the par of atomic formulas. Such multiple conclusion clauses are used to axiomatize communications among agents. Given this translation, it is nature to ask to what extent proof theory can be used to understand the meta-theory of the π-calculus. We present some preliminary results along this line for π_o, the “propositional” fragment of the π-calculus, which lacks restriction and value passing (π_o is a subset of CCS). Using ideas from proof-theory, we introduce co-agents and show that they can specify some testing equivalences for π_o. If negation-as-failure-to-prove is permitted as a co-agent combinator, then testing equivalence based on co-agents yields observational equivalence for π_o. This latter result follows from observing that co-agents directly represent formulas in the Hennessy-Milner modal logic.