Searcharxiv⌕ Search

arXiv subjects

Lê Thành Dũng Nguyên

Publications and source records attributed to Lê Thành Dũng Nguyên.

At least 19 recordsLinked to original sources
arXiv2026

A finer reparameterisation theorem for MSO and FO queries on strings

We show a theorem on monadic second-order k-ary queries on finite words. It may be illustrated by the following example: if the number of results of a query on binary strings is O(number of 0s $\times$ number of 1s), then each result can be MSO-definably identified from a 0-position, a 1-position and some finite data. Our proofs also handle the case of first-order logic / aperiodic monoids. Thus we can state and prove the folklore theorem that dimension minimisation holds for first-order string-to-string interpretations.

cs.LO↗
arXiv2026

Tree transducers of linear size-to-height increase (and the additive conjunction of linear logic)

We investigate a natural generalization to trees of Hennie machines, a known automaton model for regular string functions. Tree-to-tree Hennie machines are tree-walking tree transducers with the ability to rewrite the node labels of their input tree, subject to a bounded visit restriction. Interestingly, they do not merely compute regular tree functions (i.e. MSO transductions), but a larger class of functions with linear size-to-height increase (LSHI). We prove that this class sits between LSHI macro tree transducers (MTTs) and MSO set interpretations. To argue for its robustness, we show that it is closed under precomposition (resp. postcomposition) by MTTs of linear size (resp. height) increase. As a consequence, it contains the entire composition hierarchy of MTTs of linear height increase; we also prove that this composition hierarchy is strict. Finally, we give an alternative characterization of this function class based on a lambda-calculus with linear types. The key difference with similar characterizations of MSO transductions is the use of additive tuples in the encoding of output trees. Our equivalence proof, using game semantics / geometry of interaction, is heavily inspired by an analogous result on higher-order recursion schemes.

cs.FL↗
arXiv2026

Slightly Non-Linear Higher-Order Tree Transducers

We investigate the tree-to-tree functions computed by "affine $λ$-transducers": tree automata whose memory consists of an affine $λ$-term instead of a finite state. They can be seen as variations on Gallot, Lemay and Salvati's Linear High-Order Deterministic Tree Transducers. When the memory is almost purely affine ($\textit{à la}$ Kanazawa), we show that these machines can be translated to tree-walking transducers (and with a purely affine memory, we get a reversible tree-walking transducer). This leads to a proof of an inexpressivity conjecture of Nguyên and Pradic on "implicit automata" in an affine $λ$-calculus. We also prove that a more powerful variant, extended with preprocessing by an MSO relabeling and allowing a limited amount of non-linearity, is equivalent in expressive power to Engelfriet, Hoogeboom and Samwel's invisible pebble tree transducers. The key technical tool in our proofs is the Interaction Abstract Machine (IAM), an operational avatar of Girard's geometry of interaction, a semantics of linear logic. We work with ad-hoc specializations to $λ$-terms of low exponential depth of a tree-generating version of the IAM.

cs.FL↗
arXiv2026

The structure of polynomial growth for tree automata/transducers and MSO set queries

Given an $\mathbb{N}$-weighted tree automaton, we give a decision procedure for exponential vs polynomial growth (with respect to the input size) in quadratic time, and an algorithm that computes the exact polynomial degree of growth in cubic time. As a special case, they apply to the growth of the ambiguity of a nondeterministic tree automaton, i.e. the number of distinct accepting runs over a given input. We deduce analogous decidability results (ignoring complexity) for the growth of the number of results of set queries in Monadic Second-Order logic (MSO) over ranked trees. In the case of polynomial growth of degree $k$, we also prove a reparameterization theorem for such queries: their results can be mapped to $k$-tuples of input nodes in a finite-to-one and MSO-definable fashion. We then apply these tools to study growth rates and subclass membership problems for tree-to-tree functions. Using new proof strategies, we recover and generalize known results concerning polyregular functions, total deterministic macro tree transducers, and partial nondeterministic top-down tree transducers. In particular, we give a procedure to decide polynomial size-to-height increase for both macro tree transducers and MSO set interpretations, and compute the degree. The paper concludes with a survey of a wide range of related work.

