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

CC BY-SA 3.0
2014-05-08T04:04:12.037Z
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
CC BY-SA 3.0
2014-05-08T04:20:26.803Z
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
CC BY-SA 3.0
2014-05-08T04:34:01.840Z
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
CC BY-SA 3.0
2014-05-08T09:00:00.853Z
See http://cstheory.stackexchange.com/questions/10608/programming-languages-with-canonical-functions?rq=1
Neel Krishnaswami
CC BY-SA 3.0
2014-05-10T15:28:32.233Z
Probably you want to ask something like "What are 'large' programming languages or systems where ... is decidable?"
usul
CC BY-SA 3.0
2014-05-11T04:40:15.343Z
@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
CC BY-SA 3.0
2014-05-11T18:29:46.933Z
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
<pl.programming-languages><computability><functional-programming>
Is there any system where function equality (extensionality) is decidable?
MaiaVictor
# Is there any system where function equality (extensionality) is decidable?

(Asked by: username_0 on 2014-05-08)

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

**Tags:** pl.programming-languages, computability, functional-programming

> **Comments:**
> **username_1**: 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?  
> **username_0**: 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?)  
> **username_1**: 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.  
> **username_2**: See http://cstheory.stackexchange.com/questions/10608/programming-languages-with-canonical-functions?rq=1  
> **username_3**: Probably you want to ask something like "What are 'large' programming languages or systems where ... is decidable?"  
> **username_0**: @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?  
> **username_2**: 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.  

---

## 0 answers

