# Is there any system where function equality (extensionality) is decidable?

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

• 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 8 '14 at 4:04
• 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 8 '14 at 4: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 8 '14 at 4:34
• – Neel Krishnaswami May 8 '14 at 9: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