<p>Assuming the given type and standard definition of Church numerals this indeed seems possible if we assume the existence of computable bijective mapping between instances of given types.</p>

<p>Note that the main issue is the type mismatch of $\mathsf{it}_\sigma$ and $\mathsf{N}$, otherwise $\mathsf{it}_\sigma$ could be equal to the identity function. One way of solving this issue is to have a way of uniquely converting between the types $\sigma$ and $0$. More specifically, if we have a way of encoding instances of type $\sigma$ into $0$ (which should encode natural numbers, thus have infinitely countable number of instances), we could encode the argument before applying it to $f$ and then decoding back the result. That is, if $e: \sigma \rightarrow 0$ and $d: 0 \rightarrow \sigma$ (which are inverses, thus define a bijection), we can define:</p>

<p>$$\mathsf{it}_\sigma \; n \; f \; x = n \; (\lambda y. e \; (f \; (d \; y)) \; x$$</p>

<p>Of course, this assumes the existence of $f$ and $g$, which might be easily realizable if, for examples, we had ways to enumerate instances of corresponding types. (E.g. for Church numerals, zero and increment should suffice.)</p>

<p>Note that bounded iteration is not as expressive as general iteration. In addition, note that Church numerals are definable by typeable terms in simply typed lambda calculus, together with operations like addition, but not predecessor (for which stronger mechanisms, like polymorphism in System F, are needed). (Short writeup about this can be found <a href="http://okmij.org/ftp/Computation/lambda-calc.html#predecessor" rel="nofollow">here</a>.)</p>

CC BY-SA 3.0
2016-10-09T07:53:54.160Z
2016-10-09T07:53:54.160Z
ivcha
<p>In more expressive calculi such as System F, the Church numerals, by virtue of their design, allow for iteration over an arbitrary type.  Can this effect be replicated in the simply typed case?</p>

<p>To be precise, consider the simply typed lambda calculus with a single base type $0$, giving the Church numerals the type $\mathsf{N} := (0 \rightarrow 0) \rightarrow 0 \rightarrow 0$.  For any type $\sigma$, can we find a closed term $\mathsf{it}_\sigma : \mathsf{N} \rightarrow (\sigma \rightarrow \sigma) \rightarrow \sigma \rightarrow \sigma$ with the property that</p>

<p>$$
\mathsf{it}_\sigma \underline{n} f x \rightsquigarrow f^nx
$$</p>

<p>?</p>

CC BY-SA 3.0
2016-09-14T09:16:28.787Z
No, you can't, because otherwise you could reproduce the construction you find on [Wikipedia](https://en.wikipedia.org/wiki/Ackermann_function) and implement the Ackermann function in the STLC with type $\mathsf N\rightarrow\mathsf N$, which is impossible due to a well-known result of Schwichtemberg (Functions definable in the simply-typed lambda calculus, *Arch. Math Logik* 17 (1976) 113-114) stating, in particular, that such a function necessarily has polynomial growth.  What you are doing corresponds to Gödel's system T.
Damiano Mazza
CC BY-SA 3.0
2016-09-16T14:56:35.730Z
Consider a set-based model of STLC with your $0$ type as well as another base $1$ type. Let $0$ be interpreted with a singleton set, and $1$ with a double-ton. Consequently, $\sf N$ is interpreted as a set containing exactly one function. Taking $\sigma=1$ and $f$ be the non-identify function we obtain that $f^m = f^n$ for every $n,m$, which is a contradiction e.g. when $n=0,m=1$.
chi
<lambda-calculus><typed-lambda-calculus>
Does the simply typed lambda calculus have general iteration?
user181407
# Does the simply typed lambda calculus have general iteration?

(Asked by: username_0 on 2016-09-14)

In more expressive calculi such as System F, the Church numerals, by virtue of their design, allow for iteration over an arbitrary type. Can this effect be replicated in the simply typed case?

To be precise, consider the simply typed lambda calculus with a single base type $0$, giving the Church numerals the type $\mathsf{N} := (0 \rightarrow 0) \rightarrow 0 \rightarrow 0$. For any type $\sigma$, can we find a closed term $\mathsf{it}\_\sigma : \mathsf{N} \rightarrow (\sigma \rightarrow \sigma) \rightarrow \sigma \rightarrow \sigma$ with the property that

$$
\mathsf{it}\_\sigma \underline{n} f x \rightsquigarrow f^nx
$$

?

**Tags:** lambda-calculus, typed-lambda-calculus

> **Comments:**
> **username_1**: No, you can't, because otherwise you could reproduce the construction you find on [Wikipedia](https://en.wikipedia.org/wiki/Ackermann_function) and implement the Ackermann function in the STLC with type $\mathsf N\rightarrow\mathsf N$, which is impossible due to a well-known result of Schwichtemberg (Functions definable in the simply-typed lambda calculus, *Arch. Math Logik* 17 (1976) 113-114) stating, in particular, that such a function necessarily has polynomial growth.  What you are doing corresponds to Gödel's system T.  
> **username_2**: Consider a set-based model of STLC with your $0$ type as well as another base $1$ type. Let $0$ be interpreted with a singleton set, and $1$ with a double-ton. Consequently, $\sf N$ is interpreted as a set containing exactly one function. Taking $\sigma=1$ and $f$ be the non-identify function we obtain that $f^m = f^n$ for every $n,m$, which is a contradiction e.g. when $n=0,m=1$.  

---

## 1 answers

### Answer by username_3 on 2016-10-09. Score: 1

Assuming the given type and standard definition of Church numerals this indeed seems possible if we assume the existence of computable bijective mapping between instances of given types.

Note that the main issue is the type mismatch of $\mathsf{it}\_\sigma$ and $\mathsf{N}$, otherwise $\mathsf{it}\_\sigma$ could be equal to the identity function. One way of solving this issue is to have a way of uniquely converting between the types $\sigma$ and $0$. More specifically, if we have a way of encoding instances of type $\sigma$ into $0$ (which should encode natural numbers, thus have infinitely countable number of instances), we could encode the argument before applying it to $f$ and then decoding back the result. That is, if $e: \sigma \rightarrow 0$ and $d: 0 \rightarrow \sigma$ (which are inverses, thus define a bijection), we can define:

$$\mathsf{it}\_\sigma \; n \; f \; x = n \; (\lambda y. e \; (f \; (d \; y)) \; x$$

Of course, this assumes the existence of $f$ and $g$, which might be easily realizable if, for examples, we had ways to enumerate instances of corresponding types. (E.g. for Church numerals, zero and increment should suffice.)

Note that bounded iteration is not as expressive as general iteration. In addition, note that Church numerals are definable by typeable terms in simply typed lambda calculus, together with operations like addition, but not predecessor (for which stronger mechanisms, like polymorphism in System F, are needed). (Short writeup about this can be found [here](http://okmij.org/ftp/Computation/lambda-calc.html#predecessor).)


---

