How do you say when a language is Turing-complete only in a trivial way?

Question

I didn't know how to ask this question before but now that I'm reading about typed lambda calculus I think I've got a better idea.

There is this answer to a question asking whether CSS is Turing complete or not (note that this question is NOT about CSS at all), which I consider is not (at least in certain way, and this "certain" is what my question below is about), even if you can simulate Rule 110 with it, which is proven to be Turing complete. My intuition behind it is that only an insignificant subset of what CSS can output can be the result of a calculation. You cannot perform any calculation on colors or sizes to be set to element's styles.

Now I found an even simpler example while reading about typed lambda calculus. This article's overview describes a lambda calculus that can use booleans. I noticed that, in addition to the untyped lambda calculus operations, there is the conditional operation (if t1 then t2 else t3), which makes perfect sense. Without this, you wouldn't be able to do anything with booleans, and I would go ahead and say is really not Turing complete, or at least that is Turing complete but only in a trivial way.

So my question is, if this typed lambda calculus with booleans wouldn't have that conditional operator, would you say is Turing complete? If not, why not, and if yes, how would you express the fact that you cannot do any operation at all on it's main type of data which is what you'd expect from any Turing complete language in a categorical, technical way such that is clear that the Turing completeness of the language is really meaningless?

The reason why I'm giving so much importance to this is because I was recently trying to create a small Turing complete language myself and while doing it, got to a point in which my language was Turing complete but only in this trivial way (wasn't as obvious as the boolean lambda calculus without conditionals above, though). If I would have asked "Is this language Turing complete?" I would have probably got "Yes" as an answer and I would've think I'm done creating my language. But I really was not. And when asking myself why am I still working on my language, I'd like to be able to state exactly what is that my language is missing.

Answer 1

Untyped or simply-typed lambda-calculus is Turing-complete even with no booleans at all. Adding more stuff in the language, such as boolean constants and a boolean base types, cannot make the language less powerful, therefore it is still Turing-complete.

“Turing-complete” means that there is some “reasonable encoding” under which the language can express arbitrary computations. “Reasonable encoding” is not a formal notion; what it really means is that you must say what you consider to be computation, and how natural integers are to be encoded. For example, in the lambda-calculus, computation is beta reduction, and one possible encoding of natural integers is Church numerals.

In the simply-typed lambda calculs, there are no booleans as a built-in notion, but they can be encoded: $$\begin{align} \mathsf{true}_\tau &:= \lambda x\colon\tau. \lambda y\colon\tau. x \\ \mathsf{false}_\tau &:= \lambda x\colon\tau. \lambda y\colon\tau. x \\ \mathsf{ifthenelse}_\tau &:= \lambda f\colon\tau. \lambda g\colon\tau. \lambda b\colon(\tau\rightarrow\tau\rightarrow\tau). b \, f \, g \\ \end{align}$$

The lambda calculus with boolean constants but no corresponding destructor¹ nor any way to encode it (such as a polymorphic equality construct) does lack expressive power in a sense, but only in that it is unable to distinguish between the two boolean values. It isn't the language's computational power which is at state, but the particular encoding of booleans as the boolean constants you picked: the boolean data structure is not implemented correctly. In fact, that language does not have any boolean data structures: it has constants that you chose to call “true” and “false”, but that doesn't make them booleans given the lack of a destructor.

Consider a variant where you define the following constructors and destructor: $$ \dfrac{}{\Gamma \vdash \mathsf{dog} : \mathsf{daisy}} \qquad \dfrac{}{\Gamma \vdash \mathsf{cat} : \mathsf{daisy}} \qquad \dfrac{\Gamma \vdash M : \mathsf{daisy} \quad \Gamma \vdash N_0 : \tau \quad \Gamma \vdash N_1 : \tau}{\Gamma \vdash \mathsf{cheese}(M, N_0, N_1) : \tau} \\ \dfrac{}{\Gamma \vdash \mathsf{true} : \mathsf{boolean}} \qquad \dfrac{}{\Gamma \vdash \mathsf{false} : \mathsf{boolean}} $$ and the following reduction rules: $$\begin{align} \mathsf{cheese}(\mathsf{dog},M,N) &\to M \\ \mathsf{cheese}(\mathsf{cat},M,N) &\to N \\ \end{align}$$

This language has an encoding of the booleans as the type $\mathsf{daisy}$, with $\mathsf{cat}$ and $\mathsf{dog}$ as the constructors and $\mathsf{cheese}$ as the destructor. The type $\mathsf{boolean}$ is not a boolean type: it's just some type that happens to have two values (which are undistinguishable).

A “typed lambda calculus with booleans [without] that conditional operator” is a Turing-complete language that doesn't have booleans.

¹ _{A destructor in a typed calculus is a term such that a type constructor appears in the premises of its typing rules but not in the type of its conclusion. If/then/else is a destructor for booleans.}