### Abstract

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 \(\ell \to r\), whether there is some reduction order \({\succ} \in C\) such that \(\ell \succ 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.

### License

BSD License

### Topics

- Logic/Rewriting

### Session Orient_Rewrite_Rule_Undecidable

- Preliminaries_on_Polynomials_1
- Preliminaries_on_Polynomials_2
- Polynomial_Interpretation
- Hilbert10_to_Inequality
- Linear_Poly_Termination_Undecidable
- KBO_Subterm_Coefficients_Undecidable
- Poly_Termination_Undecidable
- Delta_Poly_Termination_Undecidable

### Depends on

- Factorization of Polynomials with Algebraic Coefficients
- First-Order Terms
- A Formalization of Knuth–Bendix Orders
- Executable Multivariate Polynomials

### Auto-related entries

- Eudoxus Reals
- Constructing the Reals as Dedekind Cuts of Rationals

## Cite

×

Orient_Rewrite_Rule_Undecidable-AFP

    @article{Orient_Rewrite_Rule_Undecidable-AFP,
      author  = {René Thiemann and Fabian Mitterwallner and Aart Middeldorp},
      title   = {Undecidability Results on Orienting Single Rewrite Rules},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Orient_Rewrite_Rule_Undecidable.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest