Pipe-calculus

Pipe-calculus is a core calculus for programming.

Note: Pipe-calculus is work in progress. This wiki page reflects the author's understanding of the topic, 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 and task automation, although it is not famous about its 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.

• read s checks if the next symbol of the input stream is s. On failure aborts the current branch of the program.
• 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.

copyNat = read S; write S; run copyNat | read Z; write Z

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

addNat = read S; write S; run addNat | read Z; run copyNat

The idea is simple. We skip the symbol Z that terminates the first number and pass on everything else. Nevertheless this language is 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 used 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 inspired by logical programming, substructural logic, process calculus, formal grammars, automata theory, type theory (up to the lambda-cube) and the study of 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. The author is interested in finding correspondence between variants of the pipe-calculus and classes of formal languages.
• Untyped lambda calculus can be translated to a subset of higher-order pipe-calculus.

Variants and computational power

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

The most simple variant of the calculus that is lacking variables and 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 and with a stack. Clarifying the computational power of specific variants of the calculus is also an ongoing effort.

Zero-order calculus

Syntax

[math]\displaystyle{ \def\seq{\mathrel{;}} \def\sync{\mathsf{sync}~} \def\null{\textbf{0}} \def\fail{\textbf{fail}} \def\pto{\mathrel{\to\mkern-17mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern10mu}}} \def\nto{\to} \begin{alignat}{3} & \mbox{Atoms}~ & a, b & ::= \mathsf{Foo} \mid \mathsf{Bar} \mid ... \\ & \mbox{Literals}~ & l, m & ::= a \mid \neg a \\ & \mbox{Primary terms}~ & a, b & ::= \sync l \\ & \mbox{Sequences}~ & s, t & ::= a \seq s \mid a \mid \null \\ & \mbox{Choices}~ & c, d & ::= s \mathsf{|} c \mid s \mid \fail \\ & \mbox{Pipelines}~ & p, q & ::= c \rhd p \mid c \\ \end{alignat} }[/math]

Atoms are unscoped symbols. We assume a finite set of atoms that is disjunct from the set of constants (operators and constant symbols).

Literals are atoms with polarity. We say that a literal of the form [math]\displaystyle{ a }[/math] is positive, while [math]\displaystyle{ \neg a }[/math] is negative.

There is only one kind of primary term, which is synchronization.

Sequences are ordered lists of primary terms. The symbol [math]\displaystyle{ \textbf{0} }[/math] denotes an empty sequence. In certain contexts it can be interpreted as success.

Nondeterministic choice is an enumeration of alternatives. [math]\displaystyle{ \textbf{fail} }[/math] denotes the lack of choices, or intuitively a failure to find any viable alternative.

The pipe operator connects a number of choices into pipelines.

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

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

[math]\displaystyle{ \begin{alignat}{4} ~~~~ & a \pto s & = & ~\sync a & \seq s \\ ~~~~ & a \nto s & = & ~\sync \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.

Note that the basic calculus does not allow the use of parentheses for grouping and disambiguation. They will be introduced later as an extension. The above grammar determines the precedence and associativity of operators, which is summarized in the following table.

Summary of operators

Symbol	Name	Associativity	Precedence
[math]\displaystyle{ \seq~\pto~\nto }[/math]	Sequence and arrows	right	highest
[math]\displaystyle{ \mid }[/math]	Nondeterministic choice	right
[math]\displaystyle{ \rhd }[/math]	Pipe	right	lowest