Pipe-calculus: Difference between revisions

Line 66: Line 66:
=== Syntax ===
=== Syntax ===
<math>
<math>
\def\show{\mathsf{show}~}
\def\match{\mathsf{match}~}
\def\seq{\mathrel{;}}
\def\seq{\mathrel{;}}
\def\succeed{\textbf{0}}
\def\alt{\mid}
\def\fail{\textbf{fail}}
\def\pipe{\rhd}
\def\pipe{\rhd}
\def\sync{\mathsf{sync}~}
\def\null{\textbf{0}}
\def\fail{\textbf{fail}}
\def\pass{\textbf{pass}}
\def\pass{\textbf{pass}}
\def\pto{\mathrel{\to\mkern-18mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern11mu}}}
\def\pto{\mathrel{\to\mkern-18mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern11mu}}}
\def\nto{\to}
\def\nto{\to}
\def\eq{ = ~}
\def\rule{ ::= ~}
\def\rule{ ::= ~}


\begin{alignat}{2}
\begin{alignat}{2}
& \mbox{Atoms}~        & x, y \rule & \mathsf{A} \mid \mathsf{B} \mid ... \\
& \mbox{Atoms}~        & x, y \rule & \mathsf{A} \mid \mathsf{B} \mid \mathsf{'foo} \mid \mathsf{'bar} \mid ... \\
 
& \mbox{Literals}~      & l, m \rule & x \mid \neg x \\
 
& \mbox{Variables}~    & v, w \rule & \mathsf{a} \mid \mathsf{b} \mid ... \\


& \mbox{Actions}~       & a, b \rule & \sync l \\
& \mbox{Variables}~     & v, w \rule & \mathsf{v} \mid \mathsf{w} \mid ... \\


& \mbox{Terms}~      & s, t, u \rule & ~a \mid (s)
& \mbox{Terms}~      & s, t, u \rule & ~
\mid s \seq t \mid \null
\show x \mid \match x
\mid \mathsf{v}
\mid (s)
\\ & & &
\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 \\
Line 100: Line 103:
There is only one kind of '''action''', which is '''synchronization'''.
There is only one kind of '''action''', which is '''synchronization'''.


'''Sequences''' are ordered lists of actions. The symbol <math>\textbf{0}</math> denotes an empty sequence which can be interpreted as successful termination.
'''Sequences''' are ordered lists of actions. The symbol <math>\succeed</math> denotes an empty sequence which can be interpreted as successful termination.


'''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.
'''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.
283

edits