# Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?

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?

• "$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 Jun 1 '15 at 23:09
• λx.Ix is not on beta normal form. – MaiaVictor Jun 2 '15 at 1:08

• 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 Jun 2 '15 at 8:20
• 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 Jun 2 '15 at 8:28