We provide a coinductive definition of strongly convergent reductions between infinite lambda terms. This approach avoids the notions of ordinals and metric convergence which have appeared in the earlier definitions of the concept. As an illustration, we prove the existence part of the infinitary standardization theorem. The proof is fully formalized in Coq using coinductive types.

The paper concludes with a characterization of infinite lambda terms which reduce to themselves in a single beta step.

The papers

extend the idea in this paper to reductions of length beyond omega.
The extension to reduction lengths beyond omega requires mixing of induction and coinduction.
Therefore the simpler setup presented in the current paper (*Infinitary Rewriting Coinductively*) is preferrable
whenever there is no need for reductions longer than omega.
This concerns for instance rewrite systems having the compression property, such as lambda calculus and left-linear term rewriting systems (with finite left-hand sides).