Arctic termination
Abstract. We extend the matrix method for proving termination of string rewriting: we use matrices of the arctic semi-ring. (Its domain are the natural numbers, extended by minus infinity, arctic multiplication is standard addition, and arctic addition is the standard maximumoperation.) This method...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Published: |
2007
|
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.132.640 http://dfa.imn.htwk-leipzig.de/matchbox/methods/tropical.pdf |
| Summary: | Abstract. We extend the matrix method for proving termination of string rewriting: we use matrices of the arctic semi-ring. (Its domain are the natural numbers, extended by minus infinity, arctic multiplication is standard addition, and arctic addition is the standard maximumoperation.) This method will be used by Matchbox in the 2007 Termination Competition. It produces some short termination proofs for hard or previously unsolved problems. We prove that the arctic termination method contains the quasi-periodic method as a special case. 1 Arctic Matrix Interpretations We adapt the matrix method for proving termination of string rewriting [7] to matrices over a different semi-ring. (This present section is extracted from a paper on the general theory of matrix interpretations over ordered semi-rings that has been submitted elsewhere [8]. Section 2 is new.) The arctic semi-ring A, also known as the (max,plus) algebra [5], has as |
|---|