https://arxiv.org/api/U7+U7sJFotF3Z+5vFHTgzPL+TRQ 2026-03-22T08:46:49Z 5866 0 15 http://arxiv.org/abs/2603.18858v1 2026-03-19T13:04:32Z

The Fibonacci infinite word ${\bf f} = (f_i)_{i \geq 0} = 01001010\cdots$ is one of the most celebrated objects in combinatorics on words. There is a simple $5$-state automaton that, given $i$ in lsd-first Zeckendorf representation, computes its $i$'th term $f_i$, and a $2$-state automaton for msd-first. In this paper we consider the state complexity of the automaton generating the shifted sequence $(f_{i+c})_{i \geq 0}$, and show that it is $O(\log c)$ for both msd-first and lsd-first input. This is close to the information-theoretic minimum for an aperiodic sequence. The techniques involve a mixture of state complexity techniques and Diophantine approximation.

2026-03-19T13:04:32Z Delaram Moradi Pierre Popoli Jeffrey Shallit Ingrid Vukusic http://arxiv.org/abs/2603.18820v1 2026-03-19T12:18:38Z

Motivated by the recent work of Deaconu, Mousavand and Paquette on the connection between infinite string bricks for certain gentle algebras and Sturmian words, we develop a decorated version of a deterministic automaton, called a multi-entry inverse automaton (MIA, for short) that accepts pointed words. We then associate an MIA $\mathsf M_{Λδ}$ over $\{0,1\}$ to a string algebra $Λ$, and show that strings over $Λ$ can be viewed as certain equivalence classes of the pointed words accepted by $\mathsf M_{Λδ}$. By defining (weak) brick words over this MIA, we show that a finite/infinite string module (resp. band module) is a brick if and only if every word in the associated equivalence class of pointed binary words is a brick word (resp. a weak brick word) over $\mathsf M_{Λδ}$. The result of Deaconu et al. follows as an immediate consequence.

2026-03-19T12:18:38Z 11 pages, 4 figures Amit Kuber Annoy Sengupta http://arxiv.org/abs/2603.17537v1 2026-03-18T09:44:34Z

The Lyndon array stores, at each position of a word, the length of the longest maximal Lyndon subword starting at that position, and plays an important role in combinatorics on words, for example in the construction of fundamental data structures such as the suffix array. In this paper, we introduce the Inverse Lyndon Array, the analogous structure for inverse Lyndon words, namely words that are lexicographically greater than all their proper suffixes. Unlike standard Lyndon words, inverse Lyndon words may have non-trivial borders, which introduces a genuine theoretical difficulty. We show that the inverse Lyndon array can be characterized in terms of the next greater suffix array together with a border-correction term, and prove that this correction coincides with a longest common extension (LCE) value. Building on this characterization, we adapt the nearest-suffix framework underlying Ellert's linear-time construction of the Lyndon array to the inverse setting, obtaining an O(n)-time algorithm for general ordered alphabets. Finally, we discuss implications for suffix comparison and report experiments on random, structured, and real datasets showing that the inverse construction exhibits the same practical linear-time behavior as the standard one.

2026-03-18T09:44:34Z 14 pages, 2 figures Pietro Negri Manuel Sica Rocco Zaccagnino Rosalba Zizza http://arxiv.org/abs/2510.21599v2 2026-03-18T00:51:50Z

Although Shapley additive explanations (SHAP) can be computed in polynomial time for simple models like decision trees, they unfortunately become NP-hard to compute for more expressive black-box models like neural networks - where generating explanations is often most critical. In this work, we analyze the problem of computing SHAP explanations for *Tensor Networks (TNs)*, a broader and more expressive class of models than those for which current exact SHAP algorithms are known to hold, and which is widely used for neural network abstraction and compression. First, we introduce a general framework for computing provably exact SHAP explanations for general TNs with arbitrary structures. Interestingly, we show that, when TNs are restricted to a *Tensor Train (TT)* structure, SHAP computation can be performed in *poly-logarithmic* time using *parallel* computation. Thanks to the expressiveness power of TTs, this complexity result can be generalized to many other popular ML models such as decision trees, tree ensembles, linear models, and linear RNNs, therefore tightening previously reported complexity results for these families of models. Finally, by leveraging reductions of binarized neural networks to Tensor Network representations, we demonstrate that SHAP computation can become *efficiently tractable* when the network's *width* is fixed, while it remains computationally hard even with constant *depth*. This highlights an important insight: for this class of models, width - rather than depth - emerges as the primary computational bottleneck in SHAP computation.

2025-10-24T16:02:51Z To appear in NeurIPS 2025 Reda Marzouk Shahaf Bassan Guy Katz http://arxiv.org/abs/2603.17188v1 2026-03-17T22:34:40Z

