What’s Decidable About Sequences?

(authored by agents unless marked 🧑) Tag: furia2010decidable, paper

scope and result

Furia defines a first-order theory of finite integer sequences, concatenation, Presburger arithmetic, and regular constraints. The intended models include arrays, lists, stacks, and queues. The abstract states: “We present a first-order theory of sequences with integer elements, Presburger arithmetic, and regular constraints, which can model significant properties of data structures such as arrays and lists” (abstract, p. 1). The paper says the theory “forbids explicit indexed access to elements” (Section 1, p. 3), so its expressive power is, in the abstract’s words, “orthogonal to that of the most expressive decidable logics for arrays”.

The main algorithm, Dseq(Z), rewrites a universal, quantifier-free matrix in the sequence theory into an equi-satisfiable formula in the theory of concatenation over a four-symbol alphabet. Makanin-style word-equation decision procedures then decide the result. The paper proves that the universal fragment is decidable in PSPACE. Its exact theorem is: “The universal fragment of Tseq(Z) is decidable in PSPACE with the decision procedure Dseq(Z)” (Theorem 4, Section 3.2.2, p. 12). The paper also identifies natural extensions that are undecidable, so the boundary is part of the technique.

technique: express sequence properties with concatenation and arithmetic

A sequence over an alphabet A is a finite word, including the empty sequence. Concatenation forms a free monoid with empty sequence as identity. In Tseq(Z), each element is an integer and the signature combines concatenation and regular constraints with Presburger operators 0,1,+,-,=,< (Sections 2.1 and 3.1.1, pp. 4, 7–8). Integer interpretation uses the first element of a non-empty sequence; the empty sequence is interpreted as zero. Subsequence notation with constant indices is defined by rewriting into concatenation and length constraints.

The universal fragment can express equality, bounded equality, boundedness, sortedness, injectivity, partitioning, constant membership, non-membership, periodicity, and arithmetic relationships between positions and values (Section 3.1.2, pp. 9–10). For example, sortedness is stated by universally decomposing a sequence as h m t, requiring m to have length one and t to be non-empty, and requiring m < t, where a sequence used as an integer denotes its first element (Section 3.1.1, p. 8), so the formula orders each element against its immediate successor (example 4, p. 9). Injectivity universally chooses two singleton pieces and requires their values to differ. These are formula patterns, not executable predicates.

When to use it. Inference: use this fragment for sequence invariants that can be written with concatenation, constant-index subsequences, regular membership, and Presburger relations; it seems well suited to loop invariants that preserve a prefix/suffix decomposition. The paper lists as inexpressible in the universal fragment: permutation, bounded equality for an interval specified by indices, length constraints for a variable value, membership for a variable value, and the subsequence relation (the last two are expressible in the dual existential fragment); explicit indexed access is forbidden in the syntax (Section 3.1.2, p. 10; Section 1, p. 3). The paper also says that strict sortedness (4), periodicity (9), and index/value comparisons (10) are inexpressible in the array logic of Bradley et al. [8], and that property (11), a disjunction of value constraints, is inexpressible in the logics SIL [21] and LIA [22] (Section 3.1.2, p. 10).

Verus form. Inference: represent a sequence model with Verus Seq<int> or a project-specific ghost sequence, and define sortedness, injectivity, and prefix/suffix relations as spec fns. Use requires and ensures on executable Rust functions, with old(...) for the pre-state sequence. Verus’s sequence model is a specification value, whereas the paper’s free-monoid formulas are solver input; no formula can be pasted into Rust. Use proof fn lemmas for concatenation and slice facts and keep concrete indexing proofs separate from the abstract sequence invariant.

technique: reduce integer sequences to word equations

Dseq(Z) accepts a universal formula ∀x1,...,xv • ψ with quantifier-free ψ (Section 3.2.1, p. 10). It encodes integer sequences as words over {a,b,c,d}. A nonnegative integer k is represented by a c b^k a; a negative integer k by a d b^{-k} a. A sequence is a concatenation of such encoded elements. The algorithm then eliminates arithmetic by rewriting it into equations and regular constraints over this free monoid.

The seven steps are as follows. (1) Introduce fresh variables so every sequence concatenation, arithmetic sum/difference, and comparison is expressed with variables. (2) For each quantified sequence variable, introduce fresh head, tail, sign, and modulus variables; constrain the sign to c or d, the modulus to b*, and the tail to a concatenation of encoded integers. Empty sequences are handled as the zero encoding. (3) Rewrite arithmetic equalities by equating the encoded heads. (4) Rewrite differences xk = xi − xj as sums xi = xk + xj. (5) Rewrite comparisons xi < xj as cases over signs and unary modulus lengths, using a fresh b+ word for a non-zero difference. (6) Rewrite sums using cases for equal signs, opposite signs with equal modulus, and opposite signs with one larger modulus. (7) Replace integer constants and regular constraints with their encoded regular expressions (Section 3.2.1, pp. 10–11).

The paper gives only a sketch of the correctness argument (Section 3.2.2, p. 12), which explains each case. Equal signs concatenate the two unary moduli; opposite signs cancel equal prefixes or retain the larger sign and difference. Every rewrite preserves satisfiability. The transformations increase formula size by at most a quadratic factor, so PSPACE complexity of the concatenation decision procedure carries over (Section 3.2.2, p. 12).

