9
$\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.

Improve this question
$\endgroup$
4
  • $\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
    Commented Feb 11, 2017 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
    Commented Feb 11, 2017 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
    Commented Feb 12, 2017 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
    Commented Feb 12, 2017 at 2:02

2 Answers 2

Reset to default
7
$\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)

Improve this answer
$\endgroup$
4
  • $\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
    Commented Feb 14, 2017 at 15:59
  • 1
    $\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
    Commented Feb 14, 2017 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
    Commented Feb 28, 2019 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
    Commented Mar 4, 2019 at 15:46
6
$\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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Welcome to MathOverflow, Professor Asperti! $\endgroup$
    – Todd Trimble
    Commented Feb 13, 2017 at 22:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .