Perpetual Reductions in Lambda Calculus


This paper surveys a part of the theory of beta-reductions in lambda calculus which might aptly be called perpetual reductions. The theory is concerned with perpetual reduction strategies, i.e., reduction strategies that compute infinite reduction paths from lambda terms (when possible), and with perpetual redexes, i.e., redexes whose contraction in lambda terms preserves the possibility (when present) of infinite reduction paths. The survey not only recasts classical theorems in a unified setting, but also offers new results, proofs, and techniques, as well as a number of applications to problems in lambda calculus and type theory.