Research Directions

J.W. Klop and I. Bethke have continued work on a generalization of Berry's Sequentiality Theorem for lambda calculus. Using the setting of infinitary lambda calculus where Bohm trees are infinite normal forms, the technique of origin tracking was employed to obtain the sequentiality property for lambda calculus. The infinitary lambda calculus differentiates in three versions according to the way syntactic depth is counted: the three versions yield ordinary lambda calculus with Bohm trees, the lazy lambda calculus with Levy-longo trees, and a version introduced by Berarducci. For all three versions Berry's sequentiality theorem is uniformly proved by the same arguments. Also, a strengthening of Berry's theorem was obtained that can be used to prove more undefinability results.