283
edits
Pipe-calculus: Difference between revisions
→Pipeline
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 138: | Line 138: | ||
<math>\rhd</math> does not occur in the normal form of closed terms. | <math>\rhd</math> does not occur in the normal form of closed terms. | ||
If the operands are matching synchronisation | If the operands are prefixed with matching literals, synchronisation occurs and both sides make progress. | ||
<math>a^+ . s \rhd a^- . t = s \rhd t</math> | <math>a^+ . s \rhd a^- . t = s \rhd t</math> | ||
| Line 146: | Line 146: | ||
<math>!s . t \rhd ?n . u = t \rhd u[s/n]</math> | <math>!s . t \rhd ?n . u = t \rhd u[s/n]</math> | ||
Any other combination of | Arguably these are the key rules of pipe-calculus<ref>Compare with the relevant section on [[Wikipedia:Process_calculus#Reduction_semantics|Wikipedia]].</ref>. | ||
Any other combination of prefixes leads to failure of the current fork. | |||
The following example fails because synchronisation cannot occur between different atoms. | The following example fails because synchronisation cannot occur between different atoms. | ||