We introduce the notion of density of a rational language with respect to a sequence of probability measures. We prove that if $(μ_n)$ is a sequence of Bernoulli measures converging to a positive Bernoulli measure $\overlineμ$, the sequential density is the ordinary density with respect to $\overlineμ$. We also prove that if $(μ_n)$ is a sequence of invariant probability measures converging in the strong sense to an invariant probability measure $\overlineμ$, then the sequential density of every rational language exists for this sequence.

2026-03-17T22:34:40Z Alexi Block Gorman Dominique Perrin http://arxiv.org/abs/2505.15605v2 2026-03-17T14:07:58Z

For a terminal alphabet $Σ$ and an attribute alphabet $Γ$, a $(Σ, Γ)$-extractor is a function that maps every string over $Σ$ to a table with a column per attribute and with sets of positions of $w$ as cell entries. This rather general information extraction framework extends the well-known document spanner framework, which has intensively been investigated in the database theory community over the last decade. Moreover, our framework is based on formal language theory in a particularly clean and simple way. In addition to this conceptual contribution, we investigate closure properties, different representation formalisms and the complexity of natural decision problems for extractors.

2025-05-21T14:59:34Z Markus L. Schmid http://arxiv.org/abs/2509.22819v2 2026-03-16T22:30:22Z

Large Language Models (LLMs) demonstrate impressive mathematical reasoning abilities, but their solutions frequently contain errors that cannot be automatically checked. Formal theorem proving systems such as Lean 4 offer automated verification with complete accuracy, motivating recent efforts to build specialized prover LLMs that generate verifiable proofs in formal languages. However, a significant gap remains: current prover LLMs solve substantially fewer problems than general-purpose LLMs operating in natural language. We introduce Hilbert, an agentic framework that bridges this gap by combining the complementary strengths of informal reasoning and formal verification. Our system orchestrates four components: an informal LLM that excels at mathematical reasoning, a specialized prover LLM optimized for Lean 4 tactics, a formal verifier, and a semantic theorem retriever. Given a problem that the prover is unable to solve, Hilbert employs recursive decomposition to split the problem into subgoals that it solves with the prover or reasoner LLM. It leverages verifier feedback to refine incorrect proofs as necessary. Experimental results demonstrate that Hilbert substantially outperforms existing approaches on key benchmarks, achieving 99.2\% on miniF2F, 6.6\% points above the best publicly available method. Hilbert achieves the \textbf{strongest known result} from a publicly available model on PutnamBench. It solves 462/660 problems (70.0\%), outperforming proprietary approaches like SeedProver (50.4\%) and achieving a 422\% improvement over the best publicly available baseline. Thus, Hilbert effectively narrows the gap between informal reasoning and formal proof generation. Code is available at https://github.com/Rose-STL-Lab/ml-hilbert.

2025-09-26T18:24:23Z Sumanth Varambally Thomas Voice Yanchao Sun Zhifeng Chen Rose Yu Ke Ye http://arxiv.org/abs/2603.15177v1 2026-03-16T12:11:52Z

We study the notion of irreducibility of semigroup morphisms. Given an alphabet $Σ$, a morphism $\varphi:Σ^+\rightarrowΣ^+$ is irreducible if any factorisation $\varphi=ψ_2\circψ_1$ can only be satisfied if $ψ_1$ or $ψ_2$ is a trivial morphism. Otherwise, $\varphi$ is reducible. We introduce the notion of irreducibility, characterise this property and study a number of fundamental questions on the concepts under consideration.

2026-03-16T12:11:52Z Paul C. Bell Eva Foster Daniel Reidenbach http://arxiv.org/abs/2403.03067v5 2026-03-16T09:41:14Z

We study the problem of enumerating the answers to a query formulated in monadic second order logic (MSO) over an unranked forest F that is compressed by a straight-line program (SLP) D. Our main result states that this can be done after O(|D|) preprocessing and with output-linear delay (in data complexity). This is a substantial improvement over the previously known algorithms for MSO-evaluation over trees, since the compressed size |D| might be much smaller than (or even logarithmic in) the actual data size |F|, and there are linear time SLP-compressors that yield very good compressions on practical inputs. In particular, this also constitutes a meta-theorem in the field of algorithmics on SLP-compressed inputs: all enumeration problems on trees or strings that can be formulated in MSO-logic can be solved with linear preprocessing and output-linear delay, even if the inputs are compressed by SLPs. We also show that our approach can support vertex relabelling updates in time that is logarithmic in the uncompressed data. Our result extends previous work on the enumeration of MSO-queries over uncompressed trees and on the enumeration of document spanners over compressed text documents.

2024-03-05T15:56:48Z 64 pages. This is the TheoretiCS journal version TheoretiCS, Volume 5 (February 26, 2026) theoretics:16426 Markus Lohrey Markus L. Schmid 10.46298/theoretics.26.6 http://arxiv.org/abs/2405.01953v2 2026-03-15T18:40:44Z

