Pipe-calculus is a core calculus for programming.
Overview
Motivation and brief story
Development of pipe-calculus stemmed from the idea that syntax should be a first class element of programming languages the same way as formation rules are integral part of logical systems. A language that complies with this principle is able to recognize the syntax of input data without using a parser library. Pipe-calculus is a very minimal language with this capability.
The first attempt to implement this idea resulted in a logical system which is referred to as well-typed parsing. Later it was realised that well-typed parsing can be translated to a calculus that uses combinators and rewriting rules instead of axioms and inference rules, and this is the basis of the current formalisation.
On the practical side pipe-calculus is motivated by shell programming, streams and operating system processes. Indeed the idea of the pipe combinator comes from shell scripting.
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. [1]
There is only one kind of primary term, which is synchronization. [2]
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.
| Symbol | Name | Associativity[3] | 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 |
Notes
- ↑ See Literal (mathematical_logic) on literals in general.
- ↑ Adding new primary terms and the respective rules is a typical way of extending pipe-calculus.
- ↑ 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 Operator associativity.