283
edits
Pipe-calculus: Difference between revisions
→Normal form
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 190: | Line 190: | ||
=== Normal form === | === Normal form === | ||
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[procalg, multiple refs]. A term is in normal form if no rewrite rule applies to it. | ||
<math> | <math> | ||
| Line 215: | Line 215: | ||
\\ | \\ | ||
(s \alt t) \alt u \rew & s \alt t \alt u \\ | (s \alt t) \alt u \rew & s \alt t \alt u \\ | ||
\pos a \seq s \alt \pos a \seq t \rew & \pos a \seq (s \alt t) \\ | \pos a \seq s \alt \pos a \seq t \rew & \pos a \seq (s \alt t) \\ | ||
\neg a \seq s \alt \neg a \seq t \rew & \neg a \seq (s \alt t) \\ | \neg a \seq s \alt \neg a \seq t \rew & \neg a \seq (s \alt t) \\ | ||
| Line 223: | Line 221: | ||
\succeed \alt s \rew & \succeed \\ | \succeed \alt s \rew & \succeed \\ | ||
s \alt \succeed \rew & \succeed \\ | s \alt \succeed \rew & \succeed \\ | ||
\\ | \end{alignat} | ||
</math> | |||
Differently from other combinators, rules for <math>\pipe</math> has to be attempted in the listed order. <ref>This is only a technical detail. Rewrite rules can be defined without overlapping but it requires more cases.</ref> | |||
As it has a default rule, <math>\pipe</math> never occurs in normal forms. | |||
<math> | |||
\begin{alignat}{1} | |||
\pos a \seq s \pipe \neg a \seq t \rew & s \pipe t \\ | \pos a \seq s \pipe \neg a \seq t \rew & s \pipe t \\ | ||
s \pipe t \rew & \fail | s \alt t \pipe u \rew & (s \pipe u) \alt (t \pipe u) \\ | ||
s \pipe t \alt u \rew & (s \pipe t) \alt (s \pipe u) \\ | |||
s \pipe t \rew & \fail \\ | |||
\end{alignat} | \end{alignat} | ||
</math> | </math> | ||
== Connection with process calculus == | == Connection with process calculus == | ||