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.
| Original language | Undefined |
|---|---|
| Article number | 10.2168/LMCS-6(1:7)2010 |
| Pages (from-to) | 1-35 |
| Number of pages | 35 |
| Journal | Logical methods in computer science |
| Volume | 6 |
| Issue number | 1:7 |
| DOIs | |
| Publication status | Published - 26 Feb 2010 |
Keywords
- normal forms
- Term rewriting
- infinite computation
- higher-order computation
- reduction strategies
- EWI-17092
- Lambda calculus
- CR-F.4.1
- CR-F.4.2
- CR-D.3.1
- METIS-270704
- IR-70343
- Combinatory Reduction Systems
- CR-F.3.2