Infinitary Combinatory Reduction Systems: Normalising Reduction Strategies

J. Ketema, Jakob Grue Simonsen

    Research output: Contribution to journalArticleAcademicpeer-review

    9 Citations (Scopus)
    115 Downloads (Pure)


    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 languageUndefined
    Article number10.2168/LMCS-6(1:7)2010
    Pages (from-to)1-35
    Number of pages35
    JournalLogical methods in computer science
    Issue number1:7
    Publication statusPublished - 26 Feb 2010


    • 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

    Cite this