Pipe-calculus: Difference between revisions

Line 67: Line 67:
== Informal description ==
== Informal description ==


=== Zero-order calculus ===
=== Terms ===


<math>
<math>
\def\dot{\mathrel{.}}
\def\dot{.}
\def\seq{\mathrel{;}}
\def\seq{\mathrel{;}}
\def\succeed{\textbf{succeed}}
\def\succeed{\textbf{succeed}}
Line 78: Line 78:
\def\pass{\textbf{pass}}
\def\pass{\textbf{pass}}
\def\eq{ = ~}
\def\eq{ = ~}
</math>
</math>Pipe-calculus terms are also called '''processes''' to emphasize their interactive, behavioral aspect. Each process has a conceptual '''input''' and '''output''' which are implicit in the rules. Output of one process can be connected to the input of another one.
''Zero-order'' pipe-calculus is a minimal variant of higher-order pipe-calculus which lacks any scoped constructs. Despite of this restriction it still have a limited computational power. Pipe-calculus terms are also called '''processes''' when their interactive, behavioral aspect is emphasized. Each process has a conceptual '''input''' and '''output''' which are implicit in the rules. Output of one process can be connected to the input of another one.
Some terms contain '''atoms''' which are unscoped and uninterpreted symbols. In grammatical context one can think of atoms as ''tokens''.


Some terms contain '''atoms''' which are unscoped and uninterpreted symbols. In grammatical context one can think of atoms as ''tokens''. The following terms are available in zero-order pipe-calculus.
The following terms are available in pipe-calculus.


* ''synchronisation'', where
* ''synchronisation'', where
** ''negative literal prefixing'' <math>a^- \dot s</math> is a process that expects an atom <math>a</math> to be signalled on its input. If the expectation is fulfilled, the process  proceeds as <math>s</math>, otherwise it fails.
** ''negative literal prefixing'' <math>a^- \dot s</math> is a process that expects an atom <math>a</math> to be signalled on its input. If the expectation is fulfilled, the process  proceeds as <math>s</math>, otherwise it fails.
** ''positive literal prefixing'' <math>a^+ \dot s</math> is a process that signals an atom <math>a</math> on its output before proceeding as <math>s</math>.
** ''positive literal prefixing'' <math>a^+ \dot s</math> is a process that signals an atom <math>a</math> on its output before proceeding as <math>s</math>.
* ''communication'', where
** ''input prefixing'' <math>?n \dot s</math> is a process that receives a term on its input. On success, it proceeds as <math>s</math> binding the name <math>n</math> to the received term.
** ''output prefixing'' <math>!s \dot t</math> is a process that sends a term <math>s</math> to its output before proceeding as <math>t</math>.
* ''sequence'' <math>s \seq t</math> is a composite process that executes <math>s</math> before proceeding as <math>t</math> unless <math>s</math> fails. In that case the composite process also fails.
* ''sequence'' <math>s \seq t</math> is a composite process that executes <math>s</math> before proceeding as <math>t</math> unless <math>s</math> fails. In that case the composite process also fails.
* ''choice'' <math>s \alt t</math> is a forking process where one fork executes <math>s</math> while the other fork concurrently executes <math>t</math>. If one of the forks fail, the composite process is replaced by the other fork.
* ''choice'' <math>s \alt t</math> is a forking process where one fork executes <math>s</math> while the other fork concurrently executes <math>t</math>. If one of the forks fail, the composite process is replaced by the other fork.
283

edits