283
edits
Pipe-calculus: Difference between revisions
→Normal form
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 191: | Line 191: | ||
Normal form of pipe-calculus terms is defined by a term rewriting system. A term is in normal form if no rewrite rule applies to it. | Normal form of pipe-calculus terms is defined by a term rewriting system. A term is in normal form if no rewrite rule applies to it. | ||
<math> | |||
\def\pos{\mathsf{pos}~} | |||
\def\neg{\mathsf{neg}~} | |||
\def\seq{\mathrel{;}} | |||
\def\succeed{\textbf{succeed}} | |||
\def\alt{\mid} | |||
\def\fail{\textbf{fail}} | |||
\def\pipe{\rhd} | |||
\def\pass{\textbf{pass}} | |||
\def\pto{\mathrel{\to\mkern-18mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern11mu}}} | |||
\def\nto{\to} | |||
\def\eq{ = ~} | |||
\def\rule{ ::= ~} | |||
</math> | |||
<math> | <math> | ||
\begin{alignat}{1} | \begin{alignat}{1} | ||
a \pto s \seq t \Rightarrow a \pto (s \seq t) \\ | |||
a \nto s \seq t \Rightarrow a \nto (s \seq t) \\ | |||
(s \seq t) \seq u \Rightarrow & s \seq (t \seq u) \\ | (s \seq t) \seq u \Rightarrow & s \seq (t \seq u) \\ | ||
(s \alt t) \seq u \Rightarrow & s seq u \alt t \seq u \\ | (s \alt t) \seq u \Rightarrow & s \seq u \alt t \seq u \\ | ||
\end{alignat} | \end{alignat} | ||
</math> | </math> | ||
== Connection with process calculus == | == Connection with process calculus == | ||