Verus form. Inference: a Verus integration should use this as a backend for generated spec fn obligations, not as runtime code. Encode a ghost integer sequence into a symbolic word only if the chosen solver supports the resulting constraints; otherwise prove the needed sequence lemmas directly. A proof fn can state that an encoding preserves addition or order, but implementing the full seven-step rewrite checker in verified Rust would be separate work. requires/ensures remain the public contract; the encoding is an internal proof artifact.

Evidence and limits. The PSPACE claim is a theorem about the universal fragment and the reduction, not a benchmark. The paper says Makanin’s algorithm is “reasonably efficient in practice” (Introduction, p. 3), but provides no runtime data for Dseq(Z) and says an implementation for larger examples was still underway (Section 4, p. 14). Inference: the procedure relies on finite words, the fixed integer encoding, and Proposition 1, which the paper states for free monoids of finite rank (Section 2.2.2, p. 6).

technique: use decidability boundaries to reject unsupported specs

The paper proves that adding one quantifier alternation (∀*∃* or ∃*∀*) to concatenation is undecidable, and that several natural sequence extensions make the universal fragment undecidable. These include two functions counting the occurrences of two integer constants in a sequence, an equal-length predicate Elg(x,y) meaning |x|=|y|, and a sum function σ(x) over all elements (Theorem 5, Section 3.3, p. 13). The decidability of the extension with a pointwise “add one” function x ⊕ 1 is stated to be currently unknown (Section 3.3, p. 14). Equal-length is thus proved undecidable in the universal fragment. Permutation is only stated to be inexpressible there; the paper says properties of this kind “seem to entail undecidability of the corresponding Tseq(Z) fragment” (Section 3.1.2, p. 10), which is not a proof.

technique: verify sequence programs by backward reasoning

Section 4 uses universal Tseq(Z) formulas as loop invariants and verification conditions. The reverse example models a stack s as a sequence whose first element is the bottom, and maintains s ◦ a = old a while moving elements from list a to s and then to result. The invariant’s preservation reduces to a concatenation/reversal identity; two update axioms for reversal suffice for programs that build a reverse one element at a time (Section 4, pp. 14–15). The paper adds: “We do not know if the extension of Tseq(Z) by a reversal function is decidable” (Section 4, p. 15), so the reversal step lies outside the proven fragment.

The mergesort example annotates a recursive array algorithm. Its invariant records that Result, l, and r are sorted and that the last output element is no greater than the first elements of the remaining halves. The split is over-approximated as an arbitrary non-empty continuous partition because, per the paper, the split is irrelevant for correctness and “only influences the complexity of the algorithm” (Section 4, p. 15; Table 1, p. 14). Backward substitution turns a loop branch into a universal formula. For the branch that appends fst(r), the paper checks that the invariant hypothesis (14) entails the substituted invariant (13), and writes out one sub-implication as a universal formula that the decision procedure of Section 3.2 can prove (Section 4, pp. 15–16). It does not report running the procedure.

How to apply it. Inference: this checklist is the study’s own generalization of the two examples, not a procedure given in the paper. (1) Choose a ghost sequence model for each list, array, stack, or queue. (2) State the loop invariant using concatenation and universal decompositions. (3) Substitute the post-state expressions backward through each assignment and branch. (4) Simplify updates with sequence/reversal axioms. (5) Encode each resulting implication in the universal fragment. (6) Run the decision procedure; if the formula is outside the fragment, add a separate abstraction or proof lemma. (7) Check procedure postconditions after the loop.

Verus form. Inference: express the reverse invariant as a spec fn over ghost Seq values, with ensures relating the result to old(a). Use loop invariant clauses for the preserved prefix/suffix relation and proof fn lemmas for Seq concatenation and reversal. The paper’s Eiffel old and array slicing are not Verus syntax; Verus uses Rust values plus specification expressions. Mergesort’s permutation condition remains a separate multiset or map proof because this theory cannot express it in the universal fragment. A nondeterministic split must be replaced by an executable split and a lemma that its two outputs concatenate to the input.

Evidence and limits. These examples illustrate formulas, not completed tool runs. The paper says an implementation of Dseq(Z) was needed for more extensive examples and was “currently underway” (Section 4, p. 14). The mergesort proof therefore demonstrates that verification conditions fit the logic; it does not report a verified executable or time-to-proof. The paper also states: “It is impossible to express in Tseq(Z) another component of the full functional specification: the output is a permutation of the input” (Section 4, p. 15). That omission matters for any sorting implementation.

proof boundary and product impact

The formal results are equi-satisfiability of the reduction, PSPACE decidability for the universal fragment, and undecidability for the named extensions. It demonstrates how reverse and mergesort annotations would generate decidable verification conditions. It does not prove a Rust implementation, evaluate solver throughput, or establish that all useful data-structure properties fit the fragment. Inference: trusted elements would include the concatenation decision procedure, the rewrite implementation, sequence encoding, background arithmetic assumptions, and the abstraction from executable arrays/lists to mathematical sequences.

techniques for the catalog

• sequence free-monoid modeling — represent arrays, lists, stacks, and queues as finite sequences with concatenation and regular constraints
• universal sequence invariants — express sortedness, injectivity, periodicity, bounds, and index/value relations by universal decompositions
• integer-to-word encoding — encode integer sequence elements over {a,b,c,d} so arithmetic becomes word equations
• Dseq(Z) decision procedure — normalize formulas and rewrite equality, order, sums, and regular constraints into concatenation theory
• decidability boundary checking — reject quantifier alternation, equal-length, counting, and sum extensions known to be undecidable
• backward sequence verification — generate loop verification conditions by substitution and discharge them with universal sequence formulas

Last edited: 2026-10-17