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

  • 1
    $\begingroup$ 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. $\endgroup$
    – Dan Doel
    Commented Jun 1, 2023 at 18:51
  • 1
    $\begingroup$ @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). $\endgroup$ Commented Jun 1, 2023 at 20:04
  • 2
    $\begingroup$ 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. $\endgroup$ Commented Jun 3, 2023 at 12:17
  • 1
    $\begingroup$ 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. $\endgroup$
    – Dan Doel
    Commented Jun 3, 2023 at 20:16
  • 1
    $\begingroup$ (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. $\endgroup$ Commented Jun 3, 2023 at 23:12


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.