1
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ Please try to clarify precisely what it is you're asking. As it is, it's hard to imagine a meaningful distinction between "useful" and "academic" Turing-equivalence of computing systems; it's an inherently academic concept and any associated usefulness of some Turing-equivalent systems is probably orthogonal. A better way to couch this might be "what makes a computing system (e.g., programming language on some hardware) useful?" Then you can point out Turing-equivalent systems which you don't think fit what a definition of "useful" should include, to help further clarify. $\endgroup$ – Patrick87 Oct 4 '13 at 16:09
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Exactly, or like adding integers to lambda calculus and all kinds of fancy operations on them like outputting them upside down or in italics, but lacking the ability to perform any math operation or comparisons among them, if not a way to encode them to and from some language's native data such as Church numerals (which is a lot like what's happening on CSS). I don't know, I still feel something is wrong with saying that language would be Turing complete. I'd probably say a subset of the language is, but not the whole language (I mean look at CSS!). $\endgroup$ – Juan Oct 5 '13 at 1:48
  • $\begingroup$ @JuanLuisSoldi If a subset of the language is Turing complete, then the whole language trivially is. $\endgroup$ – Gilles Oct 5 '13 at 1:52
  • $\begingroup$ It may seem that I'm just being picky, but if I take as rule of thumb for a language to be Turing complete to be able to simulate any Turing machine (which seems to be the consensus), then one may think that taking any language and dropping lambda calculus into it without a comprehensive way to map from and to the original language would do the trick. Which yea, makes it Turing complete but obviously misses the whole point of making it Turing complete. This "comprehensive mapping" system is what I'm concerned about, and I wonder if some theory exists around it. $\endgroup$ – Juan Oct 5 '13 at 2:05
  • $\begingroup$ @JuanLuisSoldi Turing completeness doesn't imply anything about what you can do with data structures, it's defined in terms of input and output or other encoding of computation. What you're looking for is something like correct implementation of data structures. It's definitely a matter of data structure encoding and not a matter of Turing completeness. $\endgroup$ – Gilles Oct 5 '13 at 2:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.