283
edits
Pipe-calculus: Difference between revisions
→Zero-order calculus
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 63: | Line 63: | ||
== Zero-order calculus == | == Zero-order calculus == | ||
<math> | |||
\def\dot{\mathrel{.}} | |||
\def\seq{\mathrel{;}} | |||
\def\succeed{\textbf{succeed}} | |||
\def\alt{\mid} | |||
\def\fail{\textbf{fail}} | |||
\def\pipe{\rhd} | |||
\def\pass{\textbf{pass}} | |||
\def\eq{ = ~} | |||
</math> | |||
''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 concurrent and communicating 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 include '''atoms''' which are unscoped and uninterpreted symbols. The following terms are available in zero-order pipe-calculus. | |||
* ''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 the process <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 the process <math>s</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. | |||
* ''alternatives'' <math>s \alt t</math> is a branching process where one branch executes <math>s</math> while the other branch concurrently executes <math>t</math>. If one of the branches fail, the composite process is replaced by the other branch. | |||
* ''pipeline'' <math>s \pipe t</math> is a composite process that enforces unidirectional data flow. Output of <math>s</math> is connected to the input of <math>t</math>. Input of the composite process is forwarded to the input of <math>s</math> and output of <math>t</math> is forwarded to the output of the composite process. | |||
* ''success'' <math>\mathsf{succeed}</math> is a process that successfully terminated. | |||
* ''failure'' <math>\mathsf{fail}</math> is a process that failed. | |||
* ''passive process'' <math>\mathsf{pass}</math> is a transparent process that unconditionally and endlessly forwards its input to its output. | |||
== Formal Definition == | == Formal Definition == | ||