Work-in-progress

This page is the temporary home of unfinished content.

Pipe-calculus and Lambda calculus

Encoding lambda calculus in pipe-calculus

Lambda calculus is probably the most popular and well researched model of computation. It is an inevitable reference point for any calculus with computational capabilities. One of the most interesting questions is whether (and how) lambda calculus can be encoded into another calculus. Success of such task proves Turing-completeness of a calculus. Untyped pipe-calculus (PC) seems to be an easy target, but we have to be careful not to overlook subtle details. The encoding shown here is demonstrative and comes without a rigorous proof.

By encoding I mean that normalisation of any valid lambda term can be replaced by a three step process. First, the lambda term is translated to a PC term. Second, this PC term is normalised and third, the normal form is translated back to a lambda term. If the lambda term has a normal form, a faithful encoding has to produce it (and only it). If normalisation of a lambda term does not halt, normalisation of the corresponding PC term shouldn't halt either. One also has to be aware of evaluation strategies and length of normal forms, something we neglect here.

The obvious idea is to encode lambda abstraction as input prefixing and lambda application as the pipe operation. This comes with a limitation though. Because of the default rewrite rule for [math]\displaystyle{ \rhd }[/math], there is no way to produce neutral applications, hence we can normalize only closed lambda terms, but it seems to be an acceptable trade-off if we are interested in programming languages. The translation is defined below.

[math]\displaystyle{ \begin{alignat}{1} \def\llbracket{[\![} \def\rrbracket{]\!]} \def\eq{\mathrel{=}\,} \llbracket \lambda x . t \rrbracket \eq & ?x . \llbracket t \rrbracket \\ \llbracket t ~ u \rrbracket \eq & !\llbracket u \rrbracket . \bot \rhd \llbracket t \rrbracket \\ \llbracket x \rrbracket \eq & x \end{alignat} }[/math]

The second step is normalisation. As translations utilize only a narrow fragment of PC, we can narrow down our term rewriting system too.

[math]\displaystyle{ \def\rew{\mathrel{\Rightarrow}\,} \begin{alignat}{2} !s . t \rhd ?x . u \rew & t \rhd u[s/x] \\ \bot \rhd t \rew & t \\ s \rhd t \rew & \bot & \\ \end{alignat} }[/math]

Substitution rules are exactly the same as in lambda calculus.