Argument Filterings And Usable Rules For Simply Typed Dependency Pairs
FroCoS'09: Proceedings of the 7th international conference on Frontiers of combining systems(2009)
摘要
Simply typed term rewriting (Yamada, 2001) is a framework of higher-order term rewriting without bound variables based on Lisp-like syntax. The dependency pair method for the framework has been obtained by extending the first-order dependency pair method and sub-term criterion in (Aoto &, Yamada, 2005). In this paper, we incorporate termination criteria using reduction pairs and related refinements into the simply typed dependency pair framework using recursive path orderings for S-expression rewriting systems (Toyama, 2008). In particular, we incorporate the usable rules criterion with respect to argument filterings, which is a key ingredient to prove the termination in a modular way. The proposed technique has been implemented in a termination prover and an experimental result is reported.
更多查看译文
关键词
dependency pair framework,dependency pair method,first-order dependency pair method,reduction pair,termination criterion,termination prover,higher-order term,subterm criterion,usable rules criterion,Lisplike syntax,argument filterings
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络