文章基本信息

标题：A New Look at Generalized Rewriting in Type Theory
本地全文：下载
作者：Matthieu Sozeau
期刊名称：Journal of Formalized Reasoning
印刷版ISSN：1972-5787
出版年度：2009
卷号：2
期号：1
页码：41-62
DOI：10.6092/issn.1972-5787/1574
语种：English
出版社：Alma Mater Studiorum - University of Bologna
摘要：Rewriting is an essential tool for computer-based reasoning, both automated and assisted. This is because rewriting is a general notion that permits modeling a wide range of problems and provides a means to effectively solve them. In a proof assistant, rewriting can be used to replace terms in arbitrary contexts, generalizing the usual equational reasoning to reasoning modulo arbitrary relations. This can be done provided the necessary proofs that functions appearing in goals are congruent with respect to specific relations. We present a new implementation of generalized rewriting in the Coq proof assistant, making essential use of the expressive power of dependent types and the recently implemented type class mechanism. The new rewrite tactic improves on and generalizes previous versions by natively supporting higher-order functions, polymorphism and subrelations. The type class system inspired by Haskell provides a perfect interface between the user and the tactic, making it easily extensible.