Pipe-calculus: Difference between revisions

Line 66: Line 66:
=== Syntax ===
=== Syntax ===
<math>
<math>
\def\show{\mathsf{show}~}
\def\pos{\mathsf{pos}~}
\def\match{\mathsf{match}~}
\def\neg{\mathsf{neg}~}
\def\seq{\mathrel{;}}
\def\seq{\mathrel{;}}
\def\succeed{\textbf{0}}
\def\succeed{\textbf{succeed}}
\def\alt{\mid}
\def\alt{\mid}
\def\fail{\textbf{fail}}
\def\fail{\textbf{fail}}
Line 82: Line 82:
& \mbox{Atoms}~        & a, b \rule & \mathsf{A} \mid \mathsf{B} \mid \mathsf{'foo} \mid \mathsf{'bar} \mid ... \\
& \mbox{Atoms}~        & a, b \rule & \mathsf{A} \mid \mathsf{B} \mid \mathsf{'foo} \mid \mathsf{'bar} \mid ... \\


& \mbox{Variables}~    & v, w \rule & \mathsf{v} \mid \mathsf{w} \mid ... \\
& \mbox{Primary}~    & p, q \rule & \pos a \mid \neg a \\


& \mbox{Terms}~      & s, t \rule & ~
& \mbox{Terms}~      & s, t \rule & ~
\show a \seq s \mid \match a \seq s
p
\mid \mathsf{v}
\mid (s)
\mid s \seq t \mid \succeed  
\mid s \seq t \mid \succeed  
\mid s \mathsf{|} t \mid \fail
\mid s \mathsf{|} t \mid \fail
\mid s \pipe t \mid \pass \\
\mid s \pipe t \mid \pass
\mid (s)
\end{alignat}
\end{alignat}
</math>
</math>


'''Atoms''' are unscoped symbols. We assume a countably infinite set of atoms that is disjunct from the set of constants (operators, keywords and punctuation).
'''Atoms''' are unscoped symbols. We assume a countably infinite set of atoms that is disjunct from the set of constants (operators, keywords and punctuation).
 
There are two kinds of '''primary terms''', positive and negative literals.
There are two '''synchronization''' prefixes, <math>\show a \seq s</math> and <math>\match a \seq s</math>.
'''Sequential composition''' <math>\seq</math> constructs ordered pairs. The symbol <math>\succeed</math> denotes an empty sequence which can be interpreted as successful termination.  
 
'''Alternative composition''' <math>\alt</math> connects a pair of alternatives. <math>\fail</math> denotes an empty set of alternatives, or intuitively failure to find any viable alternative.
'''Sequences''' are temporally ordered actions. The symbol <math>\succeed</math> denotes an empty sequence which can be interpreted as successful termination.
The <math>\pipe</math> '''pipe''' operator constructs '''pipelines'''. Intuitively a pipeline is a transformer with unidirectional data flow.
Prefixes can be treated as specialized indivisible sequences.
 
'''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 choices into '''pipelines'''.
<math>\pass</math> denotes a passive pipeline that transfers its input unchanged to the output.  
<math>\pass</math> denotes a passive pipeline that transfers its input unchanged to the output.  


Line 112: Line 106:
<math>
<math>
\begin{alignat}{1}
\begin{alignat}{1}
~~~~ & a \pto s & = & ~\show a \seq s \\
~~~~ & a \pto s & = & ~\pos a \seq s \\
~~~~ & a \nto s & = & ~\match a \seq s \\
~~~~ & a \nto s & = & ~\neg a \seq s \\
\end{alignat}
\end{alignat}
</math>
</math>
283

edits