SearcharxivSearch

arXiv subjects

Aliaume Lopez

Publications and source records attributed to Aliaume Lopez.

16 recordsLinked to original sources

Regularity as seen by Alice and Bob

The goal of this paper is to propose a unifying model for Nerode-style characterizations of regularity across functions with different output domains. Building on Hauser's work in communication complexity, we generalize the setting by relaxing the computability assumptions and allowing non-Boolean output domains. We consider functions of type $\Sigma^* \to \domain$, where $\Sigma$ is a finite alphabet and $\domain$ is an arbitrary domain. For several domains, we show that the model coincides with known models of computation. We further conjecture that an analogous correspondence holds for other domains that currently lack a Nerode-style characterization of regularity, and we provide ample supporting evidence. In the model, an input string $w$ is split as $w = w_1 w_2$ and distributed between two cooperating parties, Alice and Bob, who exchange a constant number of messages to compute the value of the function. Each message is either an element of the output domain or a signal drawn from a finite set of signals, and the parties must produce the correct output for every admissible split $w = w_1 w_2$. We further extend the framework to infinite alphabets in the setting of nominal sets, and investigate its expressiveness on languages of words with atoms.

cs.FL

Well-quasi-ordered classes of bounded clique-width

We study classes of graphs with bounded clique-width that are well-quasi-ordered by the induced subgraph relation, in the presence of labels on the vertices. We prove that, given a finite presentation of a class of graphs, one can decide whether the class is labelled-well-quasi-ordered. This answers positively to two conjectures of Pouzet in the restricted case of bounded clique-width classes. Namely, we prove that being labelled-well-quasi-ordered by a set of size 2 or by a well-quasi-ordered infinite set are equivalent conditions, and that in such cases, one can freely assume that the graphs are equipped with a total ordering on their vertices. Finally, we provide a structural characterization of those classes as those that are of bounded clique-width and do not existentially transduce the class of all finite paths.

math.CO

Computability of Equivariant Gröbner bases

Let $\mathbb{K}$ be a field, $\mathcal{X}$ be an infinite set (of indeterminates), and $\mathcal{G}$ be a group acting on $\mathcal{X}$. An ideal in the polynomial ring $\mathbb{K}[\mathcal{X}]$ is called equivariant if it is invariant under the action of $\mathcal{G}$. We show Gröbner bases for equivariant ideals are computable are hence the equivariant ideal membership is decidable when $\mathcal{G}$ and $\mathcal{X}$ satisfies the Hilbert's basis property, that is, when every equivariant ideal in $\mathbb{K}[\mathcal{X}]$ is finitely generated. Moreover, we give a sufficient condition for the undecidability of the equivariant ideal membership problem. This condition is satisfied by the most common examples not satisfying the Hilbert's basis property.

cs.LO

Polyregular Model Checking

We introduce a high-level language with Python-like syntax for string-to-string, polyregular, first-order definable transductions. This language features function calls, boolean variables, and nested for-loops. We devise and implement a complete decision procedure for the verification of such programs against a first-order specification. The decision procedure reduces the verification problem to the decidable first-order theory of finite words (extensively studied in automata theory), which we discharge using either complete tools specific to this theory (MONA), or to general-purpose SMT solvers (Z3, CVC5).

cs.FL

Well-Quasi-Orderings on Word Languages

The set of finite words over a well-quasi-ordered set is itself well-quasi-ordered. This seminal result by Higman is a cornerstone of the theory of well-quasi-orderings and has found numerous applications in computer science. However, this result is based on a specific choice of ordering on words, the (scattered) subword ordering. In this paper, we describe to what extent other natural orderings (prefix, suffix, and infix) on words can be used to derive Higman-like theorems. More specifically, we are interested in characterizing languages of words that are well-quasi-ordered under these orderings. We show that a simple characterization is possible for the prefix and suffix orderings, and that under extra regularity assumptions, this also extends to the infix ordering. We furthermore provide decision procedures for a large class of languages, that contains regular and context-free languages.

cs.FL

$\mathbb{N}$-polyregular functions arise from well-quasi-orderings

A fundamental construction in formal language theory is the Myhill-Nerode congruence on words, whose finitedness characterizes regular language. This construction was generalized to functions from $Σ^*$ to $\mathbb{Z}$ by Colcombet, Douéneau-Tabot, and Lopez to characterize the class of so-called $\mathbb{Z}$-polyregular functions. In this paper, we relax the notion of equivalence relation to quasi-ordering in order to study the class of $\mathbb{N}$-polyregular functions, that plays the role of $\mathbb{Z}$-polyregular functions among functions from $Σ^*$ to $\mathbb{N}$. The analogue of having a finite index is then being a well-quasi-ordering. This provides a canonical object to describe $\mathbb{N}$-polyregular functions, together with a powerful new characterization of this class.

cs.FL

Measuring well quasi-ordered finitary powersets

