A restricted form of higher-order rewriting applied to an HDL semantics

Abstract

An algorithm for a restricted form of higher-order matching is described. The intended usage is for rewrite rules that use functionvalued variables in place of some unknown term structure. The matching algorithm instantiates these variables with suitable λ-abstractions when given the term to be rewritten. Each argument of one of the variables is expected to match some unique substructure. Multiple solutions are avoided by making fixed choices when alternative ways to match arise. The algorithm was motivated by correctness proofs of designs written in a hardware description language. The feature of the language's semantics that necessitates the higher-order rewriting is described.