Abstract
Proving non-termination is important for instance if one wants to decide termination for given TRSs. Altough the usual method is to find looping reduction sequences, there are non-looping infinite reduction sequences. We find some new interesting non-looping examples and propose new definitions of inner-looping sequence and normal sequence to classify them. We also show the undecidability of the existence of inner-looping sequence.
Journal
-
- Proceedings of 8th International Workshop on Termination
-
Proceedings of 8th International Workshop on Termination 17-21, 2006-08