<p>As I said in my comment, the answer in general is no.</p>

<p>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.</p>

<p>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:</p>

<p>Harry G. Mairson, A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2):387-394, 1992. (Available online <a href="http://www.cs.brandeis.edu/~mairson/Papers/statman.ps.gz">here</a>).</p>

<p>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</p>

<p>$t_M:\mathtt{nat}[\sigma]\rightarrow\mathtt{bool}$</p>

<p>(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. </p>

CC BY-SA 3.0
2014-03-20T01:27:04.287Z
It's probably also possible to use the encoding of [multi-variate polynomial functions in STLC](http://arxiv.org/abs/cs/0701022) and then appeal to [Matiyasevich's theorem](http://www.scholarpedia.org/article/Matiyasevich_theorem).
cody
CC BY-SA 3.0
2014-03-20T02:04:47.870Z
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?
MaiaVictor
CC BY-SA 3.0
2014-03-20T08:17:19.933Z
@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).
Damiano Mazza
CC BY-SA 3.0
2014-03-20T08:19:10.690Z
@cody: Thanks, I didn't know that paper. I guess you are right.
Damiano Mazza
CC BY-SA 3.0
2014-03-19T23:54:06.310Z
2014-03-20T00:06:05.933Z
2014-03-20T00:06:05.933Z
Damiano Mazza
<p>We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?</p>

CC BY-SA 3.0
2014-03-18T23:16:53.900Z
[Simply Typed Lambda Calculus/STLC](http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus) 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
CC BY-SA 3.0
2014-03-19T10:01:24.497Z
@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.
Damiano Mazza
CC BY-SA 3.0
2014-03-19T10:22:25.273Z
@DamianoMazza: ok, indeed I didn't vote to close it ... I'll delete my comment, leave yours and wait for OP's comment/edit.
Marzio De Biasi
CC BY-SA 3.0
2014-03-19T15:24:37.073Z
@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.
MaiaVictor
CC BY-SA 3.0
2014-03-19T20:23:28.973Z
@DamianoMazza sounds like an answer to me if filled in. Viclib you might start with the proof that it is undecidable to check for TM equivalence...
vzn
CC BY-SA 3.0
2014-03-20T00:03:20.497Z
@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](http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf) and Sørensen and Urzyczyn [Lecture Notes on Curry-Howard](ftp://ftp.cs.cmu.edu/user/rwh/www/home/courses/logic/www-old/handouts/curry-howard.pdf) are excellent starting places.
Damiano Mazza
<ds.algorithms><pl.programming-languages><type-theory><functional-programming>
Algorithm to determine function equality on the simply typed lambda calculus?
MaiaVictor
# Algorithm to determine function equality on the simply typed lambda calculus?

(Asked by: username_0 on 2014-03-18)

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

**Tags:** ds.algorithms, pl.programming-languages, type-theory, functional-programming

> **Comments:**
> **username_1**: [Simply Typed Lambda Calculus/STLC](http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus) 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...  
> **username_2**: @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.  
> **username_3**: @DamianoMazza: ok, indeed I didn't vote to close it ... I'll delete my comment, leave yours and wait for OP's comment/edit.  
> **username_0**: @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.  
> **username_1**: @DamianoMazza sounds like an answer to me if filled in. Viclib you might start with the proof that it is undecidable to check for TM equivalence...  
> **username_2**: @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](http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf) and Sørensen and Urzyczyn [Lecture Notes on Curry-Howard](ftp://ftp.cs.cmu.edu/user/rwh/www/home/courses/logic/www-old/handouts/curry-howard.pdf) are excellent starting places.  

---

## 1 answers

### Answer by username_2 on 2014-03-19. Score: 14 | Accepted answer

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](http://www.cs.brandeis.edu/~mairson/Papers/statman.ps.gz)).

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.

> **Comments:**
> **username_4**: It's probably also possible to use the encoding of [multi-variate polynomial functions in STLC](http://arxiv.org/abs/cs/0701022) and then appeal to [Matiyasevich's theorem](http://www.scholarpedia.org/article/Matiyasevich_theorem).  
> **username_0**: 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?  
> **username_2**: @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).  
> **username_2**: @username_4: Thanks, I didn't know that paper. I guess you are right.  

---

