283
edits
Pipe-calculus: Difference between revisions
→Equational theory
KalmanKeri (talk | contribs) (→Syntax) |
KalmanKeri (talk | contribs) |
||
| Line 212: | Line 212: | ||
<math> | <math> | ||
\def\seq{\mathrel{;}} | \def\seq{\mathrel{;}} | ||
\def\alt{\mid} | \def\alt{\mid} | ||
\def\pipe{\rhd} | \def\pipe{\rhd} | ||
\def\eq{ = ~} | \def\eq{ = ~} | ||
</math>Sequential composition is associative with left neutral element <math>\ | </math>Sequential composition is associative with left neutral element <math>\top</math> and left absorbing element <math>\bot</math>. | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
(s \seq t) \seq u \eq & s \seq (t \seq u) \\ | (s \seq t) \seq u \eq & s \seq (t \seq u) \\ | ||
\ | \top \seq t \eq & t \\ | ||
\ | \bot \seq t \eq & \bot \\ | ||
\end{align} | \end{align} | ||
</math> | </math> | ||
Choice is associative, commutative and idempotent with neutral element <math>\ | Choice is associative, commutative and idempotent with neutral element <math>\bot</math> and absorbing element <math>\top</math>. | ||
<math> | <math> | ||
| Line 234: | Line 232: | ||
s \alt t \eq & t \alt s \\ | s \alt t \eq & t \alt s \\ | ||
s \alt s \eq & s \\ | s \alt s \eq & s \\ | ||
\ | \top \alt t \eq & \top \\ | ||
\ | \bot \alt t \eq & t \\ | ||
\end{align} | \end{align} | ||
</math> | </math> | ||
| Line 247: | Line 245: | ||
</math> | </math> | ||
Pipe has left neutral element <math>\ | Pipe has left neutral element <math>\bot</math> and right absorbing element <math>\top</math>. | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
\ | \bot \pipe t \eq & t \\ | ||
s \pipe \ | s \pipe \top \eq & \top \\ | ||
\end{align} | \end{align} | ||
</math> | </math> | ||