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

*A Coinductive Framework for Infinitary Rewriting and Equational Reasoning*(RTA 2015)*Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic*(LMCS 2018)

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