TY - GEN
T1 - Argument filterings and usable rules for simply typed dependency pairs
AU - Aoto, Takahito
AU - Yamada, Toshiyuki
PY - 2009
Y1 - 2009
N2 - 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 subterm 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.
AB - 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 subterm 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.
UR - http://www.scopus.com/inward/record.url?scp=76649118085&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=76649118085&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-04222-5_7
DO - 10.1007/978-3-642-04222-5_7
M3 - Conference contribution
AN - SCOPUS:76649118085
SN - 364204221X
SN - 9783642042218
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 117
EP - 132
BT - Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings
T2 - 7th International Symposium on Frontiers of Combining Systems, FroCoS 2009
Y2 - 16 September 2009 through 18 September 2009
ER -