283
edits
Pipe-calculus: Difference between revisions
→Normal forms
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 348: | Line 348: | ||
\\ | \\ | ||
(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^+ | a^+ . s \alt a^+ . t \rew & a^+ . (s \alt t) \\ | ||
a^- . s \alt a^- | a^- . s \alt a^- . t \rew & a^- . (s \alt t) \\ | ||
\bot \alt s \rew & s \\ | \bot \alt s \rew & s \\ | ||
s \alt \bot \rew & s \\ | s \alt \bot \rew & s \\ | ||
| Line 356: | Line 356: | ||
\end{alignat} | \end{alignat} | ||
</math> | </math> | ||
('''Todo''': these rules don't implement idempotence of <math>|</math> because commutativity is left out from the rules so equal terms don't always have a chance to "meet" on sides of <math>|</math>.) | |||
While all other rules are syntax directed, rules for <math>\pipe</math> have to be attempted in the listed order for the following reasons. | While all other rules are syntax directed, rules for <math>\pipe</math> have to be attempted in the listed order for the following reasons. | ||