283
edits
Pipe-calculus: Difference between revisions
→Syntax
KalmanKeri (talk | contribs) (→Syntax) |
KalmanKeri (talk | contribs) (→Syntax) |
||
| Line 34: | Line 34: | ||
=== Syntax === | === Syntax === | ||
<math> | <math> | ||
\def\seq{\mathrel{;}} | |||
\def\sync{\mathsf{sync}~} | |||
\def\null{\textbf{0}} | |||
\def\fail{\textbf{fail}} | |||
\def\pto{\mathrel{\to\mkern-17mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern10mu}}} | \def\pto{\mathrel{\to\mkern-17mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern10mu}}} | ||
\def\nto{\to} | \def\nto{\to} | ||
\begin{alignat}{3} | \begin{alignat}{3} | ||
& \mbox{Atoms}~ & a, b & ::= \mathsf{Foo} \mid \mathsf{Bar} \mid ... \\ | & \mbox{Atoms}~ & a, b & ::= \mathsf{Foo} \mid \mathsf{Bar} \mid ... \\ | ||
| Line 46: | Line 47: | ||
& \mbox{Literals}~ & l, m & ::= a \mid \neg a \\ | & \mbox{Literals}~ & l, m & ::= a \mid \neg a \\ | ||
& \mbox{Primary terms}~ & a, b & ::= \ | & \mbox{Primary terms}~ & a, b & ::= \sync l \\ | ||
& \mbox{Sequences}~ & s, t & ::= a | & \mbox{Sequences}~ & s, t & ::= a \seq s \mid a \mid \null \\ | ||
& \mbox{Choices}~ & c, d & ::= s \ | & \mbox{Choices}~ & c, d & ::= s \mathsf{|} c \mid s \mid \fail \\ | ||
& \mbox{Pipelines}~ & p, q & ::= c \rhd p \mid c \\ | & \mbox{Pipelines}~ & p, q & ::= c \rhd p \mid c \\ | ||
| Line 70: | Line 71: | ||
The '''pipe''' operator connects a number of choices into '''pipelines'''. | The '''pipe''' operator connects a number of choices into '''pipelines'''. | ||
For better readability, let's define some syntax sugar that will be used throughout this article. | |||
<math>\mbox{Sequences}~ s, t ::= ... \mid a \pto s \mid a \nto s \mbox{, where}</math> | |||
<math> | |||
\begin{alignat}{4} | |||
~~~~ & a \pto s & = & ~\sync a & \seq s \\ | |||
~~~~ & a \nto s & = & ~\sync \neg a & \seq s | |||
\end{alignat} | |||
</math> | |||
We name the new operators '''positive arrow''' and '''negative arrow''' respectively. | |||
When it is clear from context, we can call a negative arrow simply an arrow. | |||
Note that the basic calculus ''does not allow'' the use of parentheses for grouping and disambiguation. The above syntax definition precisely defines the precedence of operators, which is summarized in the following table. | Note that the basic calculus ''does not allow'' the use of parentheses for grouping and disambiguation. The above syntax definition precisely defines the precedence of operators, which is summarized in the following table. | ||
| Line 79: | Line 94: | ||
! style="text-align:left;"| Name | ! style="text-align:left;"| Name | ||
! style="text-align:left;"| Associativity<ref> | ! style="text-align:left;"| Associativity<ref> | ||
Notice that left or right associativity is a grammatical property of a binary operator, | Notice that ''left or right associativity'' is a grammatical property of a binary operator, | ||
which differs from the mathematical ''associativity'' of the respective operation. | which differs from the mathematical ''associativity'' of the respective operation. | ||
Even associative operations may be represented by left or right associative operators. | Even associative operations may be represented by left or right associative operators. | ||
</ref> | </ref> | ||
! style="text-align:left;"| Precedence | ! style="text-align:left;"| Precedence | ||
|- | |- | ||
| <math> | | <math>\seq~\pto~\nto</math> || Sequence and arrows || right || highest | ||
|- | |- | ||
| <math>\mid</math> || Nondeterministic choice || right || | | <math>\mid</math> || Nondeterministic choice || right || | ||
|- | |- | ||
| <math>\rhd</math> || Pipe || right || lowest | | <math>\rhd</math> || Pipe || right || lowest | ||
|} | |} | ||