<p>CPS translations will always use pairs, either explictly or by currying. Though I can't find a reference for that, I'm assuming this is a necessary condition (I'd appreciate a reference if someone has any!). Consider, for example, the CPS target language <a href="https://www.cs.princeton.edu/%7Eappel/papers/shrink.pdf" rel="nofollow noreferrer">used by Appel in here</a>:</p>
<p><span class="math-container">$$M ::= \texttt{let}\ x(x, ..., x) = M\ \texttt{in}\ M \enspace | \enspace x(x, ..., x)$$</span></p>
<p>His language also has pairs, but consider a version of it without them, and in which continuations are unary instead of polyadic, i.e.:</p>
<p><span class="math-container">$$M ::= \texttt{let}\ x(x) = M\ \texttt{in}\ M \enspace | \enspace x(x)$$</span></p>
<p>The first thing that comes to mind to prove that this language is not Turing-complete is by showing strong normalization. However, it's still possible to write looping terms in it, namely, the <span class="math-container">$\Omega$</span> combinator is possible:</p>
<p><span class="math-container">$$\Omega = \texttt{let}\ k(x) = x(x)\ \texttt{in}\ k(k)$$</span></p>
<p>Where <span class="math-container">$\Omega \rightarrow \Omega$</span> in the reduction rules of this calculus (and <span class="math-container">$\beta$</span>-reduction can be simulated for CPS terms in this language). However, as this can't be used as the target for a CPS translation, I'm assuming it's still not Turing-complete.</p>
<p>The same issue happens when we either restrict the syntax of the <span class="math-container">$\lambda$</span>-calculus to:</p>
<p><span class="math-container">$$e ::= v\ v\qquad\qquad\qquad v ::= x\enspace|\enspace\lambda x.e$$</span></p>
<p>It's still possible to write <span class="math-container">$\Omega = (\lambda k.k\ k)\ (\lambda x.x\ x)$</span> as usual, but I don't think we could simulate arbitrary terms into this format. The same issue again would appear in the (<em>asynchronous, localized</em>) <span class="math-container">$\pi$</span>-calculus if we use an unary variant without linear input (i.e., all input has to be under replication):</p>
<p><span class="math-container">$$p ::= \overline{x}\langle x\rangle\enspace|\enspace (\nu x)(p\ |\ !x(x).p)$$</span></p>
<p>Again, <span class="math-container">$\Omega = (\nu k)(\overline{k}\langle k\rangle\ |\ {!k(x).\overline{x}\langle x\rangle }$</span>) and <span class="math-container">$\Omega \rightarrow \Omega$</span>...</p>
<p>So, my question, in a general sense: assuming that these languages are indeed <em>not</em> Turing-complete, or any language that includes looping, how can I prove that?</p>
<p><strong>Edit:</strong> as it has been noticed in the comments, the syntax for the <span class="math-container">$\pi$</span>-calculus I had suggested was not the same as the other two calculi, and perhaps indeed Turing-complete. We should forbid the trick of unrevealing an input from inside another (i.e., a name that wasn't bound to anything yet should continue like that). The fixed syntax above is enough to restrict this, even if we work up to <span class="math-container">$\equiv$</span>. The restriction of a single active output should not matter and could be relaxed without changing the computational power (because we could find a barbed bisimilar term which would be the parallel composition of terms in this syntax, <span class="math-container">$p|...|p$</span> by duplicating inputs).</p>

CC BY-SA 4.0
2023-06-01T18:51:55.247Z
I don't know about the other calculi, but doesn't your lambda calculus allow $λx. (λf. f) (λ y. \ldots)$? So, β reduction doesn't preserve well-formed expressions, but you can still encode multi-argument functions.
Dan Doel
CC BY-SA 4.0
2023-06-01T20:04:31.370Z
@DanDoel, no, it doesn't. Note that expressions are only applications of two values, so we can't have a term $\lambda f.f$ in it (as there's a single variable in the body).
paulotorrens
CC BY-SA 4.0
2023-06-03T12:11:02.643Z
@paulotorrens Is it totally clear that this variant of the $\pi$-calculus is not Turing
complete?  it's known that polyadic $\pi$-calculus can be reduced to
monadic $\pi$-calculus. (P. Quaglia, D. Walker, *Types and full abstraction for polyadic pi-calculus*.) And replicated input (in some sense) contains
non-replicated input, the only difference is that the input doesn't go
away after interaction.
Martin Berger
CC BY-SA 4.0
2023-06-03T12:17:37.737Z
Part of the problem of proofs/disproofs of Turing completeness is that you need to relate a class of functions on natural numbers to your model of computation, but neither $\lambda-$ nor $\pi-$calculus have built-in natural numbers, instead we encode them. So a disproof of Turing completeness needs, in some sense, rule out all possible (computable) encodings.
Martin Berger
CC BY-SA 4.0
2023-06-03T20:16:26.067Z
Yeah, I thought about this a bit, and it seems like it might be feasible to prove that e.g. the identity function cannot be represented in the λ example, where λ term application is used to encode function application (because $\mathsf{I}\ t = t$ must β relate two different classes of terms, assuming that that can't happen). However, it is unclear that such a proof would extend to _every possible encoding_ of functions into the calculus.
Dan Doel
CC BY-SA 4.0
2023-06-03T20:40:33.753Z
@MartinBerger, it's not totally clear to me that it is not Turing-complete, but I highly believe it is. I don't think the polyadic $\pi$-calculus can be reduced to the unary one without relying on linear input, is it? The proofs I've seen (including the one you mention) rely on it and the fact that a channel can be treated differently in a sequential way (by sending each argument in a row), which needs linear input. This is exactly why I gave the $\pi$-calculus example, I believe it would represent the same class of problems and perhaps someone has looked into it already.
paulotorrens
CC BY-SA 4.0
2023-06-03T20:44:02.860Z
@DanDoel, I've been thinking about this, and I _think_ I can show that, if there is any free variable in the term, then it is equivalent to a strictly smaller term, and we can then show that in these languages, every closed term loops. So it would means that halting for these languages is decidable, so it can't be Turing-complete. I'm still trying to figure out the details (and if this method would even work).
paulotorrens
CC BY-SA 4.0
2023-06-03T23:12:49.030Z
(1/3) @paulotorrens *Really interesting problem.* Maybe it's possible to progress like
this: Assume  a map $\phi$ from names to pairs of names that
is strongly injective: i.e. whenever $x \neq y$ and $\phi(x) =
(x_1, x_2)$, $\phi(y) = (y_1, y_2)$, then $\{x_1, x_2\}$ and $\{y_1,
y_2\}$ are disjoint.
Martin Berger
CC BY-SA 4.0
2023-06-03T23:19:26.637Z
(2/3) Then we translate the asynchronous $\pi$-calculus with binary
communication (general polyadic case is similar) into the monadic
fragment where all input is replicated as follows.  $ \lbrack\!\lbrack
\overline{x}\ {yz}\rbrack\!\rbrack =
\overline{x_1}\ {y}.\overline{x_2}{y}. \lbrack\!\lbrack P\rbrack\!\rbrack$, $
\lbrack\!\lbrack x(yz)\rbrack\!\rbrack =
!x_1(y).!x_2(y). \lbrack\!\lbrack P\rbrack\!\rbrack$, $
\lbrack\!\lbrack !x(yz).P \rbrack\!\rbrack = \lbrack\!\lbrack
x(yz).P\rbrack\!\rbrack$,
Martin Berger
CC BY-SA 4.0
2023-06-03T23:19:46.137Z
(3/3) $ \lbrack\!\lbrack (\nu
x)P\rbrack\!\rbrack = (\nu x_1)(\nu x_2) \lbrack\!\lbrack
P\rbrack\!\rbrack$.  $ \lbrack\!\lbrack P|Q\rbrack\!\rbrack =
\lbrack\!\lbrack P\rbrack\!\rbrack | \lbrack\!\lbrack
Q\rbrack\!\rbrack$.  Here $\phi(x) = (x_1, x_2)$.
Martin Berger
CC BY-SA 4.0
2023-06-03T23:19:52.827Z
This would go wrong if there are outputs that could go to replicated
and non-replicated inputs, e.g. $\overline{x}{}\ y\ |\ x(v).P \ |\
!x(v).Q$.  But I am not sure this is needed in order to achieve
Turing completeness. Indeed the standard Milner encoding of
$\lambda$-calculus into $\pi$ never does this.
Martin Berger
CC BY-SA 4.0
2023-06-04T00:12:07.660Z
Above the translation of output should of course be: $ \lbrack\!\lbrack \overline{x}{yz}\rbrack\!\rbrack = \overline{x_1}{y} \ |\ \overline{x_2}{z}$. Likewise $
\lbrack\!\lbrack x(yz)\rbrack\!\rbrack =
!x_1(y).!x_2(z). \lbrack\!\lbrack P\rbrack\!\rbrack$

All this can still go wrong if the processes in question are too 'wild'. But I fear that one needs a subtle argument to show that Turing completeness needs 'wild' processes.
Martin Berger
CC BY-SA 4.0
2023-06-04T00:12:10.940Z
@MartinBerger, you're right. The subset of the $\pi$-calculus that would be equivalent to the other two languages is slightly different, as it would need (1) only one active output, and (2) a binding structure closer to the $\pi$-calculus. I had written that down, but I wasn't careful enough when asking this question. The syntax, as I've given it, is probably Turing-complete as you described. I'm gonna edit the question; thanks for noticing this, and sorry about that!
paulotorrens
CC BY-SA 4.0
2023-06-04T01:16:46.820Z
Is it possible that every language in the class is decidable?  Showing that would be one way to show that the class is not Turing complete.
Neal Young
CC BY-SA 4.0
2023-06-04T18:23:41.200Z
@paulotorrens Maybe I don't quite understand, but isn't $x\ x$ not equivalent to anything smaller? And isn't $λ x. x\ x$ a closed term that doesn't loop? However, something along those lines does seem promising. For instance, there are no closed normal forms _in class_ $e$. Maybe there is some broader classification that lets you decide normalization.
Dan Doel
CC BY-SA 4.0
2023-06-06T17:14:20.663Z
Ok really stupid question: is there a bound on the size that terms can get (as a computable function of the size of the original term)? If so, then that pretty much settles it.
cody
CC BY-SA 4.0
2023-06-08T12:00:38.650Z
@cody If you set $\newcommand{\OUT}[2]{\overline{#1}\langle #2 \rangle}
\newcommand{\IN}[2]{#1(#2)} p = \OUT{x}{x}\ | \ \OUT{x}{x} $ then doesn't  $ (\nu x)(p \ |\
!\IN{x}{x}.p) $ grows without bounds?
Martin Berger
CC BY-SA 4.0
2023-06-08T13:39:13.760Z
@DanDoel, yeah, I meant that there are no halting closed terms in $e$. I _think_ that, for any term in $e$ with free variables, I can get a $\beta$-equivalent term in $e$ that's smaller (and $\beta$-reduction preserves the class $e$, thus by confluence, they have the same result). For the $\pi$-calculus, we can use barbed congruence similarly. If that's the case, by induction on the size, it should either reduce to some trivially halting term, or to a closed term, thus halting is decidable. If this can be decided for $e$, it follows for $v$ as well.
paulotorrens
<reference-request><computability><lambda-calculus><pi-calculus>
How to prove that a language that allows infinite loops is still not Turing-complete?
paulotorrens
# How to prove that a language that allows infinite loops is still not Turing-complete?

(Asked by: username_0 on 2023-06-01)

CPS translations will always use pairs, either explictly or by currying. Though I can't find a reference for that, I'm assuming this is a necessary condition (I'd appreciate a reference if someone has any!). Consider, for example, the CPS target language [used by Appel in here](https://www.cs.princeton.edu/%7Eappel/papers/shrink.pdf):

$$M ::= \texttt{let}\ x(x, ..., x) = M\ \texttt{in}\ M \enspace | \enspace x(x, ..., x)$$

His language also has pairs, but consider a version of it without them, and in which continuations are unary instead of polyadic, i.e.:

$$M ::= \texttt{let}\ x(x) = M\ \texttt{in}\ M \enspace | \enspace x(x)$$

The first thing that comes to mind to prove that this language is not Turing-complete is by showing strong normalization. However, it's still possible to write looping terms in it, namely, the $\Omega$ combinator is possible:

$$\Omega = \texttt{let}\ k(x) = x(x)\ \texttt{in}\ k(k)$$

Where $\Omega \rightarrow \Omega$ in the reduction rules of this calculus (and $\beta$-reduction can be simulated for CPS terms in this language). However, as this can't be used as the target for a CPS translation, I'm assuming it's still not Turing-complete.

The same issue happens when we either restrict the syntax of the $\lambda$-calculus to:

$$e ::= v\ v\qquad\qquad\qquad v ::= x\enspace|\enspace\lambda x.e$$

It's still possible to write $\Omega = (\lambda k.k\ k)\ (\lambda x.x\ x)$ as usual, but I don't think we could simulate arbitrary terms into this format. The same issue again would appear in the (*asynchronous, localized*) $\pi$-calculus if we use an unary variant without linear input (i.e., all input has to be under replication):

$$p ::= \overline{x}\langle x\rangle\enspace|\enspace (\nu x)(p\ |\ !x(x).p)$$

Again, $\Omega = (\nu k)(\overline{k}\langle k\rangle\ |\ {!k(x).\overline{x}\langle x\rangle }$) and $\Omega \rightarrow \Omega$...

So, my question, in a general sense: assuming that these languages are indeed *not* Turing-complete, or any language that includes looping, how can I prove that?

**Edit:** as it has been noticed in the comments, the syntax for the $\pi$-calculus I had suggested was not the same as the other two calculi, and perhaps indeed Turing-complete. We should forbid the trick of unrevealing an input from inside another (i.e., a name that wasn't bound to anything yet should continue like that). The fixed syntax above is enough to restrict this, even if we work up to $\equiv$. The restriction of a single active output should not matter and could be relaxed without changing the computational power (because we could find a barbed bisimilar term which would be the parallel composition of terms in this syntax, $p|...|p$ by duplicating inputs).

**Tags:** reference-request, computability, lambda-calculus, pi-calculus

> **Comments:**
> **username_1**: I don't know about the other calculi, but doesn't your lambda calculus allow $λx. (λf. f) (λ y. \ldots)$? So, β reduction doesn't preserve well-formed expressions, but you can still encode multi-argument functions.  
> **username_0**: @DanDoel, no, it doesn't. Note that expressions are only applications of two values, so we can't have a term $\lambda f.f$ in it (as there's a single variable in the body).  
> **username_2**: @username_0 Is it totally clear that this variant of the $\pi$-calculus is not Turing complete?  it's known that polyadic $\pi$-calculus can be reduced to monadic $\pi$-calculus. (P. Quaglia, D. Walker, *Types and full abstraction for polyadic pi-calculus*.) And replicated input (in some sense) contains non-replicated input, the only difference is that the input doesn't go away after interaction.  
> **username_2**: Part of the problem of proofs/disproofs of Turing completeness is that you need to relate a class of functions on natural numbers to your model of computation, but neither $\lambda-$ nor $\pi-$calculus have built-in natural numbers, instead we encode them. So a disproof of Turing completeness needs, in some sense, rule out all possible (computable) encodings.  
> **username_1**: Yeah, I thought about this a bit, and it seems like it might be feasible to prove that e.g. the identity function cannot be represented in the λ example, where λ term application is used to encode function application (because $\mathsf{I}\ t = t$ must β relate two different classes of terms, assuming that that can't happen). However, it is unclear that such a proof would extend to _every possible encoding_ of functions into the calculus.  
> **username_0**: @MartinBerger, it's not totally clear to me that it is not Turing-complete, but I highly believe it is. I don't think the polyadic $\pi$-calculus can be reduced to the unary one without relying on linear input, is it? The proofs I've seen (including the one you mention) rely on it and the fact that a channel can be treated differently in a sequential way (by sending each argument in a row), which needs linear input. This is exactly why I gave the $\pi$-calculus example, I believe it would represent the same class of problems and perhaps someone has looked into it already.  
> **username_0**: @DanDoel, I've been thinking about this, and I _think_ I can show that, if there is any free variable in the term, then it is equivalent to a strictly smaller term, and we can then show that in these languages, every closed term loops. So it would means that halting for these languages is decidable, so it can't be Turing-complete. I'm still trying to figure out the details (and if this method would even work).  
> **username_2**: (1/3) @username_0 *Really interesting problem.* Maybe it's possible to progress like this: Assume  a map $\phi$ from names to pairs of names that is strongly injective: i.e. whenever $x \neq y$ and $\phi(x) = (x_1, x_2)$, $\phi(y) = (y_1, y_2)$, then $\{x_1, x_2\}$ and $\{y_1, y_2\}$ are disjoint.  
> **username_2**: (2/3) Then we translate the asynchronous $\pi$-calculus with binary communication (general polyadic case is similar) into the monadic fragment where all input is replicated as follows.  $ \lbrack\!\lbrack \overline{x}\ {yz}\rbrack\!\rbrack = \overline{x_1}\ {y}.\overline{x_2}{y}. \lbrack\!\lbrack P\rbrack\!\rbrack$, $ \lbrack\!\lbrack x(yz)\rbrack\!\rbrack = !x_1(y).!x_2(y). \lbrack\!\lbrack P\rbrack\!\rbrack$, $ \lbrack\!\lbrack !x(yz).P \rbrack\!\rbrack = \lbrack\!\lbrack x(yz).P\rbrack\!\rbrack$,  
> **username_2**: (3/3) $ \lbrack\!\lbrack (\nu x)P\rbrack\!\rbrack = (\nu x_1)(\nu x_2) \lbrack\!\lbrack P\rbrack\!\rbrack$.  $ \lbrack\!\lbrack P|Q\rbrack\!\rbrack = \lbrack\!\lbrack P\rbrack\!\rbrack | \lbrack\!\lbrack Q\rbrack\!\rbrack$.  Here $\phi(x) = (x_1, x_2)$.  
> **username_2**: This would go wrong if there are outputs that could go to replicated and non-replicated inputs, e.g. $\overline{x}{}\ y\ |\ x(v).P \ |\ !x(v).Q$.  But I am not sure this is needed in order to achieve Turing completeness. Indeed the standard Milner encoding of $\lambda$-calculus into $\pi$ never does this.  
> **username_2**: Above the translation of output should of course be: $ \lbrack\!\lbrack \overline{x}{yz}\rbrack\!\rbrack = \overline{x_1}{y} \ |\ \overline{x_2}{z}$. Likewise $ \lbrack\!\lbrack x(yz)\rbrack\!\rbrack = !x_1(y).!x_2(z). \lbrack\!\lbrack P\rbrack\!\rbrack$  All this can still go wrong if the processes in question are too 'wild'. But I fear that one needs a subtle argument to show that Turing completeness needs 'wild' processes.  
> **username_0**: @MartinBerger, you're right. The subset of the $\pi$-calculus that would be equivalent to the other two languages is slightly different, as it would need (1) only one active output, and (2) a binding structure closer to the $\pi$-calculus. I had written that down, but I wasn't careful enough when asking this question. The syntax, as I've given it, is probably Turing-complete as you described. I'm gonna edit the question; thanks for noticing this, and sorry about that!  
> **username_3**: Is it possible that every language in the class is decidable?  Showing that would be one way to show that the class is not Turing complete.  
> **username_1**: @username_0 Maybe I don't quite understand, but isn't $x\ x$ not equivalent to anything smaller? And isn't $λ x. x\ x$ a closed term that doesn't loop? However, something along those lines does seem promising. For instance, there are no closed normal forms _in class_ $e$. Maybe there is some broader classification that lets you decide normalization.  
> **username_4**: Ok really stupid question: is there a bound on the size that terms can get (as a computable function of the size of the original term)? If so, then that pretty much settles it.  
> **username_2**: @username_4 If you set $\newcommand{\OUT}[2]{\overline{#1}\langle #2 \rangle} \newcommand{\IN}[2]{#1(#2)} p = \OUT{x}{x}\ | \ \OUT{x}{x} $ then doesn't  $ (\nu x)(p \ |\ !\IN{x}{x}.p) $ grows without bounds?  
> **username_0**: @DanDoel, yeah, I meant that there are no halting closed terms in $e$. I _think_ that, for any term in $e$ with free variables, I can get a $\beta$-equivalent term in $e$ that's smaller (and $\beta$-reduction preserves the class $e$, thus by confluence, they have the same result). For the $\pi$-calculus, we can use barbed congruence similarly. If that's the case, by induction on the size, it should either reduce to some trivially halting term, or to a closed term, thus halting is decidable. If this can be decided for $e$, it follows for $v$ as well.  

---

## 0 answers

