Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Undecidability Results on Orie...

Email Gateway (May 03 2024 at 09:32):

From: Tobias Nipkow <nipkow@in.tum.de>
Undecidability Results on Orienting Single Rewrite Rules
René Thiemann, Fabian Mitterwallner, Aart Middeldorp

We formalize several undecidability results on termination for one-rule term
rewrite systems by means of simple reductions from Hilbert's 10th problem. To be
more precise, for a class C of reduction orders, we consider the question for a
given rewrite rule l -> r, whether there is some reduction order > in C such
that l > r. We include undecidability results for each of the following classes C:

• the class of linear polynomial interpretations over the natural numbers,

• the class of linear polynomial interpretations over the natural numbers in the
  weakly monotone setting,

• the class of Knuth–Bendix orders with subterm coefficients,

• the class of non-linear polynomial interpretations over the natural numbers, and
• the class of non-linear polynomial interpretations over the rational and real
  numbers.

https://www.isa-afp.org/entries/Orient_Rewrite_Rule_Undecidable.html

Enjoy!

smime.p7s

Last updated: May 19 2024 at 04:18 UTC