Pipe-calculus is a core calculus for programming.
{{#if: {{#if:||{{#if:|demo|}} }} | <templatestyles src="Note/styles.css" />
| File:OOjs UI icon lightbulb-20 fc3.svg <translate> Note:</translate> }} Pipe-calculus is work in progress. This wiki page serves as an informal introduction, and details may change by time.
Overview
Motivation and brief story
Development of pipe-calculus stemmed from the author's conviction 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. The author's interest in process calculus led him to the realization that well-typed parsing can be translated to a calculus that uses combinators and rewriting rules instead of inference rules.
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. Its early version was considered a process calculus. However it has since diverged in subtle details, it is still very close to process calculi and its presentation style maintains that heritage.
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. Extensions add various features to the basic calculus. One such important feature is the inclusion of variables. Variants without variables and any kind of scoped construction are called zero-order. Somewhat surprisingly, even the zero-order calculus has a limited computational power. On the other end of the scale there are higher-order variants where variables 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