# Does the simply typed lambda calculus have general iteration?

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$$

?

• No, you can't, because otherwise you could reproduce the construction you find on Wikipedia 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 Sep 14 '16 at 9:16
• 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 Sep 16 '16 at 14:56

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