Pipe-calculus

Pipe-calculus is a model of computation that is closely related to process calculus, lambda calculus and formal language theory.

It is intended as a core language for (possibly typed) programming languages.

Note: Pipe-calculus is work in progress. This wiki page reflects my current understanding and details may very well change over time.

Overview

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. Shell programming is a proved and efficient way of problem solving, although it is not known about clarity and simplicity.

How would a small and well established stream processing language look like? To get a taste, consider a program that adds two natural numbers encoded in unary numeral system, a popular example in theoretical computer science. Suppose that we send both numbers over a stream as a series of S symbols terminated by a symbol Z. Our example language consists of the following expressions.

• match s checks if the next symbol of the input stream is s. On failure the current branch of the program is aborted.
• write s writes the symbol s to the output stream.
• run x runs a program given its name.
• p ; q runs p then runs q unless p fails.
• p | q forks the execution of the program so that one branch runs p, another branch runs q, sharing the same input and output stream.

First we write a routine that copies a natural number from the input to the output.

passNat = match S; write S; run passNat | match Z; write Z

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

addNat = match S; write S; run addNat | match Z; run passNat

The program terminates after matching and writing out the second symbol Z it encounters. It skips the first Z that terminates the first number and copies everything else. Effectively it concatenates two Z-terminated sequences of Ss. 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 natural 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 to other fields

Pipe-calculus is examined primarily as a process calculus. Although it significantly differs from typical process calculi, it lends itself to this style of presentation. Its development is also inspired by higher-order logic programming, formal grammars, automata theory, type theory (up to the lambda-cube) and algebraic effects .

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. I'm interested in finding correspondence between variants of pipe-calculus and classes of formal languages.
• Untyped lambda calculus can be translated to a subset of higher-order pipe-calculus (to be specified later).

Variants and computational power

Pipe-calculus is meant to be an extensible framework. An important extension is the inclusion of scoped variables.

The most simple variant of the calculus that is lacking any scoped constructs is called zero-order. Somewhat surprisingly, even the zero-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 recursion, among others. The computational power of specific variants of the calculus is also an interesting question.

Zero-order calculus

[math]\displaystyle{ \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]\displaystyle{ a^- \dot s }[/math] is a process that expects an atom [math]\displaystyle{ a }[/math] to be signalled on its input. If the expectation is fulfilled, the process proceeds as [math]\displaystyle{ s }[/math], otherwise it fails.
  • positive literal prefixing [math]\displaystyle{ a^+ \dot s }[/math] is a process that signals an atom [math]\displaystyle{ a }[/math] on its output before proceeding as [math]\displaystyle{ s }[/math].
• sequence [math]\displaystyle{ s \seq t }[/math] is a composite process that executes [math]\displaystyle{ s }[/math] before proceeding as [math]\displaystyle{ t }[/math] unless [math]\displaystyle{ s }[/math] fails. In that case the composite process also fails.
• alternatives [math]\displaystyle{ s \alt t }[/math] is a branching process where one branch executes [math]\displaystyle{ s }[/math] while the other branch concurrently executes [math]\displaystyle{ t }[/math]. If one of the branches fail, the composite process is replaced by the other branch.
• pipeline [math]\displaystyle{ s \pipe t }[/math] is a composite process that enforces unidirectional data flow. Output of [math]\displaystyle{ s }[/math] is connected to the input of [math]\displaystyle{ t }[/math]. Input of the composite process is forwarded to the input of [math]\displaystyle{ s }[/math] and output of [math]\displaystyle{ t }[/math] is forwarded to the output of the composite process.
• [math]\displaystyle{ \mathsf{succeed} }[/math] is a process that successfully terminated.
• [math]\displaystyle{ \mathsf{fail} }[/math] is a process that failed.
• [math]\displaystyle{ \mathsf{pass} }[/math] is a passive process that endlessly copies its input to its output.

Formal Definition

Syntax

[math]\displaystyle{ \def\pos{\mathsf{pos}~} \def\neg{\mathsf{neg}~} \def\seq{\mathrel{;}} \def\succeed{\textbf{succeed}} \def\alt{\mid} \def\fail{\textbf{fail}} \def\pipe{\rhd} \def\pass{\textbf{pass}} \def\pto{\mathrel{\to\mkern-18mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern11mu}}} \def\nto{\to} \def\eq{ = ~} \def\rule{ ::= ~} \begin{alignat}{2} & \mbox{Atoms}~ & a, b \rule & \mathsf{A} \mid \mathsf{B} \mid \mathsf{'foo} \mid \mathsf{'bar} \mid ... \\ & \mbox{Variables}~ & x, y \rule & \mathsf{a} \mid \mathsf{b} \mid ... \\ & \mbox{Prefixes}~ & p, q \rule & a^+ \mid a^- \mid ~?x \mid ~!s \\ & \mbox{Terms}~ & s, t \rule & ~ p . s \mid s \seq t \mid \succeed \mid s \mathsf{|} t \mid \fail \mid s \pipe t \mid \pass \mid x \mid (s) \end{alignat} }[/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). There are two kinds of prefixes, positive and negative literals. They can only occur on the left hand side of a prefix operator. Sequential composition [math]\displaystyle{ \seq }[/math] constructs ordered pairs. The symbol [math]\displaystyle{ \succeed }[/math] denotes an empty sequence which can be interpreted as successful termination. Alternative composition [math]\displaystyle{ \alt }[/math] connects a pair of alternatives. [math]\displaystyle{ \fail }[/math] denotes an empty set of alternatives, or intuitively failure to find any viable alternative. The [math]\displaystyle{ \pipe }[/math] pipe operator constructs pipelines. Intuitively a pipeline is a transformer with unidirectional data flow. [math]\displaystyle{ \pass }[/math] denotes a passive pipeline that transfers its input unchanged to the output.

