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

x(Variable) s!t(Put) x?s(Get) s<·t(Feed) s<<t(Serial composition) s`+`

t(Parallel composition) ls(Loop)

`putSP`

, and `getSP`

: `getSP (\`*x* -> *s*)

. The feed operator in
`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 (

(ls!t)--> s!(lt<·s)(Internal input to )l( ls)<·t--> (ls<·t)(External input to )l

`+`

(`+`

(`+`

The substitution rule for the SP-calculus correspond to the beta-rule of \-calculus. However the eta-rule, which would correspond to

[[ x]]= x(Variable) [[\ x.M]]= x?[[M]](Abstraction) [[ MN]]= [[ 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)

*s _{1}* ===

- For all
*o*and_{1}*s'*that_{1}*s*can output and become, there must exist an_{1}*o*and_{2}*s'*that_{2}*s*can output and become. Furthermore,_{2}*o*===_{1}*o*and_{2}*s'*===_{1}*s'*must hold._{2} - For all input
*t*,*s*_{1}**<·***t*===*s*_{2}**<·***t*must hold.

- Check that we have exactly the congruence/reaction rules we need.
- Check that the congruence rules form a decidable relation. It must be possible to find all possible reactions in a stream processor.
- The equivalence relation is good, but we really want to find a congruence relation.
- Relate the SP-calculus to other calculi so that we can reuse their theory.

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.