3
$\begingroup$

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?

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

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Interesting, so intensional and extensional equality are the same under beta-eta normalization on the untyped lambda calculus. $\endgroup$ – MaiaVictor Jun 2 '15 at 1:09
  • 3
    $\begingroup$ 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. $\endgroup$ – gasche Jun 2 '15 at 7:35
  • 2
    $\begingroup$ 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. $\endgroup$ – Damiano Mazza Jun 2 '15 at 8:20
  • 2
    $\begingroup$ 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. $\endgroup$ – Damiano Mazza Jun 2 '15 at 8:28

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.