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. <math>\succeed</math> is its neutral element. | Sequential composition is associative. <math>\succeed</math> is its left neutral element. | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
s \seq | (s \seq t) \seq u \eq & s \seq (t \seq u) \\ | ||
\succeed \seq s \eq & s \\ | \succeed \seq s \eq & s \\ | ||
\end{align} | \end{align} | ||
| Line 163: | Line 163: | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
s \alt t | s \alt t \eq & t \alt s \\ | ||
s \alt | (s \alt t) \alt u \eq & s \alt (t \alt u) \\ | ||
s \alt s | s \alt s \eq & s \\ | ||
s \alt \fail | s \alt \fail \eq & s \\ | ||
s \alt \succeed | s \alt \succeed \eq & \succeed \\ | ||
\end{align} | \end{align} | ||
</math> | </math> | ||
| Line 175: | Line 175: | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
(s \alt t) \seq u | (s \alt t) \seq u \eq & s \seq u \alt t \seq u | ||
\end{align} | \end{align} | ||
</math> | </math> | ||
Pipe is associative with neutral element <math>\pass</math>. | Pipe is associative with right neutral element <math>\pass</math>. | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
s \pipe | (s \pipe t) \pipe u \eq & s \pipe (t \pipe u) \\ | ||
s \pipe \pass \eq & s \\ | s \pipe \pass \eq & s \\ | ||
\end{align} | \end{align} | ||