cs.FL↗
arXiv2024

Two or three things I know about tree transducers

You might know that the name "tree transducers" refers to various kinds of automata that compute functions on ranked trees, i.e. terms over a first-order signature. But have you ever wondered about how to remember what a macro tree transducer does? Or what are the connections between top-down tree(-to-string) transducers, multi bottom-up tree(-to-string) transducers, tree-walking transducers, (invisible) pebble tree transducers, monadic second-order transductions, unfoldings of rooted directed acyclic graphs (i.e. term graphs) -- and what happens when the functions that they compute are composed? The answers may be found in old papers (mostly coauthored by Engelfriet), but maybe you can save some time by first looking at this short note.

cs.FL↗
arXiv2024

Simply typed convertibility is TOWER-complete even for safe lambda-terms

We consider the following decision problem: given two simply typed $λ$-terms, are they $β$-convertible? Equivalently, do they have the same normal form? It is famously non-elementary, but the precise complexity - namely TOWER-complete - is lesser known. One goal of this short paper is to popularize this fact. Our original contribution is to show that the problem stays TOWER-complete when the two input terms belong to Blum and Ong's safe $λ$-calculus, a fragment of the simply typed $λ$-calculus arising from the study of higher-order recursion schemes. Previously, the best known lower bound for this safe $β$-convertibility problem was PSPACE-hardness. Our proof proceeds by reduction from the star-free expression equivalence problem, taking inspiration from the author's work with Pradic on "implicit automata in typed $λ$-calculi". These results also hold for $βη$-convertibility.

cs.LO↗
arXiv2024

Function spaces for orbit-finite sets

Orbit-finite sets are a generalisation of finite sets, and as such support many operations allowed for finite sets, such as pairing, quotienting, or taking subsets. However, they do not support function spaces, i.e. if X and Y are orbit-finite sets, then the space of finitely supported functions from X to Y is not orbit-finite. In this paper we propose two solutions to this problem: one is obtained by generalising the notion of orbit-finite set, and the other one is obtained by restricting it. In both cases, function spaces and the original closure properties are retained. Curiously, both solutions are "linear": the generalisation is based on linear algebra, while the restriction is based on linear logic.

cs.LO↗
arXiv2024

Syntactically and semantically regular languages of lambda-terms coincide through logical relations

A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed $λ$-terms, defined using denotational semantics in finite sets. We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal work of Hillebrand and Kanellakis connecting regular languages of words and syntactic $λ$-definability. Second, we show that any finitary extensional model of the simply typed $λ$-calculus, when used in Salvati's definition, recognizes exactly the same class of languages of $λ$-terms as the category of finite sets does. The proofs of these two results rely on logical relations and can be seen as instances of a more general construction of a categorical nature, inspired by previous categorical accounts of logical relations using the gluing construction.

cs.LO↗
arXiv2023

A System of Interaction and Structure III: The Complexity of BV and Pomset Logic

Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originates from the study of coherence spaces and proof nets, BV originates from the study of series-parallel orders, cographs, and proof systems. Both logics enjoy a cut-admissibility result, but for neither logic can this be done in the sequent calculus. Provability in pomset logic can be checked via a proof net correctness criterion and in BV via a deep inference proof system. It has long been conjectured that these two logics are the same. In this paper we show that this conjecture is false. We also investigate the complexity of the two logics, exhibiting a huge gap between the two. Whereas provability in BV is NP-complete, provability in pomset logic is $Σ_2^p$-complete. We also make some observations with respect to possible sequent systems for the two logics.

cs.LO↗
arXiv2023

Refutations of pebble minimization via output languages

Polyregular functions are the class of string-to-string functions definable by pebble transducers, an extension of finite-state automata with outputs and multiple two-way reading heads (pebbles) with a stack discipline. If a polyregular function can be computed with $k$ pebbles, then its output length is bounded by a polynomial of degree $k$ in the input length. But Bojańczyk has shown that the converse fails. In this paper, we provide two alternative easier proofs. The first establishes by elementary means that some quadratic polyregular function requires 3 pebbles. The second proof - just as short, albeit less elementary - shows a stronger statement: for every $k$, there exists some polyregular function with quadratic growth whose output language differs from that of any $k$-fold composition of macro tree transducers (and which therefore cannot be computed by a $k$-pebble transducer). Along the way, we also refute a conjectured logical characterization of polyblind functions.

