pith. sign in

arxiv: 2605.00947 · v1 · submitted 2026-05-01 · 💻 cs.CC · cs.LO

Termination of Real Linear Loops

Eike Neumann , Margret Tembo This is my paper

Pith reviewed 2026-05-09 15:19 UTC · model grok-4.3

classification 💻 cs.CC cs.LO
keywords terminationlinear loopsaffine loopsreal computationbit modeldecidabilityrobustnessLebesgue measure
0
0 comments X

The pith

Termination of linear and affine loops over the reals admits sound partial decision procedures on all robust instances.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper studies the problem of deciding whether linear and affine loops with real-valued updates always terminate. It shows that sound partial algorithms exist which correctly answer every instance whose termination status remains unchanged under all sufficiently small perturbations of the input coefficients. The set of non-robust instances, where the answer can flip under tiny changes, has Lebesgue measure zero in the parameter space. This places the problems as close to decidable as the continuous nature of the reals permits within the bit-model of real computation. A reader cares because exact decidability is typically impossible for real-valued problems, yet this result guarantees reliable resolution for almost all inputs.

Core claim

We show that both the universal termination problem for linear loops and for affine loops over the reals are as close to decidable as one can expect them to be: there exist sound partial algorithms that halt on all problem instances whose answer is robust under all sufficiently small perturbations. We further show that in each case the set of non-robust problem instances has Lebesgue measure zero.

What carries the argument

Robustness under small perturbations within the bit-model of real computation, which identifies the stable instances on which partial algorithms succeed.

If this is right

  • Sound partial algorithms exist that decide universal termination for linear loops on every robust input.
  • Sound partial algorithms exist that decide universal termination for affine loops on every robust input.
  • The non-robust inputs form a Lebesgue measure zero set for both the linear and the affine case.
  • The partial algorithms are guaranteed to halt precisely when the termination answer is invariant under all sufficiently small real perturbations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same near-decidability pattern may extend to other reachability or invariance questions for linear dynamical systems over the reals.
  • Numerical perturbation checks could be used in practice to certify that a given loop instance is robust before applying the partial algorithm.
  • Randomly sampled loop coefficients will almost surely produce decidable instances because the bad set has measure zero.

Load-bearing premise

The bit-model of real computation together with the chosen definition of robustness under perturbations correctly captures when an answer is stable enough to be decided.

What would settle it

An explicit linear loop whose termination status changes under some arbitrarily small perturbation of the coefficients, yet lies inside a positive Lebesgue measure set of such sensitive instances.

read the original abstract

We study the problem of deciding universal termination of linear and affine loops over the reals in the bit-model of real computation. We show that both problems are as close to decidable as one can expect them to be: there exist sound partial algorithms that halt on all problem instances whose answer is robust under all sufficiently small perturbations. We further show that in each case the set of non-robust problem instances has Lebesgue measure zero.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 3 minor

Summary. The manuscript studies the decidability of universal termination for linear and affine loops over the reals in the bit-model of real computation. It establishes that both problems admit sound partial algorithms that correctly decide all instances whose termination status is robust under sufficiently small perturbations, and proves that the set of non-robust instances has Lebesgue measure zero.

Significance. If the central claims hold, the work supplies a theoretically grounded form of near-decidability for a problem that is expected to be undecidable in full generality. The robustness-plus-measure-zero approach is a standard and useful technique in real algebraic decision procedures; when the partial algorithms are effective in the bit model, the result offers a practical handle on termination analysis for real-valued programs and clarifies the boundary between decidable and undecidable fragments.

major comments (2)
  1. [Main technical development of the partial algorithms] The soundness argument for the partial algorithms (stated in the abstract and presumably proved in the main technical section) must explicitly verify that the decision procedure remains effective when inputs are given as bit-model representations; without this, it is unclear whether the algorithms actually halt on all robust instances as claimed.
  2. [Proof of the measure-zero statement] The proof that the non-robust set has Lebesgue measure zero relies on the set being semi-algebraic or definable in an o-minimal structure; this reduction must be carried out explicitly for both the linear and affine cases, as it is the sole justification for the measure-zero claim.
minor comments (3)
  1. [Abstract and §1] The informal phrase 'as close to decidable as one can expect' in the abstract and introduction should be replaced by a precise statement of the robustness predicate and the class of instances on which the algorithms are guaranteed to succeed.
  2. [Preliminaries] Notation for loops, perturbations, and the bit-model encoding should be introduced once and used consistently; several passages reuse symbols without redefinition.
  3. [Related work] A short comparison table or paragraph relating the new partial algorithms to existing decision procedures for linear loops (e.g., those based on real algebraic geometry) would help readers assess the advance.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We address each major comment below, indicating where we will strengthen the manuscript to make the arguments fully explicit.

