We show the existence of an infinitary confluent and normalising
extension of the finite extensional lambda calculus with beta and eta.
Besides infinite beta reductions also infinite eta reductions are
possible in this extension, and terms without head normal form can be
reduced to bottom.
The normal form of this calculus are the so-called eta Böhm trees.
As corollaries we obtain a simple, syntax based construction of an
extensional Böhm model of the finite lambda calculus;
and a simple, syntax based proof that two lambda terms have the same
semantics in this model if and only if they have the same eta-Böhm
tree if and only if they are observationally equivalent wrt beta
normal forms.
The confluence proof reduces confluence of beta bottom and eta via
infinitary commutation and postponement arguments to confluence of beta
and bottom and confluence of eta.
We give counterexamples against confluence of similar extensions based
on the identification of the terms without weak head normal form and the
terms without top normal form (rootactive terms) respectively.
Joint work with Fer-Jan de Vries (University of Leicester)