# How to prove that a language that allows infinite loops is still not Turing-complete?

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:

$$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).

• 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. Jun 1, 2023 at 18:51
• @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). Jun 1, 2023 at 20:04
• 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. Jun 3, 2023 at 12:17
• 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. Jun 3, 2023 at 20:16
• (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. Jun 3, 2023 at 23:12