####
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.