283
edits
Pipe-calculus: Difference between revisions
→Equational theory
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 150: | Line 150: | ||
\def\rule{ ::= ~} | \def\rule{ ::= ~} | ||
</math> | </math> | ||
Sequential composition is associative | Sequential composition is associative with left neutral element <math>\succeed</math> and left absorbing element <math>\fail</math>. | ||
<math> | <math> | ||
| Line 156: | Line 156: | ||
(s \seq t) \seq u \eq & s \seq (t \seq u) \\ | (s \seq t) \seq u \eq & s \seq (t \seq u) \\ | ||
\succeed \seq s \eq & s \\ | \succeed \seq s \eq & s \\ | ||
\fail \seq s \eq & \fail \\ | |||
\end{align} | \end{align} | ||
</math> | </math> | ||
Alternative composition is commutative | Alternative composition is associative, commutative and idempotent with neutral element <math>\fail</math> and absorbing element <math>\succeed</math>. | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
(s \alt t) \alt u \eq & s \alt (t \alt u) \\ | |||
s \alt t \eq & t \alt s \\ | s \alt t \eq & t \alt s \\ | ||
s \alt s \eq & s \\ | s \alt s \eq & s \\ | ||
\succeed \alt s \eq & \succeed \\ | |||
\fail \alt s \eq & s \\ | |||
\end{align} | \end{align} | ||
</math> | </math> | ||
Sequential composition is right distributive over alternative composition. | |||
<math> | <math> | ||