7
$\begingroup$

There are many sources cite that simply typed lambda calculus extended with fixed-point combinator is Turing complete. For example, Does there exist a Turing complete typed lambda calculus? or the following quote from Boltzmann Samplers for Closed Simply-Typed Lambda Terms (2017).

Extended with a fix-point operator, simply-typed lambda terms can be used as the intermediate language for compiling Turing-complete functional languages.

However, I haven't found proof of this statement.

Could you please suggest where I could find the proof or the guideline of how to prove this statement? Thank you.

$\endgroup$
  • $\begingroup$ I think you need to be a bit more precise. Do you mean to say that for every type $\tau$ there is a fixed-point combinator $Y_\tau : (\tau \to \tau) \to \tau$? Also, what sort of primitive types do you have? Have you got natural numbers, for instance? $\endgroup$ – Andrej Bauer Feb 11 '17 at 19:26
  • 1
    $\begingroup$ This is a duplicate of mathoverflow.net/questions/261934/… Delete this question because it is better suited for the other forum. And in the future, please do not ask the same question twice. You are wasting everyone's resources. $\endgroup$ – Andrej Bauer Feb 11 '17 at 19:28
  • $\begingroup$ For the first question, I mean there is fixed-point combinator $Y_\tau$ for every type $\tau$. For the second question, only one base type $\alpha$ is given, e.g., int is expressed as $(\alpha\rightarrow\alpha)\rightarrow\alpha\rightarrow\alpha$. $\endgroup$ – kittyphon Feb 12 '17 at 1:58
  • $\begingroup$ and I'm sorry for duplicate cross post. I have already deleted another one. Thank you for your advice. $\endgroup$ – kittyphon Feb 12 '17 at 2:02
4
$\begingroup$

The simply-typed $\lambda$-calculus with the fixpoint combinator but without a primitive integer type is not Turing-complete, at least not in the usual sense (Church integers and computation as $\beta$-reduction). This is a consequence of a result of Statman [1], stating that (somewhat surprisingly) termination in that calculus is decidable.

Perhaps what you want is the simply-typed $\lambda$-calculus with a fixpoint combinator and a primitive integer type, together with its constructors (zero and successor) and destructors (ether a single "case" destructor, or if-then-else and predecessor). This is known as PCF and showing that it is Turing-complete is a straightforward programming exercise (I don't think there is a reference for it in the literature).

[1] Richard Statman. On the lambdaY calculus. Ann. Pure Appl. Logic 130(1-3): 325-337 (2004)

$\endgroup$
  • $\begingroup$ In Section 3 of "LCF considered as a programming language" (1977) sciencedirect.com/science/article/pii/0304397577900445, it is said that, using denotational semantics, nonterminating programs will denote $\bot$. Does it mean that termination in PCF is decidable? $\endgroup$ – kittyphon Feb 14 '17 at 15:59
  • $\begingroup$ No, it does not! Termination in PCF is undecidable, because PCF is Turing-complete. In fact, this simply means that it is undecidable to tell whether the interpretation of a program is $\bot$. $\endgroup$ – Damiano Mazza Feb 14 '17 at 17:33
  • $\begingroup$ Can one have if-then-else without a built-in predecessor, or are both required? And what do you mean by a case destructor? $\endgroup$ – user76284 Feb 28 at 16:22
  • $\begingroup$ Sorry, I realize what I wrote is not self-explanatory. By if-then-else I mean "test for zero": if N then P else Q reduces to P if N reduces to a term of the form S(M) (S being the successor) and to Q if N reduces to 0. By "case destructor" a mean a term of the form case N of 0.P | Sx.Q (which is of type $A$ if N is of integer type and P,Q have type $A$), which reduces to P if N reduces to 0 and to Q[M/x] if N reduces to S(M). The predecessor is obviously definable from the case destructor. On the contrary, it is not definable from if-then-else alone. $\endgroup$ – Damiano Mazza Mar 4 at 15:46
4
$\begingroup$

Damiano is right, the answer is no: it is not Turing complete.

Supposing to define natural numbers as some type (o->o)->o->o, even with fixpoints you cannot define the predecessor (that would be enough to have equality, and then, by Goedel characterization via mu-recursion, all computable functions).

In fact, by just adding fixpoints you only get partial polynomials instead of the total polynomials of the traditional calculus. This can also be seen by generalizing Schwichtenberg approach (see e.g. Functions Definable in the Simply-Typed Lambda Calculus) Instead of normal forms you must consider bohm-trees, now, that have very limited shapes due to typing constraints. Head variables in terms are the same as in the traditional case, and the proof proceeds in a very similar way.

$\endgroup$
  • $\begingroup$ Welcome to MathOverflow, Professor Asperti! $\endgroup$ – Todd Trimble Feb 13 '17 at 22:44

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.