<p>The result you are looking for is Böhm's theorem. The equivalence described by "behaves the same way on all inputs" is the same as the equivalence given by normal forms, but only if you treat eta-equivalent normal forms (λx.Ix and I) as equivalent. You could disallow the former as a normal forms (eta-short) and then you'd have the syntactic condition you want by Böhm's theorem, if I'm not mistaken.</p>

CC BY-SA 3.0
2015-06-02T01:09:04.710Z
Interesting, so intensional and extensional equality are the same under beta-eta normalization on the untyped lambda calculus.
MaiaVictor
CC BY-SA 3.0
2015-06-02T07:35:37.720Z
Yeah, but that does not scale very well. For example if you try to add sums (because the beta-eta equalities on their negative encoding as lambda-terms doesn't give the expected eta-rule for sums) you get an inconsistent equality where everything is equal to anything.
gasche
CC BY-SA 3.0
2015-06-02T08:20:28.177Z
I agree with Rob's answer and gasche's comment. The fact that intensional and extensional equality coincide for untyped $\beta\eta$-normal forms should be taken with a grain of salt.  As further evidence, I would remind that the $\lambda$-theories $\beta$ and $\beta\eta$ have the *range property*, meaning that, if we consider a closed term $M$ as a function from $\Lambda/\beta$ or $\Lambda/\beta\eta$ (the set of equivalence classes of closed terms under $\beta$- or $\beta\eta$-equality) to itself, then its range is either a singleton or infinite.
Damiano Mazza
CC BY-SA 3.0
2015-06-02T08:28:53.100Z
So, for instance, there is no term $M$ such that, for every term $N$, $MN$ is either $\beta$-equivalent to $\mathsf{true}$ or to $\mathsf{false}$. So, yes, your different $\beta\eta$-normal forms are extensionally different, but this is because you have little control on what they do when applied to an arbitrary term. The story is different of course if you restrict to inputs of a certain form (e.g. Church numerals). My personal conclusion is that considering $\lambda$-terms as functions acting on $\lambda$-terms themselves is not very interesting from the point of view of programming.
Damiano Mazza
CC BY-SA 3.0
2015-06-02T00:34:06.310Z
2015-06-02T02:38:05.567Z
2015-06-02T02:38:05.567Z
Rob Simmons
<p>Let <code>f</code> and <code>g</code> be lambda terms in the normal form, such that <code>f</code> is intensionally different from <code>g</code> - that is, their string representation using bruijn indexes isn't the same. Is there any choice of <code>f</code> and <code>g</code> such that, for any <code>x</code> that is also a lambda term, <code>f x == g x</code>?</p>

CC BY-SA 3.0
2015-06-01T23:09:53.487Z
"$f$ is intensionally different from $g$" Doesn't that pretty much answer your question? Just take two terms that are *extensionally* the same, but intensionally different. E.g. $\lambda x.Ix$ and $I$.
svick
CC BY-SA 3.0
2015-06-02T01:08:07.753Z
`λx.Ix` is not on beta normal form.
MaiaVictor
<pl.programming-languages><lambda-calculus><functional-programming>
Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?
MaiaVictor
# Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?

(Asked by: username_0 on 2015-06-01)

Let `f` and `g` be lambda terms in the normal form, such that `f` is intensionally different from `g` - that is, their string representation using bruijn indexes isn't the same. Is there any choice of `f` and `g` such that, for any `x` that is also a lambda term, `f x == g x`?

**Tags:** pl.programming-languages, lambda-calculus, functional-programming

> **Comments:**
> **username_1**: "$f$ is intensionally different from $g$" Doesn't that pretty much answer your question? Just take two terms that are *extensionally* the same, but intensionally different. E.g. $\lambda x.Ix$ and $I$.  
> **username_0**: `λx.Ix` is not on beta normal form.  

---

## 1 answers

### Answer by username_2 on 2015-06-02. Score: 7

The result you are looking for is Böhm's theorem. The equivalence described by "behaves the same way on all inputs" is the same as the equivalence given by normal forms, but only if you treat eta-equivalent normal forms (λx.Ix and I) as equivalent. You could disallow the former as a normal forms (eta-short) and then you'd have the syntactic condition you want by Böhm's theorem, if I'm not mistaken.

> **Comments:**
> **username_0**: Interesting, so intensional and extensional equality are the same under beta-eta normalization on the untyped lambda calculus.  
> **username_3**: Yeah, but that does not scale very well. For example if you try to add sums (because the beta-eta equalities on their negative encoding as lambda-terms doesn't give the expected eta-rule for sums) you get an inconsistent equality where everything is equal to anything.  
> **username_4**: I agree with Rob's answer and username_3's comment. The fact that intensional and extensional equality coincide for untyped $\beta\eta$-normal forms should be taken with a grain of salt.  As further evidence, I would remind that the $\lambda$-theories $\beta$ and $\beta\eta$ have the *range property*, meaning that, if we consider a closed term $M$ as a function from $\Lambda/\beta$ or $\Lambda/\beta\eta$ (the set of equivalence classes of closed terms under $\beta$- or $\beta\eta$-equality) to itself, then its range is either a singleton or infinite.  
> **username_4**: So, for instance, there is no term $M$ such that, for every term $N$, $MN$ is either $\beta$-equivalent to $\mathsf{true}$ or to $\mathsf{false}$. So, yes, your different $\beta\eta$-normal forms are extensionally different, but this is because you have little control on what they do when applied to an arbitrary term. The story is different of course if you restrict to inputs of a certain form (e.g. Church numerals). My personal conclusion is that considering $\lambda$-terms as functions acting on $\lambda$-terms themselves is not very interesting from the point of view of programming.  

---

