When using the implementation from the Fudget library,p :: SP (Either a b) (Either a b) p = idSP -+- idSP
p
is nothing but the identity stream processor for type Either a b. But if we were to use
indeterministic stream processors, we cannot be sure that
message order would be maintained through p. If we first
send Left a immediately followed by Right
b to p, why should there be a guarantee that it
will output these messages in the same order?
Naturally, the Fudget library does not have a lot of identity
stream processors in parallel. Fudgets, on the other side, are
abundant in the library, and they very often sit in
parallel. One example where implicit assumptions exist about
message order output from parallel fudgets is in the radio group
fudget radioF. Another, more explicit, assumption was
made in the implementation of the Explode game in
Section 38.1.1. In Explode, it is crucial that the
internal communication after a explosion has priority over
external communication. This is what the continuation-based
implementation of stream processors gives.
In order to reason formally about indeterministic stream processors, we present the stream-processor calculus (SP-calculus).
For the reader who has used stream processors in the Fudget library, these operators should be familiar. The operator ! correspond to
x (Variable) s ! t (Put) x ? s (Get) s <· t (Feed) s << t (Serial composition) s +t(Parallel composition) l s (Loop)
putSP, and ? can be
seen as a combination of abstraction and getSP: x ? s is
the same as getSP (\x -> s). The feed operator in
s <· t feeds the message t to the stream processor s
(similar to startupSP, which feeds a list of messages to a
stream processor). Serial composition corresponds to -==-, and parallel composition and loop are untagged,
corresponding to -*- and loopSP.
s +t=== t +s(Commutativity of +)(s +t)+u=== s +(t+u)(Associativity of +)(s << t) << u === s << (t << u) (Associativity of <<) s << (t ! u) === (s <· t) << u (Internal communication in <<) (s +t) <· u=== (s <· u) +(t <· u)(Distributivity of <· over +)(s ! t) <· u === s ! (t <· u) (Output from <·) (s ! t) << u === s ! (t << u) (Output from <<) (x ? s) <· t === s[t/x] (Substitution)
We can derive a symmetric rule by using the commutativity of
(s ! t) +u--> s ! (t +u)((Output from +))
+, but when it comes to the loop, we need two rules.As an example of these rules, consider the stream processor (s ! t)
l (s ! t) --> s ! l (t <· s) (Internal input to l) (l s) <· t --> l (s <· t) (External input to l)
+ (u ! v), which can react to s ! (t + (u ! v)), but also
to u ! ((s ! t) + v), using commutativity. Similarly, the loop
(l (s ! t)) <· u can react to both s ! l (t <· s) <· u
and l (s ! t <· u).The substitution rule for the SP-calculus correspond to the beta-rule of \-calculus. However the eta-rule, which would correspond to x ? (s <· x) === s, does not hold in general, something that we will see after having defined equivalence of stream processors.
[[x]] = x (Variable) [[\x.M]] = x ? [[M]] (Abstraction) [[M N]] = [[M]] <· [[N]] (Application)
Having the power of \-calculus, we can define some familiar stream processors, such as the identity stream processor and the null stream processor.
fix = f ? (x ? f <· (x <· x)) <· (x ? f <· (x <· x)) id = fix <· (f ? x ? x ! f) 0 = fix <· (f ? x ? f)
s1 === s2 if and only if:
There is also an interest in having programs running for a while at one site, then moving on to other sites, while gathering information etc. Such programs are often called mobile agents. As we have seen in Chapter 25, the necessary machinery for mobile agent programming is already there in the stream-processor concept. However, we need support in the underlying language implementation so that values that are closures can be exchanged between computers.