Sequentiality

Berry's Sequentiality Theorem for lambda calculus was generalised by J.W. Klop and I. Bethke. Using the setting of infinitary lambda calculus where Bohm trees are infinite normal forms, the technique of origin tracking (also used by Bertot at PLDI'91 and Abadi, Lévy and Lampson at ICFP'96) 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.