Given a $\lambda$-term $t\in \Lambda$ and an integer $k$, we say that $t$ behave likes the identity when applied to $k$ if $tk\to_\beta^*k$ (where the integer is represented as a church numeral). We will write $BI(t,k)$ for this property.

Given a term $t$, we define $a(t)$ as the smallest natural number that allows to distinguish $t$ from the identity. More formally, it is the element of $\mathbb N\cup \{+\infty\}$ such that for all $k< a(t), BI(t,k)$ and $\lnot BI(t,a(t))$. For example, $a(\lambda x. 0)=1$ and $a(\lambda x.x)=+\infty$. More generally terms $t$ such that $a(t)=+\infty$ are exactly those that behave like the identity for all integers: $a(t)=+\infty \iff \forall k, B(t,k)$.

Define the size $|t|$ of a term $t$ as the number of nodes in the corresponding abstract syntax tree.

Define $f(n):=\max\{a(t)\mid t\in \Lambda \land |t|\le n \land a(t)<+\infty\}$. It's the upper bound on the number of tests (assuming that we test by comparing $t0$ with $0$, then $t1$ with $1$ etc.) that it can take to distinguish a term of size at most $n$ from the identity. Given a term $t$, we have $a(t)\ge f(|t|)\iff a(t)=+\infty$, i.e. if it could not be distinguished from the identity by the first $f(|t|)$ tests, then it can not be distinguished from the identity by any of the tests.

Is $f$ bounded by a computable function? (And if yes, is it computable?)

Remark: The first thing I thought of is that it would imply decidability of the set of terms that behave like the identity $S_{BI}=\{t\mid a(t)=+\infty\}$, which can't be true by Rice's theorem. But the obvious argument doesn't work: given $t$, to know if $t\in S_{BI}$ even though I only need to test if $BI(t,k)$ for each $k\le f(|t|)$, I still can't do it because testing if $BI(t,k)$ (i.e. $tk\to_\beta^* k$) is undecidable (because $t$ could diverge).

  • 1
    $\begingroup$ This function is not computable, already for primitive recursive functions (which always terminate on a given input): roughly, you can write a p.r. function which is the identity if and only if a Turing machine does not halt. $\endgroup$ – cody Dec 12 '17 at 21:31

Your Answer

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

Browse other questions tagged or ask your own question.