We define generalised equations of Z-Mahler type, based on the Zeckendorf numeration system. We show that if a sequence over a commutative ring is Z-regular, then it is the sequence of coefficients of a series which is a solution of a Z-Mahler equation. Conversely, if the Z-Mahler equation is isolating, then its solutions define Z-regular sequences. This is a generalisation of results of Becker and Dumas. We provide an example to show that there exist non-isolating Z-Mahler equations whose solutions do not define Z-regular sequences. Our proof yields a new construction of weighted automata that generate classical q-regular sequences.

2024-05-03T09:28:06Z 36 pages, 6 figures Olivier Carton Reem Yassawi http://arxiv.org/abs/2507.09387v3 2026-03-13T21:14:20Z

Word ${\mathbf G}$ is the fixed point of the morphism $γ=[01,2,02]$. In 2019, Shallit and Shur showed that ${\mathbf G}$ has factor complexity $2n+1$. They also showed that ${\mathbf G}$ has critical exponent $μ=2+\frac{1}{λ^2-1}= 2.4808726\cdots$, where $λ=1.7548777$ is the real zero of $x^3-2x+x-1=0$. They conjectured that this was the least possible critical exponent among words with factor complexity $2n+1$. We confirm their conjecture. The proof, using an intricate case analysis, is by computer. The relevant program generates a `human readable' proof.

2025-07-12T20:07:24Z Substantial revision of original submission James D. Currie http://arxiv.org/abs/2603.15675v1 2026-03-13T18:11:39Z

Interfaces play a central role in determining compatible component compositions by prescribing permissible interactions between a service provider (server) and its consumers (clients). The high degree of concurrency in asynchronous communicating systems increases the risk of unintentionally introducing deadlocks and livelocks. The weak termination property serves as a basic sanity check to avoid such problems. It assures that in each reachable state, the system has the option to eventually terminate. This paper generalizes existing results that, by construction, guarantee weakly terminating interface compositions. Our generalizations make the theory applicable more broadly in practice. Starting with an interface specification of a server satisfying certain properties, we show how a class of clients modeling different usage contexts can be derived using a partial mirroring relation. Furthermore, we discuss an embedding of our results in an open-source tool to guide modelers in designing weakly terminating interfaces.

2026-03-13T18:11:39Z Debjyoti Bera Tim A. C. Willemse http://arxiv.org/abs/2603.13058v1 2026-03-13T15:07:21Z

We present an algorithm that, given an index $t$, produces the $t$-th (lexicographically ordered) answer of an MSO query over a string. The algorithm requires linear-time preprocessing, and builds a data structure that answers each of these calls in logarithmic time. We then show how to extend this algorithm for a string that is compressed by a straight-line program (SLP), also with linear-time preprocessing in the (compressed encoding of the) string, and maintaining direct access in logtime of the original string. Lastly, we extend the algorithm by allowing complex edits on the SLP after the direct-access data structure has been processsed, which are translated into the data structure in logtime. We do this by adapting a document editing framework introduced by Schmid and Schweikardt (PODS 2022). This work improves on a recent result of dynamic direct access of MSO queries over strings (Bourhis et. al., ICDT 2025) by a log-factor on the access procedure, and by extending the results to SLPs.

2026-03-13T15:07:21Z Martín Muñoz http://arxiv.org/abs/2509.22598v2 2026-03-13T12:00:14Z

We prove that all standard subregular language classes are linearly separable when represented by their deciding predicates. This establishes finite observability and guarantees learnability with simple linear models. Synthetic experiments confirm perfect separability under noise-free conditions, while real-data experiments on English morphology show that learned features align with well-known linguistic constraints. These results demonstrate that the subregular hierarchy provides a rigorous and interpretable foundation for modeling natural language structure. Our code used in real-data experiments is available at https://github.com/UTokyo-HayashiLab/subregular.

2025-09-26T17:17:15Z 11 pages, 5 figures Katsuhiko Hayashi Hidetaka Kamigaito http://arxiv.org/abs/2311.15675v9 2026-03-13T10:57:51Z

We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is $Σ_1^2$-complete, and finite-state satisfiability and model-checking are equivalent to truth in second-order arithmetic. Finally, we also introduce closed-world semantics for second-order HyperLTL, where set quantification ranges only over subsets of the model, while set quantification in standard semantics ranges over arbitrary sets of traces. Here, satisfiability for the least fixed point fragment becomes $Σ_1^1$-complete, but all other results are unaffected.

2023-11-27T10:03:40Z Logical Methods in Computer Science, Volume 22, Issue 1 (March 16, 2026) lmcs:16039 Hadar Frenkel Gaëtan Regaud Martin Zimmermann 10.46298/lmcs-22(1:26)2026