We define the type of booleans as bool := (unit chan * unit chan) chan. Then
if we have channel names true ~ unit chan * unit chan and
false ~ unit chan * unit chan in scope, we can define processes which act as
servers on these channels to ensure that &true and &false act as booleans:
true_proc := *$(?true (branches.$(!!(branches·l; <>; 1))))
false_proc := *$(?false(branches.$(!!(branches·r; <>; 1))))
true_proc continually receives pairs of channels and signals on the first of
each pair; false_proc continually receives pairs of channels and signals on
the second of each pair. Thus, we can implement if as
if(cond; th; el) := ν th_chan ~ unit. ν el_chan ~ unit.
$(!!(cond; (&th_chan, &el_chan);
$(?th_chan(_.th) + ?el_chan(_.el))))
This first allocates a channel that should be signalled on if the th branch
should be taken, and one that should be signalled on if the el branch should
be taken. It then sends references to these channels to the process serving via
cond, which will signal back on one of them. Finally, it waits for one of
them to be signalled on, taking the appropriate branch for each case.
We’ll define this for the core calculus given in Sections 39.1–4, and not for
the extensions that introduce sending of values or references—the basic idea
remains the same. Define the P ▷ p translation, along with a version for
events instead of processes, as follows:
$E ▷ p := $(E ▷ p)
1 ▷ p := $(!p; 1)
P ⊗ Q ▷ p := ν c1. ν c2. (P ▷ c1) ⊗ (Q ▷ c2) ⊗ $(?c1; $(?c2; $(!p; 1)))
ν c. P ▷ p := ν c. (P ▷ p)
*P ▷ p := *P
0 ▷ p := !p; 1
E + F ▷ p := (E ▷ p) + (F ▷ p)
?a; P ▷ p := ?a; (P ▷ p)
!a; P ▷ p := !a; (P ▷ p)
The two cases of interest are those for ⊗ and *. In the former case, we
allocate two new channels for the subprocesses to signal their completion on,
and then we wait for both before signalling on p. In the latter case, we
change nothing, because a replicating process does not terminate.
Given this translation, we can define sequential composition as simply
P; Q := ν p. (P ▷ p) ⊗ $(?p; Q)
I.e.: Do P, signalling on p when finished, and in parallel, wait for a
signal on p and then do Q.
I’ll assume for this exercise that our underlying expression language has a
type bool of booleans, rather than using Milner booleans. I’ll also assume a
function nor : bool -> bool -> bool. We will make use of recursive
definitions, but we will always recurse with the same arguments, which allows
particularly simple translation into core PiC in the manner described in
Section 39.3.
Most of the actual statement of the exercise beyond “write a latch” seems kind
of off; for example, the prose descriptions of I_reset and I_set do not
actually match the definitions given, and the second evolution it asks you to
show appears to be wrong. I’ll try to go for something that makes more sense.
I’ll also change the specification to use two channels as inputs rather than
one channel of pairs, to better represent the fact that either of a latch’s
inputs may be independently updated.
Before we can define any gates or latches, we have to consider that there are
several possible approaches to how we can represent a circuit element—most
importantly, should it constantly write an output, or should it only output
upon each input? I’ll go with the former, since it seems to better reflect how
this kind of circuit works—a wire always has a voltage, which can always be
read, rather than only sending an impulse once. To be a bit more precise, say
that a process is in a signalling state for a channel c if there is exactly
one value v such that the process can take the action c ! v, and that it is
in a pre-signalling state for c if it cannot take any action c ! v, but
it can evolve to a signalling state for c in finitely many silent steps.
Say that a channel is an output wire of a process if the process is always
either signalling or pre-signalling on that channel. Then we’ll model a circuit
element with input wires i_1, i_2, ... and output wires o_1, o_2... as a
process P, with the property that whenever a process Q has the is as
output wires, P ⊗ Q has the os as output wires.
We can now define the NOR gate. The process NOR(i1, i2, o) will ensure that
o is a wire whose value is the nor of the values of i1 and i2.
NOR(i1, i2, o) := $(?i1(x.$(?i2(y. $(!o(nor(x)(y); NOR(i1, i2, o)))))))
We can then define the latch L(r, s, q, z) as follows:
L(r, s, q, z) := NOR(r, z, q) ⊗ NOR(s, q, z)
In order to give an example, it will be convenient to define a
“sequence-to-signal” transformer E(seq, sig) which takes a channel outputting
a sequence of values—i.e., one where performing a read causes the sequence
to advance—and writes a signal to the output wire sig—i.e., reading
from sig causes no effect, and sig changes values after a nondeterministic
period of time. The definition requires a recursion with different arguments,
so for maximal clarity, we’ll write down the translation of that part into core
PiC directly.
E(seq, sig) := ν next. $copy1 ⊗ *$(?next(x.$(!sig(x; hold))))
copy1 := ?seq(v.$(!next(v; 1)))
hold := $(!sig(x; hold) + copy1)
It will also be convenient to define a “demuxer” process D(c, cl, cr) which
transforms a pair-of-booleans input wire c into two single-boolean output
wires cl and cr.
D(c, cl, cr) := $(?c(x.$(!cl(x·l; D(c, cl, cr)) + !cr(x·r; D(c, cl, cr)))))
We can now give an example. Here is a demo “driver” process that performs a set and reset.
driver(r, s) := ν rs. ν rs_sig. D(rs_sig, r, s) ⊗ E(rs, rs_sig) ⊗
yield(<false, false>, yield(<true, false>,
yield(<false, true>, *yield(<false, false>, 1))))
yield(v, P) := $(!rs(v; P))
Consider the evolution of driver(r, s) ⊗ L(r, s, q, z). …Actually, don’t.
It’s incredibly verbose. :(
This is pretty simple. We already have non-deterministic choice between events, so we turn that into non-deterministic choice between processes using a receive.
P_1 + P_2 := ν c. $(!c;1) ⊗ $(?c; P_1 + ?c; P_2)
…
…