Pipe-calculus

2023-05-24T19:09:07Z

KalmanKeri: /* Pipeline */

'''Pipe-calculus''' is a universal model of computation closely related to [[Wikipedia:process_calculus|process calculus]], [[Wikipedia:lambda_calculus|lambda calculus]] and [[Wikipedia:Formal_grammar|formal grammars]].
One of its distinctive features is the inclusion of syntactic symbols, so it is possible to express program structure and complex data types using only the built-in constructs.

Pure pipe-calculus is untyped. Construction of a [[ideas_for_a_type_system|type system]] is in the exploration phase, placing the focus on well-typed communication of programs.

Although the core calculus is sufficiently expressive to be used as a programming language, with added [[Syntax_sugar_(Pipe-calculus)|syntax sugar]] it can be the basis of various typed or untyped programming languages.
Its characteristic features like I/O and stream orientation make pipe-calculus a suitable choice even for scripting languages.

<div style="background-color: #f4f4f4; border: 1px solid #e8e8e8; padding: 0.3em 0.7em 0.3em 0.7em;">
'''Note:''' Pipe-calculus is a work in progress. This wiki page reflects the current status of the project and details may well change over time.</div>

== Introduction ==

=== Motivation ===

Development of pipe-calculus started with the idea that syntax should be a first class element of programming languages as well as formation rules are integral part of logical systems. A language like that is able to interpret complex input without using a parser library. Pipe-calculus is a minimal language with this capability.

On the practical side pipe-calculus is inspired by shell programming, which is largely based on text streams and stream processing tools. Indeed the idea of the ''pipe'' combinator comes from shell scripting.

=== An example ===

To get a taste of pipe-calculus, consider a program that adds two natural numbers encoded in [[wikipedia:Unary_numeral_system|unary numeral system]]. Suppose that we send both numbers over a stream as a series of <code>1</code>s terminated by an <code>end</code> symbol. Our example language consists of the following expressions.

* <code>match s</code> expects that the next symbol of the input stream is <code>s</code>. On failure the current fork of the program is aborted.
* <code>write s</code> appends the symbol <code>s</code> to the output stream.
* <code>run x</code> runs a program given its name.
* <code>p ; q</code> runs <code>p</code> then runs <code>q</code> unless <code>p</code> fails.
* <code>p | q</code> forks the execution of the program so that one fork runs <code>p</code>, another fork runs <code>q</code>, sharing the same input and output stream.

Start by writing a routine that copies a natural number from the input to the output.

passNat = match 1; write 1; run passNat | match end; write end

Now we can write the program that writes the sum of two numbers to the output.

addNat = match 1; write 1; run addNat | match end; run passNat

The program terminates after matching and writing out the second <code>end</code> symbol. It skips the first <code>end</code> that terminates the first number and copies everything else.
Effectively it concatenates two sequences of <code>1</code>s. If any other symbol occurs in the input stream, the program fails.

This language is obviously too weak. We can write simple filters, but we can't even check the equality of two numbers. In order to do it, we need a method that allows the first number to be accumulated and read back symbol by symbol as we read the second number.
Pipe-calculus can be seen as a framework to study the required extensions that turn this tiny language into a practical programming language.

=== Connection with other fields ===

