Modular Construction of Fixed Point Combinators and Clocked Böhm Trees

Fixed point combinators (and their generalization: looping combinators) are classic notions belonging to the heart of λ-calculus and logic. We start with an exploration of the structure of fixed point combinators (fpc´s), vastly generalizing the wellknown fact that if Yis an fpc, Y(SI) is again an fpc, generating the Böhm sequence of fpc´s. Using the infinitary λ-calculus we devise infinitely many other generation schemes for fpc´s. In this way we find schemes and building blocks to construct new fpc´s in a modular way. Having created a plethora of new fixed point combinators, the task is to prove that they are indeed new. That is, we have to prove their β-inconvertibility. Known techniques via Böhm Trees do not apply, because all fpc´s have the same Böhm Tree (BT). Therefore, we employ ´clocked BT´s´, with annotations that convey information of the tempo in which the data in the BT are produced. BT´s are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for λ-terms. The corresponding equality is strictly intermediate between =_β and =_BT, the equality in the classical models of λ-calculus. An analogous approach pertains to Lévy-Longo and Berarducci trees. Finally, we increase the discrimination power by a precision of the clock notion that we call ´atomic clock´.