2026-07-21T21:12:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3897 2024-03-06T10:34:36Z ddc:004 open_access

Infinitary Rewriting Coinductively Endrullis, Jörg Polonsky, Andrew infinitary rewriting coinduction lambda calculus standardization 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jörg Endrullis and Andrew Polonsky 2013 Is Part Of LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2011.16 urn:nbn:de:0030-drops-38971 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.16 eng https://creativecommons.org/licenses/by-nd/3.0/legalcode