FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions

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: