283
edits
Pipe-calculus: Difference between revisions
→Equational theory
KalmanKeri (talk | contribs) (→Syntax) |
KalmanKeri (talk | contribs) |
||
| Line 150: | Line 150: | ||
<math> | <math> | ||
\def\show{\mathsf{show}~} | |||
\def\match{\mathsf{match}~} | |||
\def\seq{\mathrel{;}} | \def\seq{\mathrel{;}} | ||
\def\succeed{\textbf{0}} | |||
\def\alt{\mid} | |||
\def\fail{\textbf{fail}} | |||
\def\pipe{\rhd} | \def\pipe{\rhd} | ||
\def\pass{\textbf{pass}} | \def\pass{\textbf{pass}} | ||
\def\pto{\mathrel{\to\mkern-18mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern11mu}}} | \def\pto{\mathrel{\to\mkern-18mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern11mu}}} | ||
\def\nto{\to} | \def\nto{\to} | ||
\def\eq{ = ~} | |||
\def\rule{ ::= ~} | |||
</math> | </math> | ||
Sequential composition is associative. <math>\ | Sequential composition is associative. <math>\succeed</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 \ | s \seq \succeed = & ~\succeed \seq s = ~s \\ | ||
\end{align} | \end{align} | ||
</math> | </math> | ||
| Line 172: | Line 176: | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
s \ | s \alt t = & ~t \alt s \\ | ||
s \ | s \alt (t \alt u) = & ~(s \alt t) \alt u \\ | ||
s \ | s \alt s = & ~s \\ | ||
s \ | s \alt \fail = & ~s \\ | ||
\end{align} | \end{align} | ||
</math> | </math> | ||
| Line 183: | Line 187: | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
(s \ | (s \alt t) \seq u = & ~s \seq u \alt t \seq u | ||
\end{align} | \end{align} | ||
</math> | </math> | ||