Higher-Order Rewriting and Partial Evaluation

Olivier Danvy, Kristoffer H. Rose

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearch


    We demonstrate the usefulness of higher-order rewriting techniques for specializing programs, i.e., for partial evaluation. More precisely, we demonstrate how casting program specializers as combinatory reduction systems (CRSs) makes it possible to formalize the corresponding program transformations as meta-reductions, i.e., reductions in the internal “substitution calculus.” For partial-evaluation problems, this means that instead of having to prove on a case-by-case basis that one's “two-level functions” operate properly, one can concisely formalize them as a combinatory reduction system and obtain as a corollary that static reduction does not go wrong and yields a well-formed residual program.
    We have found that the CRS substitution calculus provides an adequate expressive power to formalize partial evaluation: it provides sufficient termination strength while avoiding the need for additional restrictions such as types that would complicate the description unnecessarily (for our purpose).
    In addition, partial evaluation provides a number of examples of higher-order rewriting where being higher order is a central (rather than an occasional or merely exotic) property. We illustrate this by demonstrating how standard but non-trivial partial-evaluation examples are handled with higher-order rewriting.
    Original languageEnglish
    Book seriesB R I C S Report Series
    Number of pages20
    Publication statusPublished - 1997


    Dive into the research topics of 'Higher-Order Rewriting and Partial Evaluation'. Together they form a unique fingerprint.

    Cite this