5
$\begingroup$

It's well known that the computation models untyped lambda calculus and $\mu$-recursive function are equivalent in terms of computability (in fact they are both Turing complete.) It is also well known that, among some of the variations of them, the simply typed lambda calculus ($\lambda_{\rightarrow}$) and the primitive recursive function ($R_p$), are less powerful (i.e. neither of them is Turing complete.)

Since the intuition of the essential restrictions applied in both cases feels similar, I have the instinct that the class of functions computable by either of them is the same, i.e. $\lambda_{\rightarrow} \cong R_p $; but I cannot find any literature discussing this issue myself after a quick search.

Thus, I'd like to ask 1) whether simply typed lambda calculus and primitive recursive function are equivalent and 2) if so, is there any literature that I can have a look at discussing this?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ The simply typed lambda calculus is still also a formal system. The untyped lambda calculus is inconsistent as a formal system due to Curry's paradox. For the usual deduction rules, the simply typed lambda calculus is equiconsistent with Mac Lane set theory (bounded ZF). Strange enough, this does not tell us much about its computational strength. $\endgroup$
    – Thomas Klimpel
    Jul 7, 2017 at 10:04
  • $\begingroup$ @ThomasKlimpel I believe you're referring to Churche's "simple type theory", which is a theory closely related to the foundational logics in the implementations of HOL and Isabelle/HOL. It does contain the STLC, but it also contains axioms expressing logical rules, see e.g. here: plato.stanford.edu/entries/type-theory-church $\endgroup$
    – cody
    Jul 7, 2017 at 14:42
  • 1
    $\begingroup$ @cody Adrian Mathias, in "The strength of Mac Lane set theory", talks about the "known equiconsistency of [Mac Lane set theory] with the simple theory of types", but I don't think Mathias means the system developed by Church in "A Formulation of the Simple Theory of Types" or its extensions like HOL. I think Mathias means a simplification of the ramified theory of types by Russell and Whitehead. Not sure this is what Thomas has in mind, maybe he can clarify. $\endgroup$
    – Martin Berger
    Jul 7, 2017 at 15:14
  • 1
    $\begingroup$ @MartinBerger From a consistency point of view, those systems have essentially the same strength. Or rather, you have the freedom to make them as strong as desired, but a certain "base strength" is hard to avoid. I do think of Church's "simple type theory" (i.e. HOL), especially theorem 7 on page 21 of William Farmer's The Seven Virtues of Simple Type Theory. But SEP is also a great resource, see links given in type theory as foundations $\endgroup$
    – Thomas Klimpel
    Jul 7, 2017 at 18:03

1 Answer 1

Reset to default
7
$\begingroup$

The simply-typed λ-calculus with β-equality at type (o → o) → o → o (which can be seen as type of the natural numbers, whenever o is any base type) can define exactly the extended polynomials (= polynomials with if-then-else), see (1). Other notions of equality change this. (2) shows that using $\beta\eta$-equality leads to a larger class of definable functions, although no simple characterisation is given.

Schwichtenberg's result can be generalised to functions on words over the binary alphabet, represented as type (o → o) → ((o → o) → o → o), see (3), and also to free algebras, see (4).

  1. H. Schwichtenberg, Definierbare Funktionen im λ-Kalkül mit Typen.

  2. M. Zakrzewski, Definable Functions in the Simply Typed λ-Calculus.

  3. M. Zaionc, Word operation definable in the typed lambda-calculus.

  4. M. Zaionc, λ-Definability on free algebras.

Improve this answer
$\endgroup$

Your Answer

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

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