Infinitary Combinatory Reduction Systems

J. Ketema, Jakob Grue Simonsen

    Research output: Contribution to journalArticleAcademicpeer-review

    14 Citations (Scopus)
    23 Downloads (Pure)

    Abstract

    We define infinitary Combinatory Reduction Systems (iCRSs), thus providing the first notion of infinitary higher-order rewriting. The systems defined are sufficiently general that ordinary infinitary term rewriting and infinitary $\lambda$-calculus are special cases. Furthermore, we generalise a number of known results from first-order infinitary rewriting and infinitary $\lambda$-calculus to iCRSs. In particular, for fully-extended, left-linear iCRSs we prove the well-known compression property, and for orthogonal iCRSs we prove that (1) if a set of redexes $\mathcal{U}$ has a complete development, then all complete developments of $\mathcal{U}$ end in the same term and that (2) any tiling diagram involving strongly convergent reductions $S$ and $T$ can be completed iff at least one of $S/T$ and $T/S$ is strongly convergent. We also prove an ancillary result of independent interest: A set of redexes in an orthogonal iCRS has a complete development iff the set has the so-called finite jumps property.
    Original languageEnglish
    Pages (from-to)893-926
    Number of pages34
    JournalInformation and computation
    Volume209
    Issue number6
    DOIs
    Publication statusPublished - Jun 2011

    Keywords

    • EWI-19795
    • METIS-277577
    • IR-76393
    • Combinatory Reduction Systems
    • Infinitary Rewriting
    • Higher-order term rewriting

    Fingerprint Dive into the research topics of 'Infinitary Combinatory Reduction Systems'. Together they form a unique fingerprint.

    Cite this