Calculi for interaction (Q1901716)

Action structures have previously been proposed as an algebra for both the syntax and the semantics of interactive computation. Here, a class of concrete action structures called action calculi is identified, which can serve as a non-linear syntax for a wide variety of models of interactive behaviour. Each action in an action calculus is represented as an assembly of molecules; the syntactic binding of names is the means by which molecules are bound together. A graphical form, action graphs, is used to aid presentation. One action calculus differs from another only in its generators, called controls. Action calculi generalise a previously defined action structure PIC for the pi calculus. Several extensions to PIC are given as action calculi, giving essentially the same power as the pi calculus. An action calculus is also given for the typed lambda calculus, and for Petri nets parametrized on their places and transitions. An equational characterization of action calculi is given: each action calculus \(A\) is the quotient of a term algebra by certain equations. The terms are generated by a set of operators, including those basic to all action structures as well as the controls specific to \(A\); the equations are the basic axioms of action structures together with four additional axiom schemata.