I already argued that streams are not general enough to represent communication between processes, but let's keep the model simple.
Function from stream to stream fails to represent one crucial property of the process - which input message must have been fed to the process in order to observe a specific output message. I do not mean data dependency here, but something like control dependency, or causality. Streams (or full orders) are a special case of partial orders that can be used to model causality, so there seems everything is ok - except there is no ordering between elements of input stream and output stream.
Imagine a function from stream of unit to stream of unit:
data Stream a = Message a (Stream a)
type X = (Stream ()) -> (Stream ())
There is just one function of type X - identity (non-termination is out of equation as we are talking math functions, not Haskell functions).
On the other hand, there are multiple different behaviors that accept empty messages and output empty messages.
One would be an identity behavior - for each input message send one output message. Another would be a counter - for nth input message send n output messages. By applying a function from Nat to Nat to the definition of the counter, one obtains a new behavior: for nth input message send f(n) output messages. Thus there are infinitely many observably different behaviors of this type, and trying to denote them by a single function is unsatisfactory at least.
So, the quick solution seems to define a process as a function from input list (a prefix of stream) to a list of outputs produced after receiving the last input (so the whole output list is obtained by concatenating output lists for all prefixes of the input). This may work for a single input stream, but for multiple streams we need to encode which stream received the last message.
A more general way to look onto this is to say that a process extends a partially ordered set of input messages to a partially ordered set of both input and output messages, with a constraint that it does not introduce PO links to an input message (but obviously is allowed to introduce such links from an input to an output, or between two outputs).
Need to think of a formal (and elegant) way for saying this.
9 comments:
I may want to express Join Calculus (http://citeseer.ist.psu.edu/cache/papers/cs/31709/http:zSzzSzresearch.microsoft.comzSz~fournetzSzpaperszSzjoin-tutorial.pdf/fournet00join.pdf) semantics in "cobs" instead of usual rCHAM.
Cobs are more general, as they handle any algebraic data structure, not just lists, as their "streams". Also, cobs do not use imperative identity of processes, but append-only exptension of "trace", with active cobs representing the current state of affairs. This, BTW, might prove more powerful to model termination of processes.
Before proceeding further, I need to address the usual problem - communication via futures is fine until a single consumer needs to be connected to multiple independent producers.
CCP solves this problem in one way, I might consider some other (probably the fact that cobs operate with more general notion that streams may help).
Actually, LMNtal looks quite similar to my idea of cobs, have to look closer into this paper (http://citeseer.ist.psu.edu/564720.html).
Also need to find an explanation of what to do with abandoned futures, or rather, with the cobs that depend on their values.
And, of course, more reading on Guarded Horn Clauses is needed.
Define operational semantics for graphs, then introduce textual syntax.
Probably use mutual "let", then see if mixins are possible.
Finally, introduce resources.
Oops, almost forgot to mention Petri Nets.
Post a Comment