Pipe-calculus is presented as a process calculus. Although it significantly differs from typical process calculi, it still lends itself to this style of presentation.
Its development is also inspired by
[[Wikipedia:Higher-order_logic_programming|higher-order logic programming]],
[[Wikipedia:Automata_theory|automata theory]],
[[Wikipedia:Type_theory|type theory]] (up to the [[Wikipedia:Lambda_cube|lambda-cube]]) and
[[Wikipedia:Effect_system|algebraic effects]]
<ref>
Matija Pretnar: [https://www.eff-lang.org/handlers-tutorial.pdf An Introduction to Algebraic Effects and Handlers]
</ref>.

In certain cases the connection can be made more precise.

* Programs written in pipe-calculus can recognize and generate words of formal languages encoded as terms.
* Untyped lambda calculus can be translated to a subset of higher-order pipe-calculus (to be specified later).

=== Variants and computational power ===

The most basic variant of the calculus that lacks any scoped constructs is called '''zeroth-order''' as a reference to [[Wikipedia:Zeroth-order_logic|zeroth-order logic]].
Somewhat surprisingly, even the zeroth-order calculus has a limited computational power.
In the '''higher-order''' calculus there are lexically scoped variables that can bind arbitrary terms. Intermediate variants can be constructed by extending the basic calculus with new constructs. Determining the computational power of specific variants of the calculus is of interest.

It is an observation and also a driving force of development that specific variants of the calculus can recognize specific classes of formal languages in the [[Wikipedia:Chomsky_hierarchy|Chomsky hierarchy]]. For example it is assumed that the zeroth-order calculus with top level recursion can encode [[Wikipedia:Finite-state_machine|finite-state machines]] and as a consequence it can recognize regular languages.

== Informal description ==

=== Terms ===

<math>
\def\dot{.}
\def\seq{\mathrel{;}}
\def\alt{\mid}
\def\pipe{\rhd}
\def\pass{\textbf{pass}}
\def\eq{ = ~}
</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.
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 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 <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>.
* ''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.
* ''choice'' <math>s \alt t</math> is a forking process where one fork executes <math>s</math> while the other fork executes <math>t</math>. Execution of the forks overlap in time. If one of the forks fails, the composite process is replaced by the other fork.
* ''pipeline'' <math>s \pipe t</math> is a composite process that enforces unidirectional, left to right data flow between its components.
* ''top'' <math>\top</math> is a process that successfully terminated.
* ''bottom'' <math>\bot</math> is also a terminated process. In certain contexts it denotes failure.

=== Prefixes ===

''Prefixes'' are basic units of behavior (called ''actions'' in process algebra). In pipe-calculus they can only occur together with a continuation.

=== Sequence ===

Sequences bring the concept of temporal order to pipe-calculus. In <math>s \mathrel{;} t</math>, <math>s</math> is executed before <math>t</math> (more precisely, the behavior of <math>s</math> is observed before the behavior of <math>t</math>).
If <math>s</math> fails (it reduces to <math>\bot</math>), <math>t</math> is not executed at all and the sequence fails.

<math>\bot \mathrel{;} t = \bot</math>

If the left operand succeeds, the right operand follows.

<math>\top \mathrel{;} t = t</math>

In <math>s ; s</math>, <math>s</math> is executed twice. In other words, sequence is not idempotent.
Logically <math>;</math> has common properties with non-commutative (shortcut) conjunction.

Prefixed forms also obey this temporal ordering: the behavior of the prefix is observed before the behavior of the continuation<ref>Wikipedia implies that prefixed forms are specialized forms of sequential composition: "In process calculi, the sequentialisation operator is usually integrated with input or output, or both." ([[Wikipedia:Process_calculus#Sequential_composition|Process calculus]] on Wikipedia)
</ref>.

=== Choice ===

* fork - join
* failure is local to forks
* forks may overlap
* but identical forks cannot be distinguished
* choice and mathematical case analisys

==== Exclusive choice ====

One can make choices mutually exclusive by limiting themeselves to trees of choices where each leaf of the tree is one of the forms <math>a^+ . s</math> and <math>a^- . s</math> [and all atoms are different]. This is an example of guarded choice[]. It allows for the encoding of sum types and the corresponding <math>case</math> expressions in strongly typed functional languages.

=== Pipeline ===

After discussing sequence and choice, the pipe combinator is the first where interaction occurs between processes.
<math>s \rhd t</math> is a composite process that enforces unidirectional data flow between its components. Input of the composite process is forwarded to the input of <math>s</math>, output of <math>s</math> is connected to the input of <math>t</math> and output of <math>t</math> is forwarded to the output of the composite process, according to the following diagram.

<math>\underset{s \rhd t}{\boxed{\to \boxed{s} \to \boxed{t} \to}}</math>

Compared to the parallel composition <math>\mid</math> in [[Wikipedia:π-calculus|π-calculus]], <math>\rhd</math> can be classified as unidirectional parallel composition.

==== Rules ====

If the operands are prefixed with matching literals, synchronisation occurs and both sides make progress.

<math>a^+ . s \rhd a^- . t = s \rhd t</math>

If the left operand is an output prefix and the right operand is an input prefix, communication occurs and both sides make progress. The term sent by the left side is available on the right side.

<math>!s . t \rhd ?n . u = t \rhd u[s/n]</math>

Arguably these are the key rules of pipe-calculus<ref>Compare with the relevant section on [[Wikipedia:Process_calculus#Reduction_semantics|Wikipedia]].</ref>.
Any other combination of prefixes leads to failure of the current fork.
The following example fails because synchronisation cannot occur between different atoms.

<math>a^+ . s \rhd b^- . t = \bot</math>

If any of the arguments is a choice, each fork of the left side is paired with each fork of the right side.

<math>r \mid s \rhd t \mid u = (r \rhd t) \mid (r \rhd u) \mid (s \rhd t) \mid (s \rhd u)</math>

==== Pipe and Unix pipelines ====

A [[Wikipedia:Pipeline_(Unix)|pipeline]] in Unix shell programming is a good analogy for the pipe combinator. Piped programs execute concurrently. In <math>P1 | P2</math> it cannot occur that the output of <math>P1</math> directly reaches the output of the pipeline.
Unix processes can handle more than one input and output streams, but only the standard input and output streams are passed on through the pipe.

==== Recognition and interpretation ====

One can also think of <math>s \rhd t</math> in a syntactic setting. In this case <math>s</math> represents ''input'' or ''source'', while <math>t</math> plays the role of a ''recognizer'', ''parser'' or ''interpreter''.

== Formal Definition ==

=== Syntax ===
<math>
\def\pos{\mathsf{pos}~}
\def\neg{\mathsf{neg}~}
\def\seq{\mathrel{;}}
\def\alt{\mid}
\def\pipe{\rhd}
\def\eq{ = ~}
\def\rule{ ::= ~}

\begin{alignat}{3}
& \mbox{Atoms}~ & a, b \rule & \mathsf{A} \mid \mathsf{B} \mid \mathsf{'foo} \mid \mathsf{'bar} \mid \mathsf{'+} \mid \mathsf{'*} \mid ... \\

& \mbox{Variables}~ & x, y \rule & \mathsf{a} \mid \mathsf{b} \mid ... \\

& \mbox{Prefixes}~ & p, q \rule
& ~ a^+ & & \text{Positive literal (signal)} \\
& & \mid & ~ a^- & & \text{Negative literal (match)} \\
& & \mid & ~ ?x & & \text{Abstraction (input)} \\
& & \mid & ~ !s & & \text{Argument (output)} \\

& \mbox{Terms}~ & s, t \rule
& ~ p . s & & \text{Prefix operator} \\
& & \mid & ~ s \seq t & & \text{Sequential composition} \\
& & \mid & ~ s \mathsf{|} t & & \text{Choice} \\
& & \mid & ~ s \pipe t & & \text{Pipe (interpretation)} \\
& & \mid & ~ \top & & \text{Termination, also success} \\
& & \mid & ~ \bot & & \text{Termination, also failure} \\
& & \mid & ~ x & & \text{Variable} \\
& & \mid & ~ (s) & & \text{Grouping} \\
\end{alignat}
</math>

{| class="wikitable"
|+ Operator summary
|-
! style="text-align:left;"| Symbol
! 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.
See [[Wikipedia:Operator_associativity|Operator associativity]].
</ref>
! style="text-align:left;"| Precedence
|-
| <math>\seq</math> || right || highest
|-
| <math>\mid</math> || right ||
|-
| <math>\rhd</math> || right || lowest
|}

=== Equational theory ===

Pipe-calculus can be described as a process algebra
<ref name="Baeten">
J.C.M. Baeten: [https://pure.tue.nl/ws/files/2154050/200402.pdf A brief history of process algebra.], Theoretical Computer Science 335 (2005) 131 – 146
</ref>
<ref name="Fokkink">
Wan Fokkink: [https://www.cs.vu.nl/~wanf/BOOKS/procalg.pdf Introduction to Process Algebra], Springer-Verlag
</ref>
.
The following identities are satisfied by all <math>s, t, u</math> pipe-calculus terms.

<math>
\def\seq{\mathrel{;}}
\def\alt{\mid}
\def\pipe{\rhd}
\def\eq{ = ~}
</math>Sequential composition is associative with left neutral element <math>\top</math> and left absorbing element <math>\bot</math>.

<math>
\begin{align}
(s \seq t) \seq u \eq & s \seq (t \seq u) \\
\top \seq t \eq & t \\
\bot \seq t \eq & \bot \\
\end{align}
</math>

Choice is associative, commutative and idempotent with neutral element <math>\bot</math> and absorbing element <math>\top</math>.

<math>
\begin{align}
(s \alt t) \alt u \eq & s \alt (t \alt u) \\
s \alt t \eq & t \alt s \\
s \alt s \eq & s \\
\top \alt t \eq & \top \\
\bot \alt t \eq & t \\
\end{align}
</math>

Sequential composition is right distributive over choice.

<math>
\begin{align}
(s \alt t) \seq u \eq & s \seq u \alt t \seq u
\end{align}
</math>

Pipe has left neutral element <math>\bot</math> and right absorbing element <math>\top</math>.

<math>
\begin{align}
\bot \pipe t \eq & t \\
s \pipe \top \eq & \top \\
\end{align}
</math>

Todo: pipe is also associative for ''well behaving'' operands. A process whose forks are all of the same prefixed form are certainly well behaving.

=== Normal forms ===

Normal form of pipe-calculus terms is defined by a term rewriting system<ref name="Fokkink"/>. A term is in normal form if no rewrite rule applies to it.

<math>
\def\seq{\mathrel{;}}
\def\alt{\mid}
\def\pipe{\rhd}
\def\in{\,?}
\def\out{!}
\def\rew{\mathrel{\Rightarrow}\,}
</math>
<math>
\begin{alignat}{1}
(s \seq t) \seq u \rew & s \seq (t \seq u) \\
(s \alt t) \seq u \rew & s \seq u \alt t \seq u \\
\top \seq s \rew & s \\
\bot \seq s \rew & \bot \\
\\
(s \alt t) \alt u \rew & s \alt (t \alt u) \\
a^+ . s \alt a^+ \seq t \rew & a^+ . (s \alt t) \\
a^- . s \alt a^- \seq t \rew & a^- . (s \alt t) \\
\bot \alt s \rew & s \\
s \alt \bot \rew & s \\
\top \alt s \rew & \top \\
s \alt \top \rew & \top \\
\end{alignat}
</math>

While all other rules are syntax directed, rules for <math>\pipe</math> have to be attempted in the listed order for the following reasons.

# The processes <math>a^- . s \pipe a^+ . t</math> and <math>\in x . s \pipe \out t . u</math> behave differently depending on the order of rule application, even if their normal forms are identical.
# The process <math>r \alt s \pipe t \alt u</math> produces subresults in different order depending of the order of rule application. Explicit application order avoids nondeterminism in both cases.
# We need a default rule that fails in order to ensure that <math>\pipe</math> never occurs in normal forms<ref>The default case allows for embedding synchronisation failure in the object language, so it can be captured by <math>\mid</math>.</ref>.

<math>
\begin{alignat}{2}
a^+ . s \pipe a^- . t \rew & s \pipe t \\
\out s . t \pipe \in x . u \rew & t \pipe u[s/x] \\
r \alt s \pipe t \alt u \rew & (r \pipe t \alt u) \alt (s \pipe t \alt u) \\
s \alt t \pipe u \rew & (s \pipe u) \alt (t \pipe u) \\
s \pipe t \alt u \rew & (s \pipe t) \alt (s \pipe u) \\
\bot \pipe t \rew & t \\
s \pipe \top \rew & \top \\
s \pipe t \rew & \bot & \\
\end{alignat}
</math>

Notice that finding a matching rewriting rule does not require checking the equality of terms, only of atoms.

== Extensions ==

* Recursion (μ-recursion, top level recursion, regular grammars)
* Stack (context-free grammars)
* Guarded choice
* Ordered choice (PEG, backtracking, local context)
* Intersection

== Connection with process calculus ==

'''[[wikipedia:process_calculus | Process calculi]]''' (or '''process algebras''') is an approach for formally modeling concurrent systems. ''Process'' refers to the behavior of a system. The word ''algebra'' denotes an algebraic approach in talking about behavior, while the word ''calculus'' emphasizes the computational aspect of processes.
<ref name="Baeten">
J.C.M. Baeten: [https://pure.tue.nl/ws/files/2154050/200402.pdf A brief history of process algebra.], Theoretical Computer Science 335 (2005) 131 – 146
</ref>
There are lots of implementations of this approach and none of them can be pointed to as the primary one.

A process calculus can be characterized by the atomic units of behavior (actions, events) and formers of compound processes (operators, combinators).
Implementations may include several of both categories and they are often open for extensions.

It is a recurrent pattern in the literature that processes can be viewed in two ways: one can combine component processes and examine the evolution of the resulting process. In this setting component processes may communicate with each other and the compound process may come to a rest without displaying external behavior. A single process can also be examined by placing it into a (not strictly specified) environment which is able to interact with the process.

Pipe-calculus fits into this framework if we make the following observations.

* Prefixes are atomic units of behavior (actions).
* Prefixes with sequential composition and choice form basic process algebra (BPA). <ref name="Fokkink">
Wan Fokkink: [https://www.cs.vu.nl/~wanf/BOOKS/procalg.pdf Introduction to Process Algebra], Springer-Verlag
</ref>
* The pipe operation can be seen as a restricted, unidirectional parallel composition.

There are also notable differences.

* The most outstanding difference is the lack of channels. Pipe-calculus processes only have a conceptual input and output, however one can simulate channels with synchronisation where atoms stand for channel names.
* Communication primitives in mainstream process calculi often inseparably unite two conceptual steps: the selection of a communication channel and the act of message sending. For example [[wikipedia:pi-calculus|Π-calculus]] <ref> Joachim Parrow: [https://courses.cs.vt.edu/~cs5204/fall05-kafura/Papers/PICalculus/parrow~2.pdf An Introduction to the π-Calculus], chapter to appear in Handbook of Process Algebra, ed. Bergstra, Ponse and Smolka,
Elsevier</ref> defines ''input prefixing'' <math>c\left(x\right).P</math> and ''output prefixing'' <math>\overline{c} \langle y \rangle.P</math> to denote receiving a name via channel <math>c</math> and sending a name via channel <math>c</math> respectively, before proceeding as <math>P</math>. Although one can introduce as convention ''synchronization'' where the communicated message is ignored, and ''broadcast'' where a group of processes are receiving messages on the same channel. In pipe-calculus these steps are separated by design.
* In pipe-calculus there is no counterpart of ''name hiding'' that prevents interference between two groups of processes using the same channel name for communication. Since there is no general, bidirectional parallel composition, we don't need a hiding primitive. The pipe operation naturally restricts communication to a pipeline.
* In pipe-calculus, if a process fails to synchronize, it is aborted. This is different from the usual implementation where a process that fails to synchronize does not evolve, it "keeps waiting" for a message, opening up the possibility for asynchronous communication.

== Notes ==

<references />