Algorithm to determine function equality on the simply typed lambda calculus?

Question

We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?

Answer 1

As I said in my comment, the answer in general is no.

The important point to understand (I say this for Viclib, who seems to be learning about these things) is that having a programming language/set of machines in which all programs/computations terminate by no means implies that function equality (i.e., whether two programs/machines compute the same function) is decidable. An easy example: take the set of polynomially-clocked Turing machines. By definition, all such machines terminate on all inputs. Now, given any Turing machine whatsoever $M$, there is a Turing machine $M_0$ that, given in input the string $x$, simulates $|x|$ steps of the computation of $M$ on a fixed input (say, the empty string) and accepts if $M$ terminates in at most $|x|$ steps, or rejects otherwise. If $N$ is a Turing machine that always immediately rejects, $M_0$ and $N$ are both (obviously) polynomially-clocked, and yet if we could decide whether $M_0$ and $N$ compute the same function (or, in this case, decide the same language), we would be able to decide whether $M$ (which, remember, is an arbitrary Turing machine) terminates on the empty string.

In the case of the simply typed $\lambda$-calculus (STLC), a similar argument works, except that gauging the expressive power of the STLC is not as trivial as in the above case. When I wrote my comment, I had in mind a couple of papers by Hillebrand, Kanellakis and Mairson from the early 90s, which show that, by using more complex types than the usual type of Church integers, one may encode in the STLC sufficiently complex computations for the above argument to work. Actually, I see now that the needed material is already in Mairson's simplified proof of Statman's theorem:

Harry G. Mairson, A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2):387-394, 1992. (Available online here).

In that paper, Mairson shows that, given any Turing machine $M$, there is a simple type $\sigma$ and a $\lambda$-term $\delta_M:\sigma\rightarrow\sigma$ encoding the transition function of $M$. (This is not obvious a priori, if one has in mind the extremely poor expressive power of the STLC on Church integers. Indeed, Mairson's encoding is not immediate). From this, it is not hard to construct a term

$t_M:\mathtt{nat}[\sigma]\rightarrow\mathtt{bool}$

(where $\mathtt{nat}[\sigma]$ is the instantiation on $\sigma$ of the type of Church integers) such that $t_M\,\underline{n}$ reduces to $\underline{1}$ if $M$ terminates in at most $n$ steps when fed the empty string, or reduces to $\underline{0}$ otherwise. As above, if we were able to decide that the function represented by $t_M$ is the constant $\underline{0}$ function, we would have decided the termination of $M$ on the empty string.