283
edits
Pipe-calculus: Difference between revisions
→Rules
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) (→Rules) |
||
| Line 160: | Line 160: | ||
<math>a^+ . s \rhd a^- . t = s \rhd t</math> | <math>a^+ . s \rhd a^- . t = s \rhd t</math> | ||
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 | 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 output by the left side is available in the continuation of the right side. | ||
<math>!s . t \rhd ?n . u = t \rhd u[s/n]</math> | <math>!s . t \rhd ?n . u = t \rhd u[s/n]</math> | ||
Arguably these are the key rules of pipe-calculus<ref>Compare with | Arguably these are the key rules of pipe-calculus<ref>Compare with [[Wikipedia:Process_calculus#Reduction_semantics|reduction semantics]] of process calculi on Wikipedia.</ref>. | ||
Any other combination of prefixes leads to failure | Any other combination of prefixes leads to failure. | ||
The following example fails because synchronisation cannot occur between different atoms. | The following example fails because synchronisation cannot occur between different atoms. | ||