283
edits
Pipe-calculus: Difference between revisions
→Equational theory
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 140: | Line 140: | ||
== Equational theory == | == Equational theory == | ||
Sequential composition is associative. <math>\null</math> is | Sequential composition is associative. <math>\null</math> is its neutral element. | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
s \seq (t \seq u) = & ~(s \seq t) \seq u \\ | s \seq (t \seq u) = & ~(s \seq t) \seq u \\ | ||
s \seq \null = & ~\null \seq s = ~s \\ | |||
\end{align} | \end{align} | ||
</math> | </math> | ||
| Line 153: | Line 153: | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
s \mid t = & ~t \mid s \\ | |||
s \mid (t \mid u) = & ~(s \mid t) \mid u \\ | s \mid (t \mid u) = & ~(s \mid t) \mid u \\ | ||
s \mid s = & ~s \\ | |||
s \mid \fail = & ~s \\ | |||
\end{align} | \end{align} | ||
</math> | </math> | ||
| Line 165: | Line 165: | ||
\begin{align} | \begin{align} | ||
(s \mid t) \seq u = & ~s \seq u \mid t \seq u | (s \mid t) \seq u = & ~s \seq u \mid t \seq u | ||
\end{align} | |||
</math> | |||
Pipe is associative and its neutral element is <math>\pass</math>. | |||
<math> | |||
\begin{align} | |||
s \pipe (t \pipe u) = & ~(s \pipe t) \pipe u \\ | |||
s \pipe \pass = & ~\pass \pipe s = ~s \\ | |||
\end{align} | \end{align} | ||
</math> | </math> | ||