Separability of Infinite Lambda Terms

Abstract. Infinite lambda calculi extend finite lambda calculus with infinite terms and transfinite reduction. In this paper we extend some classical results of finite lambda calculus to infinite terms. The first result we extend to infinite terms is Böhm Theorem which states the separability of two finite βη-normal forms. The second result we extend to infinite terms is the equivalence of the prefix relation up to infinite eta expansions and the contextual preorder that observes head normal forms. Finally we prove that the theory given by equality of ∞η-Böhm trees is the largest theory induced by the confluent and normalising infinitary lambda calculi extending the calculus of Böhm trees.