The complexity of a well-quasi-order (wqo) can be measured through three ordinal invariants: the width as a measure of antichains, height as a measure of chains, and maximal order type as a measure of bad sequences. We study these ordinal invariants for the finitary powerset, i.e., the collection Pf(A) of finite subsets of a wqo A ordered with the Hoare embedding relation. We show that the invariants of Pf(A) cannot be expressed as a function of the invariants of A, and provide tight upper and lower bounds for them. We then focus on a family of well-behaved wqos, for which these invariants can be computed compositionally, using a newly defined ordinal invariant called the approximate maximal order type. This family is built from multiplicatively indecomposable ordinals, using classical operations such as disjoint unions, products, finite words, finite multisets, and the finitary powerset construction.

cs.LO

Labelled Well Quasi Ordered Classes of Bounded Linear Clique-Width

We are interested in characterizing which classes of finite graphs are well-quasi-ordered by the induced subgraph relation. To that end, we devise an algorithm to decide whether a class of finite graphs well-quasi-ordered by the induced subgraph relation when the vertices are labelled using a finite set. In this process, we answer positively to a conjecture of Pouzet, under the extra assumption that the class is of bounded linear clique-width. As a byproduct of our approach, we obtain a new proof of an earlier result from Daliagault, Rao, and Thomassé, by uncovering a connection between well-quasi-orderings on graphs and the gap embedding relation of Dershowitz and Tzameret.

cs.LO

Preservation Theorems Through the Lens of Topology

In this paper, we introduce a family of topological spaces that captures the existence of preservation theorems. The structure of those spaces allows us to study the relativisation of preservation theorems under suitable definitions of surjective morphisms, subclasses, sums, products, topological closures, and projective limits. Throughout the paper, we also integrate already known results into this new framework and show how it captures th essence of their proofs.

cs.LO

Commutative N-polyregular functions

This paper studies which functions computed by $\mathbb{Z}$-weighted automata can be realized by $\mathbb{N}$-weighted automata, under two extra assumptions: commutativity (the order of letters in the input does not matter) and polynomial growth (the output of the function is bounded by a polynomial in the size of the input). We leverage this effective characterization to decide whether a function computed by a commutative $\mathbb{N}$-weighted automaton of polynomial growth is star-free, a notion borrowed from the theory of regular languages that has been the subject of many investigations in the context of string-to-string functions during the last decade. Furthermore, we open the road to a generalization of our results to non-commutative functions, by formalizing a canonical computational model for $\mathbb{N}$-weighted automata of polynomial growth based on the notion of residual transducer.

cs.LO

Z-polyregular functions

This paper introduces a robust class of functions from finite words to integers that we call Z-polyregular functions. We show that it admits natural characterizations in terms of logics, Z-rational expressions, Z-rational series and transducers. We then study two subclass membership problems. First, we show that the asymptotic growth rate of a function is computable, and corresponds to the minimal number of variables required to represent it using logical formulas. Second, we show that first-order definability of Z-polyregular functions is decidable. To show the latter, we introduce an original notion of residual transducer, and provide a semantic characterization based on aperiodicity.

cs.FL

Fixed Points and Noetherian Topologies

This paper provides a canonical construction of a Noetherian least fixed point topology. While such least fixed point are not Noetherian in general, we prove that under a mild assumption, one can use a topological minimal bad sequence argument to prove that they are. We then apply this fixed point theorem to rebuild known Noetherian topologies with a uniform proof. In the case of spaces that are defined inductively (such as finite words and finite trees), we provide a uniform definition of a divisibility topology using our fixed point theorem. We then prove that the divisibility topology is a generalisation of the divisibility preorder introduced by Hasegawa in the case of well-quasi-orders.

cs.LO

When Locality Meets Preservation

This paper investigates the expressiveness of a fragment of first-order sentences in Gaifman normal form, namely the positive Boolean combinations of basic local sentences. We show that they match exactly the first-order sentences preserved under local elementary embeddings, thus providing a new general preservation theorem and extending the Lós-Tarski Theorem. This full preservation result fails as usual in the finite, and we show furthermore that the naturally related decision problems are undecidable. In the more restricted case of preservation under extensions, it nevertheless yields new well-behaved classes of finite structures: we show that preservation under extensions holds if and only if it holds locally.

cs.LO

A Structural and Nominal Syntax for Diagrams

The correspondence between monoidal categories and graphical languages of diagrams has been studied extensively, leading to applications in quantum computing and communication, systems theory, circuit design and more. From the categorical perspective, diagrams can be specified using (name-free) combinators which enjoy elegant equational properties. However, conventional notations for diagrammatic structures, such as hardware description languages (VHDL, Verilog) or graph languages (Dot), use a different style, which is flat, relational, and reliant on extensive use of names (labels). Such languages are not known to enjoy nice syntactic equational properties. However, since they make it relatively easy to specify (and modify) arbitrary diagrammatic structures they are more popular than the combinator style. In this paper we show how the two approaches to diagram syntax can be reconciled and unified in a way that does not change the semantics and the existing equational theory. Additionally, we give sound and complete equational theories for the combined syntax.

cs.PL

Diagrammatic Semantics for Digital Circuits

We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about abstract circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.

cs.PL