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

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

• Simply Typed Lambda Calculus/STLC wikipedia. since its not Turing complete, is there any other basic model of computation that its equivalent to? it also might be useful to study the halting detection algorithm, which acc to wikipedia is decidable for STLC...
– vzn
Mar 18, 2014 at 23:16
• @Marzio: Actually, I think the problem here is with the way the question is formulated, which is quite imprecise. Once properly formulated, this is a research-level question. A better formulation would be: we know that beta-equality of simply typed lambda-terms is decidable. Given $M,N:\sigma\rightarrow\tau$, is it decidable whether for all $X:\sigma$, $MX\simeq_\beta NX$? The answer is negative in general (so no algorithm such as the one sought by Viclib exists). Although perhaps expected, this is not obvious a priori and is a consequence of a couple of papers from the 90s. Mar 19, 2014 at 10:01
• @DamianoMazza: ok, indeed I didn't vote to close it ... I'll delete my comment, leave yours and wait for OP's comment/edit. Mar 19, 2014 at 10:22
• @DamianoMazza and Marzio, I don't know enough to make such a formal question. I wish I did, though, but this isn't something I learn on my school. In fact, even googling for "beta-equality", which is something I actually tried before asking the question, gives me so few results that it is almost like this term didn't even exist. So I don't even have an idea where you learn and read about all that. Would you guys kindly point me to the right place to start self studying the topic? Question updated. Mar 19, 2014 at 15:24
• @Viclib: beta-equivalence is a technical notion, I avoided mentioning it in my answer. Roughly, two terms are beta-equivalent when they yield the same result. So saying $MX\simeq_\beta NX$ for all $X$ means that $M$ and $N$ compute the same function. Concerning pointers for learning about the (typed or untyped) lambda-calculus, I think Peter Selinger's notes and Sørensen and Urzyczyn Lecture Notes on Curry-Howard are excellent starting places. Mar 20, 2014 at 0:03

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.

• It's probably also possible to use the encoding of multi-variate polynomial functions in STLC and then appeal to Matiyasevich's theorem.
– cody
Mar 20, 2014 at 1:27
• So the STLC is not turing complete, but is powerful enough to encode the transition function of a Turing machine!? So a Turing Machine could be defined as a tape plus a STLC program operating on it? Mar 20, 2014 at 2:04
• @Viclib: Think about it: simulating one step of an arbitrary Turing machine does not require much computational power. Basically, you only need finite data types (with if-then-else), lists (with the basic operations: cons, tail, etc.) and ordered pairs. (In fact, the Extended Church-Turing Thesis claims that such low complexity is common to every reasonable machine model). What the STLC is missing is the ability to run TM transitions "ad libitum", independently of the input: it can only iterate them a number of times equal to a tower of exponentials in the input size (see Mairson's paper). Mar 20, 2014 at 8:17
• @cody: Thanks, I didn't know that paper. I guess you are right. Mar 20, 2014 at 8:19