283
edits
Pipe-calculus: Difference between revisions
→Overview
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 10: | Line 10: | ||
'''Note:''' Pipe-calculus is a work in progress. This wiki page reflects the current status of the project and details may well change over time.</div> | '''Note:''' Pipe-calculus is a work in progress. This wiki page reflects the current status of the project and details may well change over time.</div> | ||
== | == Introduction == | ||
=== Motivation === | === Motivation === | ||
| Line 42: | Line 42: | ||
Pipe-calculus can be seen as a framework to study the required extensions that turn this tiny language into a practical programming language. | Pipe-calculus can be seen as a framework to study the required extensions that turn this tiny language into a practical programming language. | ||
=== Connection | === Connection with other fields === | ||
Pipe-calculus is | Pipe-calculus is presented as a process calculus. Although it significantly differs from typical process calculi, it still lends itself to this style of presentation. | ||
Its development is also inspired by | Its development is also inspired by | ||
[[Wikipedia:Higher-order_logic_programming|higher-order logic programming]], | [[Wikipedia:Higher-order_logic_programming|higher-order logic programming]], | ||
[[Wikipedia:Automata_theory|automata theory]], | [[Wikipedia:Automata_theory|automata theory]], | ||
[[Wikipedia:Type_theory|type theory]] (up to the [[Wikipedia:Lambda_cube|lambda-cube]]) and | [[Wikipedia:Type_theory|type theory]] (up to the [[Wikipedia:Lambda_cube|lambda-cube]]) and | ||
| Line 57: | Line 56: | ||
In certain cases the connection can be made more precise. | 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 | * 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 (to be specified later). | * Untyped lambda calculus can be translated to a subset of higher-order pipe-calculus (to be specified later). | ||