Generalized Rewriting in Type Theory.
David Basin · 1994
While type theories such as Nuprl are expressive logics for theorem proving, they present difficulties for designers of term rewriting systems. The two most serious difficulties are: 1) They do not provide a global equality. Instead users rewrite over arbitrary user-defined relations. 2) Each rewrite step must be proved valid. In general, these proofs cannot be recursively generated. We have overcome these difficulties and designed a package for the Nuprl system that works well in practice. Our solution is an extensible set of functions for directing and validating relational inferences. The heart of our package is a set of operators that use a user-supplied lemma database to create new rewrites from old ones. These routines place no restrictions on relations; a rewrite's success depends on the strength of the database. Overall, the package allows rewrites to be pieced together in numerous ways, providing the user with a tool to construct sophisticated rewrite strategies.