283
edits
Pipe-calculus: Difference between revisions
→Syntax
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) (→Syntax) |
||
| Line 35: | Line 35: | ||
=== Syntax === | === Syntax === | ||
<math> \ | <math> | ||
\def\pto{\mathrel{\to\mkern-17mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern10mu}}} | |||
\def\nto{\to} | |||
</math> | |||
<math> \mbox{ | <math> | ||
\begin{alignat}{3} | |||
& \mbox{Atoms}~ & a, b & ::= \mathsf{Foo} \mid \mathsf{Bar} \mid ... \\ | |||
'''Atoms''' are unscoped symbols. We assume a finite set of atoms that is disjunct from the set of operators and | & \mbox{Literals}~ & l, m & ::= a \mid \neg a \\ | ||
& \mbox{Primary terms}~ & a, b & ::= \mbox{sync}~ l \\ | |||
& \mbox{Sequences}~ & s, t & ::= a;s \mid a \mid \textbf{0} \\ | |||
& \mbox{Choices}~ & c, d & ::= s \textbf{|} c \mid s \mid \textbf{fail} \\ | |||
& \mbox{Pipelines}~ & p, q & ::= c \rhd p \mid c \\ | |||
\end{alignat} | |||
</math> | |||
'''Atoms''' are unscoped symbols. We assume a finite set of atoms that is disjunct from the set of constants (operators and constant symbols). | |||
'''Literals''' are atoms with '''polarity'''. | '''Literals''' are atoms with '''polarity'''. | ||
We say that a literal of the form <math> | We say that a literal of the form <math>a</math> is ''positive'', while <math>\neg a</math> is ''negative''. | ||
<ref> | <ref>See [[wikipedia:Literal_(mathematical_logic)|Literal (mathematical_logic)]] on literals in general.</ref> | ||
See [[wikipedia:Literal_(mathematical_logic)|Literal (mathematical_logic)]] | |||
There is only one kind of '''primary term''', which is '''synchronization'''. | |||
<ref>Adding new primary terms and the respective rules is a typical way of extending pipe-calculus.</ref> | |||
'''Sequences''' are ordered lists of primary terms. The symbol <math>\textbf{0}</math> denotes an empty sequence. In certain contexts it can be interpreted as success. | |||
'''Nondeterministic choice''' is an enumeration of alternatives. <math>\textbf{fail}</math> denotes the lack of choices, or intuitively a failure to find any viable alternative. | |||
The '''pipe''' operator connects a number of choices into '''pipelines'''. | |||
'' | 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. | ||
{| class="wikitable" | |||
|+ Summary of operators | |||
|- | |||
! style="text-align:left;"| Symbol | |||
! style="text-align:left;"| Name | |||
! style="text-align:left;"| Associativity<ref> | |||
Notice that left or right associativity is a grammatical property of a binary operator, | |||
which differs from the mathematical ''associativity'' of the respective operation. | |||
Even associative operations may be represented by left or right associative operators. | |||
</ref> | |||
! style="text-align:left;"| Precedence | |||
|- | |||
| <math>;</math> || Sequence || right || highest | |||
|- | |||
| <math>\mid</math> || Nondeterministic choice || right || | |||
|- | |||
| <math>\rhd</math> || Pipe || right || lowest | |||
|} | |||
== Notes == | == Notes == | ||
<references /> | <references /> | ||