Highlights in infinitary rewriting and lambda calculus

We present some highlights from the emerging theory of infinitary rewriting, both for first-order term rewriting systems and λ-calculus.In the first section we introduce the framework of infinitary rewriting for first-order rewrite systems, so without bound variables. We present a recent observation concerning the continuity of infinitary rewriting.In the second section we present an excursion to the infinitary λ-calculus. After the main definitions, we mention a recent observation about infinite looping λ-terms, that is, terms that reduce in one step to themselves. Next we describe the fundamental trichotomy in the semantics of λ-calculus: Böhm trees, Lévy–Longo trees, and Berarducci trees. We conclude with a short description of a new refinement of Böhm tree semantics, called clocked semantics.