For better readability, let's define some syntax sugar that will be used throughout this article. Extend the syntax of terms as follows.

[math]\displaystyle{ \mbox{Terms}~ s, t ::= ... \mid a \pto s \mid a \nto s \mbox{, where} }[/math]

[math]\displaystyle{ \begin{alignat}{1} ~~~~ & a \pto s & = & ~\pos a \seq s \\ ~~~~ & a \nto s & = & ~\neg a \seq s \\ \end{alignat} }[/math]

We name the new operators positive arrow and negative arrow respectively. When it is clear from context, we can call a negative arrow simply an arrow. The precedence and associativity of operators is summarized in the following table.

Summary of operators

Symbol	Associativity	Precedence
[math]\displaystyle{ \seq~\pto~\nto }[/math]	right	highest
[math]\displaystyle{ \mid }[/math]	right
[math]\displaystyle{ \rhd }[/math]	right	lowest

Equational theory

Pipe-calculus can be studied as a process algebra . The following identities are satisfied by all [math]\displaystyle{ s, t, u }[/math] pipe-calculus terms.

[math]\displaystyle{ \def\seq{\mathrel{;}} \def\succeed{\textbf{succeed}} \def\alt{\mid} \def\fail{\textbf{fail}} \def\pipe{\rhd} \def\pass{\textbf{pass}} \def\eq{ = ~} }[/math]Sequential composition is associative with left neutral element [math]\displaystyle{ \succeed }[/math] and left absorbing element [math]\displaystyle{ \fail }[/math].

[math]\displaystyle{ \begin{align} (s \seq t) \seq u \eq & s \seq (t \seq u) \\ \succeed \seq s \eq & s \\ \fail \seq s \eq & \fail \\ \end{align} }[/math]

Alternative composition is associative, commutative and idempotent with neutral element [math]\displaystyle{ \fail }[/math] and absorbing element [math]\displaystyle{ \succeed }[/math].

[math]\displaystyle{ \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 \\ \succeed \alt s \eq & \succeed \\ \fail \alt s \eq & s \\ \end{align} }[/math]

Sequential composition is right distributive over alternative composition.

[math]\displaystyle{ \begin{align} (s \alt t) \seq u \eq & s \seq u \alt t \seq u \end{align} }[/math]

Pipe is associative with right neutral element [math]\displaystyle{ \pass }[/math].

[math]\displaystyle{ \begin{align} (s \pipe t) \pipe u \eq & s \pipe (t \pipe u) \\ s \pipe \pass \eq & s \\ \end{align} }[/math]

Normal forms

Normal form of pipe-calculus terms is defined by a term rewriting system. A term is in normal form if no rewrite rule applies to it.

[math]\displaystyle{ \def\seq{\mathrel{;}} \def\succeed{\textbf{succeed}} \def\alt{\mid} \def\fail{\textbf{fail}} \def\pipe{\rhd} \def\pass{\textbf{pass}} \def\rew{\Rightarrow~} }[/math] [math]\displaystyle{ \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 \\ \succeed \seq s \rew & s \\ \fail \seq s \rew & \fail \\ \\ (s \alt t) \alt u \rew & s \alt t \alt u \\ \pos a \seq s \alt \pos a \seq t \rew & \pos a \seq (s \alt t) \\ \neg a \seq s \alt \neg a \seq t \rew & \neg a \seq (s \alt t) \\ \fail \alt s \rew & s \\ s \alt \fail \rew & s \\ \succeed \alt s \rew & \succeed \\ s \alt \succeed \rew & \succeed \\ \end{alignat} }[/math]

Differently from other combinators, rules for [math]\displaystyle{ \pipe }[/math] has to be attempted in the listed order. As it fails in the default case, [math]\displaystyle{ \pipe }[/math] never occurs in normal forms.

[math]\displaystyle{ \begin{alignat}{1} \pos a \seq s \pipe \neg a \seq t \rew & s \pipe t \\ 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) \\ s \pipe t \rew & \fail \\ \end{alignat} }[/math]

Connection with 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. 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.

• Actions are the atomic units of behavior.
• Actions with sequential and alternative composition form basic process algebra (BPA).
• The pipe operation can be seen as a restricted, unidirectional parallel composition.

There are also notable differences.

• Communication primitives in mainstream process calculi often inseparably unite two conceptual steps: the selection of a communication target (e.g. a channel or another process) and the act of message sending. For example Π-calculus defines input prefixing [math]\displaystyle{ c\left(x\right).P }[/math] and output prefixing [math]\displaystyle{ \overline{c} \langle y \rangle.P }[/math] to denote receiving a name via channel [math]\displaystyle{ c }[/math] and sending a name via channel [math]\displaystyle{ c }[/math] respectively, before proceeding as [math]\displaystyle{ P }[/math]. Although one can introduce as a 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 hiding that prevents interference between two groups of processes that are 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

Questions to be answered

• Is pipe associative?
• In general, what kind of equality should be used for deciding the commutativity and associativity of combinators?
• As a process calculus, is it a linear time or branching time system?