Infinitary Rewriting Coinductively
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.
infinitary rewriting
coinduction
lambda calculus
standardization
16-27
Regular Paper
Jörg
Endrullis
Jörg Endrullis
Andrew
Polonsky
Andrew Polonsky
10.4230/LIPIcs.TYPES.2011.16
Creative Commons Attribution-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nd/3.0/legalcode