<p>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.</p>

<p>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).</p>

<p><hr>
<sub></p>

<ol>
<li><p>H. Schwichtenberg, <a href="https://epub.ub.uni-muenchen.de/4273/" rel="nofollow noreferrer">Definierbare Funktionen im λ-Kalkül mit Typen</a>.    </p></li>
<li><p>M. Zakrzewski, <a href="https://arxiv.org/abs/cs/0701022" rel="nofollow noreferrer">Definable Functions in the Simply Typed λ-Calculus</a>.</p></li>
<li><p>M. Zaionc, <a href="http://www.sciencedirect.com/science/article/pii/0304397587900776" rel="nofollow noreferrer">Word operation definable in the typed lambda-calculus.</a></p></li>
<li><p>M. Zaionc, <a href="http://www.sciencedirect.com/science/article/pii/016800729190019I" rel="nofollow noreferrer">λ-Definability on free algebras</a>.
</sub></p></li>
</ol>

CC BY-SA 3.0
2017-07-07T07:26:42.613Z
2017-07-07T09:52:28.540Z
2017-07-07T09:52:28.540Z
Martin Berger
<p>It's well known that the computation models <em>untyped lambda calculus</em> and <em>$\mu$-recursive function</em> 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 <em>simply typed lambda calculus</em> ($\lambda_{\rightarrow}$) and the <em>primitive recursive function</em> ($R_p$), are less powerful (i.e. neither of them is Turing complete.)</p>

<p>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.</p>

<p>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?</p>

CC BY-SA 3.0
2017-07-07T10:04:17.373Z
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](https://en.wikipedia.org/wiki/Curry%27s_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.
Thomas Klimpel
CC BY-SA 3.0
2017-07-07T14:42:55.313Z
@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: https://plato.stanford.edu/entries/type-theory-church/
cody
CC BY-SA 3.0
2017-07-07T15:14:30.950Z
@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.
Martin Berger
CC BY-SA 3.0
2017-07-07T18:03:01.243Z
@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](http://imps.mcmaster.ca/doc/seven-virtues.pdf). But SEP is also a great resource, see links given in [type theory as foundations](https://math.stackexchange.com/questions/431482/type-theory-as-foundations/828049#828049)
Thomas Klimpel
<reference-request><computability><typed-lambda-calculus>
Is simply typed lambda calculus equivalent to primitive recursive functions
Haochen Xie
# Is simply typed lambda calculus equivalent to primitive recursive functions

(Asked by: username_0 on 2017-07-07)

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?

**Tags:** reference-request, computability, typed-lambda-calculus

> **Comments:**
> **username_1**: 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](https://en.wikipedia.org/wiki/Curry%27s_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.  
> **username_2**: @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: https://plato.stanford.edu/entries/type-theory-church/  
> **username_3**: @username_2 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.  
> **username_1**: @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](http://imps.mcmaster.ca/doc/seven-virtues.pdf). But SEP is also a great resource, see links given in [type theory as foundations](https://math.stackexchange.com/questions/431482/type-theory-as-foundations/828049#828049)  

---

## 1 answers

### Answer by username_3 on 2017-07-07. Score: 7 | Accepted answer

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](https://epub.ub.uni-muenchen.de/4273/).
2. M. Zakrzewski, [Definable Functions in the Simply Typed λ-Calculus](https://arxiv.org/abs/cs/0701022).
3. M. Zaionc, [Word operation definable in the typed lambda-calculus.](http://www.sciencedirect.com/science/article/pii/0304397587900776)
4. M. Zaionc, [λ-Definability on free algebras](http://www.sciencedirect.com/science/article/pii/016800729190019I).


---