read point-by-point responses

  1. Referee: The soundness argument for the partial algorithms (stated in the abstract and presumably proved in the main technical section) must explicitly verify that the decision procedure remains effective when inputs are given as bit-model representations; without this, it is unclear whether the algorithms actually halt on all robust instances as claimed.

    Authors: We thank the referee for highlighting this point. The soundness proof in Theorem 3.2 already reduces termination on robust instances to the effective decision of polynomial sign conditions via quantifier elimination over the reals, which is known to be computable in the bit model. Nevertheless, to remove any ambiguity, we will add an explicit paragraph immediately after the statement of Theorem 3.2 that spells out the bit-model representation of the input matrix and vector, the arithmetic operations used to compute the robustness witness, and why the procedure is guaranteed to terminate on every robust instance. This change will be incorporated in the revised version. revision: yes

  2. Referee: The proof that the non-robust set has Lebesgue measure zero relies on the set being semi-algebraic or definable in an o-minimal structure; this reduction must be carried out explicitly for both the linear and affine cases, as it is the sole justification for the measure-zero claim.

    Authors: We agree that the measure-zero argument should be stated more explicitly. In the linear case, Lemma 4.2 already exhibits the non-robust set as a finite union of proper algebraic varieties (hence a semi-algebraic set of positive codimension). For the affine case, the current proof sketches a homogenization that reduces the problem to the linear setting, but does not spell out the resulting semi-algebraic formula. We will expand Section 5 to include the full, explicit semi-algebraic definition of the non-robust affine instances and verify that it likewise has Lebesgue measure zero. This revision will appear in the next version of the manuscript. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper's central claims concern the existence of sound partial algorithms for termination of real linear and affine loops that halt precisely on robust instances under bit-model perturbations, together with a Lebesgue measure-zero result for the non-robust set. These statements are derived from the definability of the termination predicate in an o-minimal structure and standard measure-theoretic properties of semi-algebraic sets; no step reduces by construction to a fitted parameter, self-referential definition, or load-bearing self-citation whose content is merely renamed. The derivation chain is self-contained against external real-algebraic decision procedures and does not invoke any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard mathematical foundations of real numbers, Lebesgue measure, and the bit-model of computation; no free parameters, ad-hoc axioms, or invented entities are introduced in the abstract.

axioms (1)
  • standard math Standard axioms of the real numbers and Lebesgue measure theory
    Invoked to define perturbations and to assert that non-robust instances have measure zero.

pith-pipeline@v0.9.0 · 5350 in / 1082 out tokens · 44199 ms · 2026-05-09T15:19:42.639533+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages

  1. [1]

    Computability , YEAR =

    Arno Pauly , title =. Computability , YEAR =

    work page

  2. [2]

    and Gerhold, Stefan , title =

    Bell, Jason P. and Gerhold, Stefan , title =. Israel Journal of Mathematics , volume =. 2007 , doi =

    work page 2007

  3. [3]

    1969 , booktitle =

    The fundamental theorem of algebra in recursive analysis , author =. 1969 , booktitle =

    work page 1969

  4. [4]

    2006 , publisher =

    Basu, Saugata and Pollack, Richard and Roy, Marie-Fran. 2006 , publisher =

    work page 2006

  5. [5]

    Mathematical Structures in Computer Science , volume =

    Collins, Pieter , title =. Mathematical Structures in Computer Science , volume =

    work page

  6. [6]

    Pour-El and J

    Marian B. Pour-El and J. Ian Richards , title =

    work page

  7. [7]

    CAV'04 , year =

    Ashish Tiwari , title =. CAV'04 , year =

    work page

  8. [8]

    1991 , PAGES =

    Ko, Ker-I , TITLE =. 1991 , PAGES =

    work page 1991

  9. [9]

    Klaus Weihrauch , title =

    work page

  10. [10]

    Theoretical Computer Science , volume =

    Brattka, Vasco and Presser, Gero , title =. Theoretical Computer Science , volume =

    work page

  11. [11]

    2002 , school =

    Schr\"oder, Matthias , title =. 2002 , school =

    work page 2002

  12. [12]

    Theoretical Computer Science , volume =

    Schr\"oder, Matthias , title =. Theoretical Computer Science , volume =. 2002 , pages =

    work page 2002

  13. [13]

    2021 , MONTH = Aug, KEYWORDS =

    Eike Neumann , URL =. 2021 , MONTH = Aug, KEYWORDS =. doi:10.46298/lmcs-17(3:16)2021 , JOURNAL =

    work page doi:10.46298/lmcs-17(3:16)2021 2021

  14. [14]

    Theoretical Computer Science , volume =

    Ziegler, Martin and Brattka, Vasco , title =. Theoretical Computer Science , volume =. 2004 , pages =

    work page 2004

  15. [15]

    Logical Methods in Computer Science , volume =

    Sewon Park and Franz Brau. Logical Methods in Computer Science , volume =. 2024 , doi =

    work page 2024