Termination of rewrite relations on $λ$-terms based on Girard's notion of reducibility.
Theoretical Computer Science(2015)
摘要
In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of β-reduction in the polymorphic λ-calculus, to prove the termination of various kinds of rewrite relations on λ-terms, including rewriting modulo some equational theory and rewriting with matching modulo βη, by using the notion of computability closure. This provides a powerful termination criterion for various higher-order rewriting frameworks, including Klop's Combinatory Reductions Systems with simple types and Nipkow's Higher-order Rewrite Systems.
更多查看译文
关键词
Termination,Rewriting,λ-calculus,Types,Girard's reducibility,Rewriting modulo,Matching modulo βη,Patterns à la Miller
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要