cs.FL↗
arXiv2021

Implicit automata in typed $λ$-calculi II: streaming transducers vs categorical semantics

We characterize regular string transductions as programs in a linear $λ$-calculus with additives. One direction of this equivalence is proved by encoding copyless streaming string transducers (SSTs), which compute regular functions, into our $λ$-calculus. For the converse, we consider a categorical framework for defining automata and transducers over words, which allows us to relate register updates in SSTs to the semantics of the linear $λ$-calculus in a suitable monoidal closed category. To illustrate the relevance of monoidal closure to automata theory, we also leverage this notion to give abstract generalizations of the arguments showing that copyless SSTs may be determinized and that the composition of two regular functions may be implemented by a copyless SST. Our main result is then generalized from strings to trees using a similar approach. In doing so, we exhibit a connection between a feature of streaming tree transducers and the multiplicative/additive distinction of linear logic. Keywords: MSO transductions, implicit complexity, Dialectica categories, Church encodings

cs.LO↗
arXiv2020

Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix

This paper establishes a bridge between linear logic and mainstream graph theory, building on previous work by Retoré (2003). We show that the problem of correctness for MLL+Mix proof nets is equivalent to the problem of uniqueness of a perfect matching. By applying matching theory, we obtain new results for MLL+Mix proof nets: a linear-time correctness criterion, a quasi-linear sequentialization algorithm, and a characterization of the sub-polynomial complexity of the correctness problem. We also use graph algorithms to compute the dependency relation of Bagnol et al. (2015) and the kingdom ordering of Bellin (1997), and relate them to the notion of blossom which is central to combinatorial maximum matching algorithms. In this journal version, we have added an explanation of Retoré's "RB-graphs" in terms of a general construction on graphs with forbidden transitions. In fact, it is by analyzing RB-graphs that we arrived at this construction, and thus obtained a polynomial-time algorithm for finding trails avoiding forbidden transitions; the latter is among the material covered in another paper by the author focusing on graph theory (arXiv:1901.07028).

cs.LO↗
arXiv2020

Constrained path-finding and structure from acyclicity

This note presents several results in graph theory inspired by the author's work in the proof theory of linear logic; these results are purely combinatorial and do not involve logic. We show that trails avoiding forbidden transitions, properly arc-colored directed trails and rainbow paths for complete multipartite color classes can be found in linear time, whereas finding rainbow paths is NP-complete for any other restriction on color classes. For the tractable cases, we also state new structural properties equivalent to Kotzig's theorem on the existence of bridges in unique perfect matchings. Another result on graphs equipped with unique perfect matchings that we prove here is the combinatorial counterpart of a theorem due to Bellin in linear logic: a connection between blossoms and bridge deletion orders.

cs.DM↗
arXiv2019

When lattice cubes meet affine subspaces: a short note

We give short and simple proofs of what seem to be folklore results: * the maximum cardinality of the intersection of a lattice cube with an affine subspace; * the minimum number of affine subspaces needed to cover a lattice cube.

math.CO↗
arXiv2019

Typed lambda-calculi and superclasses of regular functions

We propose to use Church encodings in typed lambda-calculi as the basis for an automata-theoretic counterpart of implicit computational complexity, in the same way that monadic second-order logic provides a counterpart to descriptive complexity. Specifically, we look at transductions i.e. string-to-string (or tree-to-tree) functions - in particular those with superlinear growth, such as polyregular functions, HDT0L transductions and Sénizergues's "k-computable mappings". Our first results towards this aim consist showing the inclusion of some transduction classes in some classes defined by lambda-calculi. In particular, this sheds light on a basic open question on the expressivity of the simply typed lambda-calculus. We also encode regular functions (and, by changing the type of programs considered, we get a larger subclass of polyregular functions) in the elementary affine lambda-calculus, a variant of linear logic originally designed for implicit computational complexity.

cs.LO↗