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 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 inference rules, and this is the basis of the current formalisation.

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.

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.

On the practical side pipe-calculus is motivated by shell programming and streams. Indeed the idea of the pipe combinator comes from shell scripting.

Variants

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 higher-order variants 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.

When used as recognizers, extended variants of the calculus can generally recognize more expressive formal languages.

Zero-order calculus

Syntax

Atoms and literals are building blocks of terms, but not terms themselves.

[math]\displaystyle{ \mbox{Atoms}~ A, B ::= \mathsf{Foo} ~|~ \mathsf{Bar} ~|~ ... }[/math]

[math]\displaystyle{ \mbox{Literals}~ l, m ::= A ~|~ \neg A }[/math]

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. See Literal (mathematical_logic) for more details on literals in general.

Primitive terms