283
edits
KalmanKeri (talk | contribs) (→Terms) |
KalmanKeri (talk | contribs) |
||
| Line 110: | Line 110: | ||
=== The pipe combinator === | === The pipe combinator === | ||
After discussing sequence and choice, the pipe combinator is the first where | After discussing sequence and choice, the pipe combinator is the first where interaction occurs between processes. | ||
<math>s \rhd t</math> is a composite process that enforces unidirectional data flow between its components according to the following diagram. | <math>s \rhd t</math> is a composite process that enforces unidirectional data flow between its components. Input of the composite process is forwarded to the input of <math>s</math>, output of <math>s</math> is connected to the input of <math>t</math> and output of <math>t</math> is forwarded to the output of the composite process, according to the following diagram. | ||
<math>\underset{s \rhd t}{\boxed{\to \boxed{s} \to \boxed{t} \to}}</math> | <math>\underset{s \rhd t}{\boxed{\to \boxed{s} \to \boxed{t} \to}}</math> | ||
| Line 122: | Line 122: | ||
<math>a^+ . s \rhd a^- . t = s \rhd t</math> | <math>a^+ . s \rhd a^- . t = s \rhd t</math> | ||
If any of the arguments is a choice, each | If the left operand is an output prefix and the right operand is an input prefix, communication occurs and both sides make progress. The term sent by the left side is available on the right side. | ||
<math>!s . t \rhd ?n . u = t \rhd u[s/n]</math> | |||
Any other combination of operands leads to failure of the current fork. | |||
<math>(a^+ . s \rhd b^- . t) = \mathsf{fail}</math> | |||
If any of the arguments is a choice, each fork of the left side is paired with each fork of the right side. | |||
<math>r \mid s \rhd t \mid u = (r \rhd t) \mid (r \rhd u) \mid (s \rhd t) \mid (s \rhd u)</math> | <math>r \mid s \rhd t \mid u = (r \rhd t) \mid (r \rhd u) \mid (s \rhd t) \mid (s \rhd u)</math> | ||
==== Pipe and Unix pipelines ==== | ==== Pipe and Unix pipelines ==== | ||
edits