283
edits
Pipe-calculus: Difference between revisions
→Normal forms
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 249: | Line 249: | ||
\def\fail{\textbf{fail}} | \def\fail{\textbf{fail}} | ||
\def\pipe{\rhd} | \def\pipe{\rhd} | ||
\def\in{\,?} | \def\in{\,?} | ||
\def\out{!} | \def\out{!} | ||
| Line 271: | Line 270: | ||
</math> | </math> | ||
Unlike other combinators, rules for <math>\pipe</math> | Unlike other combinators, rules for <math>\pipe</math> have to be attempted in the listed order. There are multiple reasons to this. | ||
# The processes <math>a^- . s \pipe a^+ . t</math> and <math>\in x . s \pipe \out t . u</math> behave differently depending on the order of rule application, even if their normal forms are identical. | |||
# The process <math>r \alt s \pipe t \alt u</math> produces subresults in different order depending of the order of rule application. Explicit application order avoids nondeterminism in both cases. | |||
# We need a default rule that fails in order to ensure that <math>\pipe</math> never occurs in normal forms<ref>The default case allows for embedding synchronisation failure in the object language, so it can be captured by <math>\mid</math>.</ref>. | |||
<math> | <math> | ||
\begin{alignat}{ | \begin{alignat}{2} | ||
a^+ . s \pipe a^- . t \rew & s \pipe t \\ | a^+ . s \pipe a^- . t \rew & s \pipe t \\ | ||
\out s . t \pipe \in x . u \rew & t \pipe u[s/x] \\ | \out s . t \pipe \in x . u \rew & t \pipe u[s/x] \\ | ||
r \alt s \pipe t \alt u \rew & (r \pipe t \alt u) \alt (s \pipe t \alt u) \\ | |||
s \alt t \pipe u \rew & (s \pipe u) \alt (t \pipe u) \\ | 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 \alt u \rew & (s \pipe t) \alt (s \pipe u) \\ | ||
\fail \pipe t \rew & t \\ | \fail \pipe t \rew & t \\ | ||
s \pipe t \rew & \fail \\ | s \pipe \succeed \rew & \succeed \\ | ||
s \pipe t \rew & \fail & \\ | |||
\end{alignat} | \end{alignat} | ||
</math> | </math> | ||