This page is temporary home of immature 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 this task proves Turing-completeness. 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 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 pipe, there is no way to produce neutral applications, hence we can normalize only closed lambda terms, but it seems acceptable for 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]