283
edits
Pipe-calculus: Difference between revisions
→Motivation and brief story
KalmanKeri (talk | contribs) (→Syntax) |
KalmanKeri (talk | contribs) |
||
| Line 6: | Line 6: | ||
== Overview == | == Overview == | ||
=== Motivation | === Motivation === | ||
Development of pipe-calculus stemmed from the idea that syntax should be a first class element of programming languages | Development of pipe-calculus stemmed from 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 that complies with this principle is able to recognize the syntax of input data without using a parser library. Pipe-calculus is a 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. | 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 | On the practical side pipe-calculus is motivated by shell programming, which is largely based on text streams and composable 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. The idea of stream processing [] also occurs in functional programming, although it didn't receive much attention. | ||
How would a stream processing language look like? To get a taste, consider a program that adds two natural numbers encoded in [[wikipedia:Unary_numeral_system|unary numeral system]], a popular example in theoretical computer science. Suppose that we send both numbers through a stream as a series of <code>S</code> symbols terminated by a symbol <code>Z</code>. Our programming language consists of the following expressions. | |||
* <code>read s</code>: check if the next symbol of the input stream is <code>s</code>. On failure abort the current branch of the program. | |||
* <code>write s</code>: write the symbol <code>s</code> to the output stream. | |||
* <code>run x</code>: run a program given its name. | |||
* <code>p ; q</code>: run <code>p</code> then run <code>q</code> unless p fails. | |||
* <code>p | q</code>: fork the current program so that one branch runs <code>p</code>, the other branch runs <code>q</code>. | |||
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 the program that adds two numbers. | |||
addNat = read S; write S; run addNat | read Z; run copyNat | |||
The idea is simple. We remove the symbol <code>Z</code> 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 facility that allows the accumulation of the first number and reading it back symbol by symbol as we read the second number. | |||
=== Connection to other fields === | === Connection to other fields === | ||