Work-in-progress - Revision history

KalmanKeri: /* Encoding lambda calculus in pipe-calculus */

2023-05-25T22:06:20Z

Encoding lambda calculus in pipe-calculus

← Older revision		Revision as of 22:06, 25 May 2023
Line 22:		Line 22:
	\end{alignat}		\end{alignat}
	</math>		</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>
			\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.

KalmanKeri at 21:38, 25 May 2023

2023-05-25T21:38:02Z

← Older revision		Revision as of 21:38, 25 May 2023
Line 1:		Line 1:
	This page is temporary home of ~~immature~~ content.		This page is the temporary home of unfinished content.

	== Pipe-calculus and Lambda calculus ==		== Pipe-calculus and Lambda calculus ==

KalmanKeri: /* Encoding lambda calculus in pipe-calculus */

2023-05-25T21:37:05Z

Encoding lambda calculus in pipe-calculus

← Older revision		Revision as of 21:37, 25 May 2023
Line 5:		Line 5:
	=== Encoding lambda calculus in pipe-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.		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.		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.		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 [[Pipe-calculus#Normal_forms\|default rewrite rule]] for <math>\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>		<math>

KalmanKeri: Created page with "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..."

2023-05-25T21:16:28Z

Created page with "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..."

New page

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>
\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>