Author: Dieter Hofbauer
Paper Information
Title: | Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions |
Authors: | Dieter Hofbauer |
Proceedings: | WST WST2018proceedings |
Editor: | Salvador Lucas |
Keywords: | string rewriting, termination, derivational complexity |
Abstract: | ABSTRACT. Weight functions are among the simplest methods for proving termination of string rewrite systems, and of rather limited applicability. In this working paper, we propose a generalized approach. As a first step, syllable decomposition yields a transformed, typically infinite rewrite system over an infinite alphabet, as the title indicates. Combined with generalized weight functions, termination proofs become feasible also for systems that are not necessarily simply terminating. The method is limited to systems with linear derivational complexity, however, and this working paper is restricted to original alphabets of size two. The proof principle is almost self-explanatory, and if successful, produces simple proofs with short proof certificates, often even shorter than the problem instance. A prototype implementation was used to produce nontrivial examples. |
Pages: | 1 |
Talk: | Jul 18 14:30 (Session 127Q: Program termination and orderings (II)) |
Paper: |