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].

Definecoinductivebisim : p -> p ->propbybisim P Q := (forallA P1, one P A P1 ->existsQ1, one Q A Q1 /\ bisim P1 Q1) /\ (forallX M, onep P (dn X) M ->existsN, onep Q (dn X) N /\forallw, bisim (M w) (N w)) /\ (forallX M, onep P (up X) M ->existsN, onep Q (up X) N /\nablaw, bisim (M w) (N w)) /\ (forallA Q1, one Q A Q1 ->existsP1, one P A P1 /\ bisim P1 Q1) /\ (forallX N, onep Q (dn X) N ->existsM, onep P (dn X) M /\forallw, bisim (M w) (N w)) /\ (forallX N, onep Q (up X) N ->existsM, onep P (up X) M /\nablaw, 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.

?=bisim (in a x\ in a y\ z) (in a x\ nu w\ in a y\ out w w z).Yes.More[y] ? yNo more solutions.?=bisim (in a x\ nu y\ match x y (out c c z)) (in a x\ z).Yes.More[y] ? yNo 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].