283
edits
Pipe-calculus: Difference between revisions
→Normal forms
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 233: | Line 233: | ||
\def\pipe{\rhd} | \def\pipe{\rhd} | ||
\def\pass{\textbf{pass}} | \def\pass{\textbf{pass}} | ||
\def\rew{\Rightarrow | \def\in{\,?} | ||
\def\out{!} | |||
\def\rew{\mathrel{\Rightarrow}\,} | |||
</math> | </math> | ||
<math> | <math> | ||
\begin{alignat}{1} | \begin{alignat}{1} | ||
(s \seq t) \seq u \rew & s \seq t \seq u \\ | (s \seq t) \seq u \rew & s \seq (t \seq u) \\ | ||
(s \alt t) \seq u \rew & s \seq u \alt t \seq u \\ | (s \alt t) \seq u \rew & s \seq u \alt t \seq u \\ | ||
\succeed \seq s \rew & s \\ | \succeed \seq s \rew & s \\ | ||
\fail \seq s \rew & \fail \\ | \fail \seq s \rew & \fail \\ | ||
\\ | \\ | ||
(s \alt t) \alt u \rew & s \alt t \alt u \\ | (s \alt t) \alt u \rew & s \alt (t \alt u) \\ | ||
a^+ . s \alt a^+ \seq t \rew & a^+ . (s \alt t) \\ | |||
a^- . s \alt a^- \seq t \rew & a^- . (s \alt t) \\ | |||
\fail \alt s \rew & s \\ | \fail \alt s \rew & s \\ | ||
s \alt \fail \rew & s \\ | s \alt \fail \rew & s \\ | ||
| Line 252: | Line 254: | ||
</math> | </math> | ||
Unlike 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 fails in the default case, <math>\pipe</math> never occurs in normal forms. | As it fails in the default case, <math>\pipe</math> never occurs in normal forms. | ||
<math> | <math> | ||
\begin{alignat}{1} | \begin{alignat}{1} | ||
\ | a^+ . s \pipe a^- . t \rew & s \pipe t \\ | ||
\out s . t \pipe \in x . u \rew & t \pipe u[s/x] \\ | |||
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) \\ | ||