Infinitary Combinatory Reduction Systems: Normalising Reduction Strategies
Jeroen Ketema, Jakob Grue Simonsen
TL;DR
This paper investigates reduction strategies in infinitary Combinatory Reduction Systems, proving their normalising properties under various fairness conditions, and extends results from first-order infinitary rewriting to the infinitary lambda calculus.
Contribution
It introduces the first normalising strategies for infinitary lambda calculus and generalises existing results to orthogonal, fully-extended iCRSs.
Findings
All fair, outermost-fair, and needed-fair strategies are normalising for orthogonal, fully-extended iCRSs.
Provides the first examples of normalising strategies for infinitary lambda calculus.
Extends normalising strategy results from first-order to infinitary rewriting.
Abstract
We study normalising reduction strategies for infinitary Combinatory Reduction Systems (iCRSs). We prove that all fair, outermost-fair, and needed-fair strategies are normalising for orthogonal, fully-extended iCRSs. These facts properly generalise a number of results on normalising strategies in first-order infinitary rewriting and provide the first examples of normalising strategies for infinitary lambda calculus.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.