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 A⊃ B, 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].
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:
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.
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
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,
It is now possible to test some simple examples in the system, for example 6.
?= 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].