3

Is there any programming language or system where function equality (extensionality) is decidable?

MaiaVictor
  • 3,137
  • 11
  • 33
  • If equality $\cong$ was decidable in a Turing complete language, then for any Turing machine $M$, there would be an encoding $enc(M)$. So to decide if $M$ halts we could simply compute $enc(M) \cong enc(M_{halt})$, where $M_{halt}$ is a machine that always halts. Does that sound like a feasible algorithm to you? – Martin Berger May 08 '14 at 04:04
  • 1
    No, I don't mean a Turing Complete language. Maybe I should be more clear. My question is pretty much: "is function equality decidable in any language (that has functions) at all?" For example, the Simply Typed Lambda Calculus comes to mind. (Unfortunately it is not decidable there, despite the system itself not being turing complete - but what about other non-turing-complete systems with functions?) – MaiaVictor May 08 '14 at 04:20
  • If you remove enough power from a language, extensional equality will eventually be decidable, e.g. consider the following small 'language' $\mathcal{L} = {\lambda x.x}$, which is a sub-calculus of the $\lambda$-calculus. – Martin Berger May 08 '14 at 04:34
  • 4
    See http://cstheory.stackexchange.com/questions/10608/programming-languages-with-canonical-functions?rq=1 – Neel Krishnaswami May 08 '14 at 09:00
  • Probably you want to ask something like "What are 'large' programming languages or systems where ... is decidable?" – usul May 10 '14 at 15:28
  • @NeelKrishnaswami I'm not sure this answers my question, the STLC doesn't have this property (AFAIK). It happens that every term has a normal form, but it doesn't mean that two equal functions have the same normal form. Correct? – MaiaVictor May 11 '14 at 04:40
  • The STLC has a unique normal forms property. If you add sum types, it has normal forms which are unique up to a decidable equivalence. Once you add natural numbers, the problem of equivalence is undecidable. – Neel Krishnaswami May 11 '14 at 18:29

0 Answers0