Presentation | 2006-06-22 Transformation of Equational Rewriting Systems for Removing some Equations Koichi MIURA, Naoki NISHIDA, Masahiko SAKAI, Toshiki SAKABE, Keiichiro KUSAKARI, |
---|---|
PDF Download Page | PDF download Page Link |
Abstract(in Japanese) | (See Japanese page) |
Abstract(in English) | In equational rewriting, which is rewriting modulo equations, the set of all direct successors from a given term is in generally undecidable because the word problem for equations is undecidable. In this paper, we give an equivalent transformation of equational rewriting systems. The procedure converts some of the given equations to corresponding rewrite rules, and simultaneously adds rewrite rules whose left-hand sides are equivalent modulo equations with the left-hand sides of some of the given rules. Succeeded to reduce the number of equation so that the word problem for the remaining equation is decidable, the set of all direct successors of a given term becomes decidable. The procedure requires that input equations are commutative to the other equations. We also give a successful example of the procedure that is for ambient calculus. |
Keyword(in Japanese) | (See Japanese page) |
Keyword(in English) | term rewriting system / rewriting modulo equations / ambient calculus / structural congruence |
Paper # | SS2006-14 |
Date of Issue |
Conference Information | |
Committee | SS |
---|---|
Conference Date | 2006/6/15(1days) |
Place (in Japanese) | (See Japanese page) |
Place (in English) | |
Topics (in Japanese) | (See Japanese page) |
Topics (in English) | |
Chair | |
Vice Chair | |
Secretary | |
Assistant |
Paper Information | |
Registration To | Software Science (SS) |
---|---|
Language | JPN |
Title (in Japanese) | (See Japanese page) |
Sub Title (in Japanese) | (See Japanese page) |
Title (in English) | Transformation of Equational Rewriting Systems for Removing some Equations |
Sub Title (in English) | |
Keyword(1) | term rewriting system |
Keyword(2) | rewriting modulo equations |
Keyword(3) | ambient calculus |
Keyword(4) | structural congruence |
1st Author's Name | Koichi MIURA |
1st Author's Affiliation | Graduate School of Information Science, Nagoya University() |
2nd Author's Name | Naoki NISHIDA |
2nd Author's Affiliation | Graduate School of Information Science, Nagoya University |
3rd Author's Name | Masahiko SAKAI |
3rd Author's Affiliation | Graduate School of Information Science, Nagoya University |
4th Author's Name | Toshiki SAKABE |
4th Author's Affiliation | Graduate School of Information Science, Nagoya University |
5th Author's Name | Keiichiro KUSAKARI |
5th Author's Affiliation | Graduate School of Information Science, Nagoya University |
Date | 2006-06-22 |
Paper # | SS2006-14 |
Volume (vol) | vol.106 |
Number (no) | 120 |
Page | pp.pp.- |
#Pages | 6 |
Date of Issue |