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

  • $\begingroup$ 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? $\endgroup$ – Martin Berger May 8 '14 at 4:04
  • 1
    $\begingroup$ 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?) $\endgroup$ – MaiaVictor May 8 '14 at 4:20
  • $\begingroup$ 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. $\endgroup$ – Martin Berger May 8 '14 at 4:34
  • 4
    $\begingroup$ See cstheory.stackexchange.com/questions/10608/… $\endgroup$ – Neel Krishnaswami May 8 '14 at 9:00
  • $\begingroup$ Probably you want to ask something like "What are 'large' programming languages or systems where ... is decidable?" $\endgroup$ – usul May 10 '14 at 15:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.