3
$\begingroup$

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

?

Improve this question
$\endgroup$
2
  • 5
    $\begingroup$ 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. $\endgroup$ – Damiano Mazza Sep 14 '16 at 9:16
  • 2
    $\begingroup$ 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$. $\endgroup$ – chi Sep 16 '16 at 14:56
2
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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