|
 
|
[CGP10] Improved Matrix Interpretation
Conférence Internationale avec comité de lecture : SOFSEM'10, Int. Conf. on Current Trends in Theory and Practice of Computer Science, , January 2010, Vol. 5901, pp.12, Series LNCS, Spindleruv Ml{\'y}n, Czech Republic,
motcle:
Résumé:
We present a new technique to prove termination of Term Rewriting
Systems, with full automation. A crucial task in this context is to find suitable
well-founded orderings. A popular approach consists in interpreting terms into
a domain equipped with an adequate well-founded ordering. In addition to the
usual interpretations: natural numbers or polynomials over integer/rational numbers,
the recently introduced matrix based interpretations have proved to be very
efficient regarding termination of string rewriting and of term rewriting. In this
spirit we propose to interpret terms as polynomials over integer matrices. Designed
for term rewriting, our generalisation subsumes previous approaches allowing
for more orderings without increasing the search space. Thus it performs
better than the original version. Another advantage is that, interpreting terms to
actual polynomials of matrices, it opens the way to matrix non linear interpretations.
This result is implemented in the CiME3 rewriting toolkit.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| CGP10, | |||
| title | = | "{Improved Matrix Interpretation}", | |
| author | = | " P. Courtieu and G. Gbedo and O. Pons ", | |
| booktitle | = | "{SOFSEM'10, Int. Conf. on Current Trends in Theory and Practice of Computer Science, }", | |
| year | = | 2010, | |
| month | = | "January", | |
| series | = | "LNCS", | |
| volume | = | 5901, | |
| pages | = | "12", | |
| address | = | "Spindleruv Ml{\'y}n, Czech Republic", | |
| } | |||
