Previous Up Next

6  The π-calculus example in more detail

To illustrate another example and how it can be used, consider the implementation of the π-calculus that is contained in the example file pi/pi.def. Of the several things defined in that file, the operational semantics for the π-calculus is given using one-step transitions: for a specific example, see 4.

Beyond the syntactic differences, the operational semantics of λProlog and Bedwyr differ significantly. If a specification is simply a Horn clause program, the two systems coincide. They differ in the operational interpretation of implication: in Bedwyr, to prove AB, all possible ways to prove A are explored and for each answer substitution θ that is found, the goal Bθ is attempted (see 7.5). Bedwyr also contains the ∇-quantifier [MT05].

Listing 4: Some one-step transitions (from examples/pi/pi.def).

Define one : p -> a -> p -> prop, onep : p -> (name -> a) -> (name -> p) -> prop by onep (in X M) (dn X) M; one (out X Y P) (up X Y) P; one (taup P) tau P; one (match X X P) A Q := one P A Q; onep (match X X P) A M := onep P A M;

Listing 5: (Open) bisimulation (from examples/pi/pi.def).

Define coinductive bisim : p -> p -> prop by bisim P Q := (forall A P1, one P A P1 -> exists Q1, one Q A Q1 /\ bisim P1 Q1) /\ (forall X M, onep P (dn X) M -> exists N, onep Q (dn X) N /\ forall w, bisim (M w) (N w)) /\ (forall X M, onep P (up X) M -> exists N, onep Q (up X) N /\ nabla w, bisim (M w) (N w)) /\ (forall A Q1, one Q A Q1 -> exists P1, one P A P1 /\ bisim P1 Q1) /\ (forall X N, onep Q (dn X) N -> exists M, onep P (dn X) M /\ forall w, bisim (M w) (N w)) /\ (forall X N, onep Q (up X) N -> exists M, onep P (up X) M /\ nabla w, bisim (M w) (N w)).

Returning to the example in 4, notice that two predicates are defined: one and onep. The first one relates a process, an action, and a process. The second one relates a process, an abstraction of an action, and an abstraction of a process. The one predicate is used to capture “free transitions” and the “τ-transition” while the second is used to capture bounded transitions. See [TM04, Tiu05] for more details on this encoding strategy for the π-calculus.

5 provides all that is necessary to specify (open) bisimulation for (finite) π-calculus. The keyword coinductive tells the system that it will be attempting to explore a greatest fixed point. That keyword also enables tabling, which avoids redundant computations and accept loops as successes (see 12). The other cases should look natural, at least once one understands the λ-tree approach to representing syntax and the use of the ∇-quantifier. The main thing to point out here is that in the specification, no special side conditions need to be added to the system: all the familiar side conditions from the usual papers on the π-calculus are treated by the implementation of the Bedwyr logic: the user of the system no longer needs to deal with them explicitly but implicitly and declaratively (via quantifier scope, αβη-conversion, etc.).

It is now possible to test some simple examples in the system, for example 6.

Listing 6: Run on examples/pi/pi.def

?= bisim (in a x\ in a y\ z) (in a x\ nu w\ in a y\ out w w z). Yes. More [y] ? y No more solutions. ?= bisim (in a x\ nu y\ match x y (out c c z)) (in a x\ z). Yes. More [y] ? y No more solutions. ?= bisim (nu x\ out a x (in c y\ match x y (out c c z))) (nu x\ out a x (in c y\ z)). No. ?=

These query prove that a(x).a(y).0 and a(x).(ν w).a(y).w!w.0 are bisimilar, that a(x).(ν y).[x=y].c!c.0 and a(x).0 are bisimilar, and that (ν x).a!x.c(y).[x=y].c!c.0 and (ν x).a!x.c(y).0 are not bisimilar.

Several other aspects of the π-calculus are explored in the examples files of the distribution. For example, the file pi/pi_modal.def contains a specification of the modal logics for mobility described in [MPW93], the file pi/corr-assert.def specifies the checking of “correspondence assertions” for the π-calculus as described in [GJ03], and the file pi/pi_abscon.def specifies the polyadic π-calculus following [Mil99].

Previous Up Next