A restricted form of higher-order rewriting applied to an HDL semantics
RTA '95: Proceedings of the 6th International Conference on Rewriting Techniques and Applications(1995)
摘要
An algorithm for a restricted form of higher-order matching is described. The intended usage is for rewrite rules that use function-valued 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.
更多查看译文
关键词
HDL Semantics,Higher-Order Rewriting Applied,Restricted Form
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络