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, 2017 at 21:31


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.