Talk:Algebra of communicating processes

A couple of questions. In your example of $|$ what exactly happens with that communicated information? Does it get passed to y (it appears not), or is it a matter of possibly having some action s(d) that reads and then does something with what it reads... or...? The others seem clear to me, but this operator is not at all so.

I'm also curious as to how $\tau$ interacts with things. You don't mention it in the axioms at all. Would it be sufficiently nicely behaved so as to let $a\cdot \tau =\tau \cdot a=a$? That would make $(S,+,\cdot )$ a straight semiring. Proably too much to hope for.

One final thing - in the axioms you have the statement $ax||y=a(x||y)$ but $ax$ isn't really defined. Is it an implcit $a\cdot x$ where the $\cdot$ is dropped? If so I would suggest putting it in as it is clearer in terms of the defined operations, or providing a note somewhere earlier regarding the dropping of $\cdot$ as is often the case in classical algebra. Leland McInnes 07:07, 10 January 2006 (UTC)

On communications: my understanding is that instances of the free variable 'd' in 'y' get replaced with the value '1', so yes, the value does get passed to 'y'. I agree that the example doesn't make that very clear as it stands. I'll see about adding some further clarification.

I haven't had time to add anything on $\tau$ yet. Fear not! There are relevant axioms. But $\tau$ is involved in abstraction, which I haven't said anything about yet, so I haven't got around to listing the axioms. I'm learning ACP as I write this, so the going is a bit slow.

Nice catch on the statement $ax||y=a(x||y)$. There should indeed be sequencing operators in there. I inadvertently left them out - I'll try to insert them sometime tomorrow.

Thanks for the feedback, and the help! --Allan McInnes 09:02, 10 January 2006 (UTC)

Re $a\cdot \tau =\tau \cdot a=a$: I don't believe that this holds. My understanding is that $\tau \cdot a=a$, but that $a\cdot \tau \neq a$ $a\cdot \tau =a$, but that $\tau \cdot a\neq a$ due to interactions between $\tau$ and the $+$ operator. However, I may not fully understand what is going on. If you're interested, ACP_τ: A Universal Axiom System for Process Specification provides an explanation of the full axiom system, so you can try to puzzle this out yourself. --Allan McInnes 22:55, 11 January 2006 (UTC)

Thanks, I see what is going on now. It's subtle but it revolves around the nature of $\delta$ which doesn't act as a true zero for the (would be) semi-ring - we don't, in fact, have a semi-ring after all. That is, $\delta$ doesn't commute so while $\delta \cdot x=\delta$ we lack a property that $x\cdot \delta =\delta$. This lack of symmetry propogates through the system resulting in a lack of symmetry in distributive laws, and in the properties of $\tau$ (or, I guess, you can see the fact that $\delta$ doesn't commute, as you normally expect of a zero, as a result of the lack of a left distributive law). The consequences are intriguing - we don't have a structure that is "nice" as far as mathematicians are concerned. In general it seems far easier to understand than what I've seen of CSP and CCS though - very naturally lends itself to term rewriting and algebraic analysis (at least from the universal algebra view - that lack of "niceness" means it falls outside of what standard abstract algebra provides for so we don't get many of the really powerful results from there). -- Leland McInnes 23:53, 10 January 2006 (UTC)

Hardly surprising that you'd find ACP easier to digest: it was explicitly inspired by abstract algebra, and thus would tend to be more comprehensible to mathematicians. You might also be interested in μCRL, which combines ACP with a language for algebraic datatype specification. As far as the "niceness" goes: yes, you do tend to lose some symmetries you might otherwise have when you are modelling things that are dynamic. It adds some challenges. But, on the other hand, it opens up new vistas for research, since you need to find techniques other than the existing ones. --Allan McInnes 23:02, 11 January 2006 (UTC)

Is there a typo in the axioms?

After 5 years I suppose that both Allan and Leeland McInnes know more about this subject. In the comment there is a confusion in the operator. It is not true that $a\cdot x\vert \vert y=a\cdot (x\vert \vert y)$ it should say $a\cdot x\vert \vert y=a\cdot (x\vert \lfloor y)$ the difference between $\vert \vert$ and $\vert \lfloor$ is the commitment to start with the left side. I am new on ACP, but as far as I have understood, the $\vert \vert$ operator is not just parallel composition, but parallel interaction or parallel interleaving.

Based on the article linked above I will fix this typo in the axioms:

${\begin{matrix}x\vert \vert y&=&x\vert \lfloor y+y\vert \lfloor x+x\vert y&\qquad to\ this:\qquad &x\vert \vert y&=&x\vert \lfloor y+y\vert \lfloor x\\\end{matrix}}$

This part seems wrong

Communication — interaction (or communication) between processes is represented using the binary communications operator, $\vert$. For example, the actions $r(d)$ and $w(d)$ might be interpreted as the reading and writing of a data item $d\in D=\{1,2,3,\ldots \}$, respectively. Then the process

$(\sum _{d\in D}r(d)\cdot y)\vert (w(1)\cdot z)$

The $(r(1)+r(2)+\ldots )\cdot y\vert (w(1)\cdot z)$ seems to be wrong, unless it means some kind of typing. I think this is the correct one:

$(r(d)\cdot y)\vert (w(1)\cdot z)$

if the meaning of the $\sum _{d\in D}$ is a kind of type declaration, it would be more clear if written as:

$(r(d:D)\cdot y)\vert (w(1)\cdot z)$

Any Idea?