CODEWITHSUNDEEP
lambdafunctional-programminglambda-calculus
luochen1990
luochen1990

Reputation: 3857

Is there two lambda terms which are extensional equal but have different normal forms?

Considering untyped lambda calculus. "normal form" simply means "beta-eta-nf". "different/same" lambda terms is compared mod alpha-conversion.

This question is just the same as "Is there a counterexample of the following proposition?"

∀ t1 : term, ∀ t2 : term, (∃ t1'= nf t1  ∧  ∃ t2' = nf t2) →  (t1' = t2' ↔  ex_eq  t1  t2)

Or, is there a proof of it?

Upvotes: 2

Views: 367

Answers (1)

Andrey Tyukin
Andrey Tyukin

Reputation: 44957

(In the following, read = as \equiv_{\beta\eta})

I think what you want is a direct application of the Böhm's Theorem. The theorem states:

Theorem (Böhm, 1968) Let f, g be two closed lambda terms in beta-eta normal form which are not equivalent up to alpha-conversion. Then there exist closed terms a_1, ..., a_n in beta-eta normal form such that for all x, y it holds:

  f a_1 ... a_n x y = x
  g a_1 ... a_n x y = y

A direct corollary is:

Corollary: If f and g are two closed terms in beta-eta normal form which are not equal up to alpha-conversion, then they are not extensionally equivalent.

Proof: For the sake of contradiction, assume that f g are in NF and different, but that they are extensionally equivalent. Choose a_1, ..., a_n as in Böhm's theorem. Since f, g are assumed to be extensionally equivalent, then f a_1 must be equal to g a_1. But this contradicts f a_1 ... a_n x y = x != y = g a_1 ... a_n x y for arbitrary unequal x and y. Therefore the assumption must be false, and f and g cannot be extensionally equivalent after all.

Now:

Corollary: Suppose f, g are two closed lambda terms with existing normal forms nf and ng respectively. It holds: nf is equivalent to ng up to alpha conversion if and only if f and g are extensionally equivalent.

Proof: One direction: if nf is equivalent to ng up to alpha conversion, then f and g are extensionally equivalent because of confluence (Church-Rosser theorem). Opposite direction: by contraposition of the previous corollary, if nf and ng are extensionally equivalent, then they must be equal up to alpha conversion.

So, the answer to your question is "No, there are no two terms that are extensionally equal but have different normal forms". That doesn't help you much though, because existence of normal forms is undecidable. So, for example, it does not all of a sudden make the equivalence of two arbitrary programs decidable.

Upvotes: 4

Related Questions