Argument filterings and usable rules for simply typed dependency pairs

Takahito Aoto; Toshiyuki Yamada

doi:10.1007/978-3-642-04222-5_7

Argument filterings and usable rules for simply typed dependency pairs

Takahito Aoto, Toshiyuki Yamada

Systems & Software Division

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings
Pages	117-132
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-04222-5_7
Publication status	Published - 2009
Event	7th International Symposium on Frontiers of Combining Systems, FroCoS 2009 - Trento, Italy Duration: 2009 Sep 16 → 2009 Sep 18

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5749 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	7th International Symposium on Frontiers of Combining Systems, FroCoS 2009
Country/Territory	Italy
City	Trento
Period	09/9/16 → 09/9/18

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-642-04222-5_7

Cite this

Aoto, T., & Yamada, T. (2009). Argument filterings and usable rules for simply typed dependency pairs. In Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings (pp. 117-132). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5749 LNAI). https://doi.org/10.1007/978-3-642-04222-5_7

Argument filterings and usable rules for simply typed dependency pairs. / Aoto, Takahito; Yamada, Toshiyuki.

Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings. 2009. p. 117-132 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5749 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Aoto, T & Yamada, T 2009, Argument filterings and usable rules for simply typed dependency pairs. in Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5749 LNAI, pp. 117-132, 7th International Symposium on Frontiers of Combining Systems, FroCoS 2009, Trento, Italy, 09/9/16. https://doi.org/10.1007/978-3-642-04222-5_7

Aoto T, Yamada T. Argument filterings and usable rules for simply typed dependency pairs. In Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings. 2009. p. 117-132. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-04222-5_7

@inproceedings{3db585c91e9c49cdbe2f197002d74f15,

title = "Argument filterings and usable rules for simply typed dependency pairs",

abstract = "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.",

author = "Takahito Aoto and Toshiyuki Yamada",

year = "2009",

doi = "10.1007/978-3-642-04222-5_7",

language = "English",

isbn = "364204221X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "117--132",

booktitle = "Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings",

note = "7th International Symposium on Frontiers of Combining Systems, FroCoS 2009 ; Conference date: 16-09-2009 Through 18-09-2009",

}

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 -

Argument filterings and usable rules for simply typed dependency pairs

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this