arXiv subjects
Publications and source records attributed to Dieter Hofbauer.
Automating semantic labelling for termination proofs is a combinatorially hard problem since the number of algebras grows prohibitively large even for small domains. We report on experiments with our tools Matchbox and MnM, comparing various model finding strategies: exhaustive enumeration for bounded domain sizes within restricted search spaces, and semantic context-closure for fixed algebras.
This report contains the proceedings of the 19th International Workshop on Termination (WST 2023), which was held in Obergurgl during August 24--25 as part of Obergurgl Summer on Rewriting (OSR 2023).
We provide a critical assessment of the current set of benchmarks for relative SRS termination in the Termination Problems Database (TPDB): most of the benchmarks in Waldmann_19 and ICFP_10_relative are, in fact, strictly terminating (i. e., terminating when non-strict rules are considered strict), so these benchmarks should be removed, or relabelled. To fill this gap, we enumerate small relative string rewrite systems. At present, we have complete enumerations for a 2-letter alphabet up to size 11, and for a 3-letter alphabet up to size 8. For some selected benchmarks, old and new, we discuss how to prove termination, automated or not.
We over-approximate reachability sets in string rewriting by languages defined by admissible factors, called tiles. A sparse set of tiles contains only those that are reachable in derivations, and is constructed by completing an automaton. Using the partial algebra defined by a sparse tiling for semantic labelling, we obtain a transformational method for proving local termination. With a known result on forward closures, and a new characterisation of overlap closures, we obtain methods for proving termination and relative termination, respectively. We report on experiments showing the strength of these methods.