arXiv subjects

Thomas Seiller

Publications and source records attributed to Thomas Seiller.

At least 19 recordsLinked to original sources

arXiv2026

Compositional Generalization via Structural Identification in a Category-Theoretic Framework

Compositional generalization is usually evaluated through model accuracy. We instead ask which structural or lexical identifications make held-out COGS examples admissible from the structures observed in training. Sentences are represented as functors from syntactic addresses to lexical tokens, and selective collapses induce Kan extensions that propagate observed associations. Across 21 COGS generalization types, admissibility follows distinct identification profiles, while residual failures separate unsupported structural templates. These data-side diagnoses characterize what the training corpus licenses under specified identifications, without training a predictive model.

cs.CL↗

arXiv2026

A calculus of types in Isbell nuclei

We identify two constructions from different mathematical traditions. In linear logic and realisability, logical types are generated rather than fixed in advance: one begins with a universe of realisers equipped with execution, uses orthogonality to test their interactions, and takes types to be the biorthogonally closed subsets. In enriched Isbell duality, a quantitative relation induces an adjunction whose fixed points form a category, its nucleus. These constructions proceed by different means; we show that, in the present setting, they produce the same objects. The shared datum is minimal: an associative product, called execution, and a real-valued measurement, with no compatibility assumed between them. The failure of the measurement to be additive is at once the relation defining orthogonality and the quantitative relation whose Isbell nucleus we form, and the types cut out by orthogonality are exactly the fixed points of the associated adjunction. The identification pays off in both directions. The most natural product of types fails to be associative; repairing this failure forces a different notion of type, sensitive to both sides of a composite, on which the induced product is associative and, when execution has units, carries two residuals. What emerges is a noncommutative Lambek calculus, derived directly from execution and orthogonality rather than imposed. In the reverse direction, each such type, read on the categorical side, generates a quantitative relation of its own, and with it a derived adjunction and a further generation of types; these derived types are again types of the original situation, computed by the residuals of the Lambek calculus. We also prove a coherence theorem for the threefold arrangements of this construction and, in the finite-dimensional case, give explicit formulas for the product.

cs.LO↗

arXiv2026

Mathematical Informatics: Algorithms

This work continues the development of an intensional approach to computability initiated in previous work, in which programs and computations, rather than functions, constitute the primary objects of study. In this setting, models of computation are described as monoid actions on a configuration space, and programs as dynamical systems constrained by this action. Within this framework, we introduce a formal notion of algorithm as a finite directed graph whose edges are labelled by partial maps over an abstract data structure. This definition separates control from data, representing the former as a graph and the latter as an algebra of operations. We then define what it means for a program, in a given model of computation, to implement such an algorithm, by requiring a correspondence between computational steps and labelled transitions that preserves the induced transformations on representations of data. This yields a precise notion of implementation and situates algorithms as abstract partial specifications of computational behaviour.

cs.LO↗

arXiv2026

Linear Realisability and Implicative Algebras

Realizability, introduced by Kleene, can be understood as a concretization of the Brouwer-Heyting-Kolmogorov (BHK) interpretation of proofs, providing a framework to interpret mathematical statements and proofs in terms of their constructive or computational content. Over time, this concept has evolved through various extensions, such as Kreisel's modified realizability or Krivine's classical realizability. Parallel to these developments, Girard's work on linear logic introduced another perspective, often seen as another concrete realization of the BHK interpretation. The resulting constructions, encompassing models like geometry of interaction, ludics, and interaction graphs, were recently unified under the term linear realizability models to stress the intuitive connection with intuitionnistic and classical realizability. The present work establishes for the first time a formal link between linear realizability models and the realizability constructions of Kleene and Krivine. Our approach leverages Miquel's framework: just as linear logic can be viewed as a decomposition of intuitionistic and classical logic, we propose a linear decomposition of implicative algebras and show that linear realisability models provide concrete examples of such decompositions.

cs.LO↗

arXiv2026

Projective metric geometry of tropical nuclei: gap matrices, event loci, and order chambers

The tropical row span and column span of a real matrix are, from the polyhedral point of view, different objects living in different ambient spaces. These polytopes are known to be combinatorially isomorphic as polyhedral complexes; we prove that they are isometric under a Hilbert projective metric. We show that this isometry, along with a considerable amount of additional metric and polyhedral structure, is a direct consequence of a single categorical construction: the Isbell nucleus of the matrix, viewed as a profunctor enriched over the extended reals. The projective nucleus carries two canonical structures inherited from enrichment. The first is a Hilbert projective metric, with respect to which the Isbell conjugate maps are mutually inverse isometries -- this is the Isometry Theorem. The second is a polyhedral cell decomposition cut out by the Isbell inequalities, recovering the type decomposition of tropical convexity. These two structures are linked pointwise by the \emph{gap matrix}. The Events Theorem identifies each positive entry of the gap matrix with the exact projective distance to the locus where the corresponding inequality becomes tight: algebraic slack in the Isbell inequalities equals geometric distance to the cell walls. Thresholding the gap matrix at successive radii produces a constructible sheaf of formal concept lattice towers, extracting discrete algebraic structure from the continuous geometry at each point. In the square case there is generically a unique full-dimensional cell. The Centering Theorem identifies its Chebyshev center -- the point maximally insulated from all cell walls -- and shows that the optimal radius equals the minimum directed cycle mean of an associated digraph, connecting the projective geometry of the nucleus to the classical theory of optimal assignments.

math.AG↗

arXiv2024

Linear Realisability over nets: multiplicatives (long version)

We provide a new realisability model based on orthogonality for the multiplicative fragment of linear logic, both in presence of generalised axioms (MLL*) and in the standard case (MLL). The novelty is the definition of cut elimination for generalised axioms. We prove that our model is adequate and complete both for MLL* and MLL.

cs.LO↗

arXiv2023

Linear Realisability and Cobordisms

Cobordism categories are known to be compact closed. They can therefore be used to define non-degenerate models of multiplicative linear logic by combining the Int construction with double glueing. In this work we detail such construction in the case of low-dimensional cobordisms, and exhibit a connexion between those models and the model of Interaction graphs introduced by Seiller. In particular, we exhibit how the so-called trefoil property is a consequence of the associativity of composition of higher structures, providing a first step toward establishing models as obtained from a double glueing construction. We discuss possible extensions to higher-dimensional cobordisms categories

cs.LO↗

arXiv2023

pymwp: A Tool for Guaranteeing Complexity Bounds for C Programs

Complexity analysis offers assurance of program's runtime behavior, but large classes of programs remain unanalyzable by existing automated techniques.The mwp-flow analysis sidesteps many difficulties shared by existing approaches, and offers interesting features, such as compositionality, multivariate bounds, and applicability to non-terminating programs.It analyzes resource usage and determines if a program's variables growth rates are no more than polynomially related to their inputs sizes.This sound calculus, however, is computationally expensive to manipulate, and provides no feedback if the program does not have polynomial bounds.Those two defaults were addressed in a previous work, and prepared for the tool we present here: pymwp, a static complexity analyzer for C programs based on our improved mwp-flow analysis.

cs.PL↗

arXiv2022

Agafonov's Theorem for finite and infinite alphabets and probability distributions different from equidistribution

An infinite sequence $α$ over an alphabet $Σ$ is $μ$-distributed w.r.t. a probability map $μ$ if, for every finite string $w$, the limiting frequency of $w$ in $α$ exists and equals $μ(w)$. %We raise the question of how to characterize the probability maps $μ$ for which $μ$-distributedness is preserved across finite-state selection, or equivalently, by selection by programs using constant space. We prove the following result for any finite or countably infinite alphabet $Σ$: every finite-state selector over $Σ$ selects a $μ$-distributed sequence from every $μ$-distributed sequence \emph{if and only if} $μ$ is induced by a Bernoulli distribution on $Σ$, that is a probability distribution on the alphabet extended to words by taking the product. The primary -- and remarkable -- consequence of our main result is a complete characterization of the set of probability maps, on finite and infinite alphabets, for which finite-state selection preserves $μ$-distributedness. The main positive takeaway is that (the appropriate generalization of) Agafonov's Theorem holds for Bernoulli distributions (rather than just equidistributions) on both finite and countably infinite alphabets. As a further consequence, we obtain a result in the area of symbolic dynamical systems: the shift-invariant measures $μ$ on $Σ^ω$ such that any finite-state selector preserves the property of genericity for $μ$, are exactly the positive Bernoulli measures.

cs.FL↗

arXiv2022

Multiplicative linear logic from a resolution-based tile system

We present the stellar resolution, a "flexible" tile system based on Robinson's first-order resolution. After establishing formal definitions and basic properties of the stellar resolution, we show its Turing-completeness and to illustrate the model, we exhibit how it naturally represents computation with Horn clauses and automata as well as nondeterministic tiling constructions used in DNA computing. In the second and main part, by using the stellar resolution, we formalise and extend ideas of a new alternative to proof-net theory sketched by Girard in his transcendental syntax programme. In particular, we encode both cut-elimination and logical correctness for the multiplicative fragment of linear logic (MLL). We finally obtain completeness results for both MLL and MLL extended with the so-called MIX rule. By extending the ideas of Girard's geometry of interaction, this suggests a first step towards a new understanding of the interplay between logic and computation where linear logic is seen as a (constructed) way to format computation.

cs.LO↗

arXiv2022

Realizing Implicit Computational Complexity

This abstract aims at presenting an ongoing effort to apply a novel typing mechanism stemming from Implicit Computational Complexity (ICC), that tracks dependencies between variables in three different ways, at different stages of maturation.The first and third projects bend the original typing discipline to gain finer-grained view on statements independence, to optimize loops by hoisting invariant and by splitting loops "horizontally" to parallelize them more efficiently.The second project refines and implements the original analysis to obtain a fast, modular static analyzer.All three projects aims at pushing the original type system, inspired from ICC, to its limits, to assess how ICC can in practice leads to original, sometimes orthogonal, approaches.

cs.CC↗

arXiv2022

A Novel Loop Fission Technique Inspired by Implicit Computational Complexity

This work explores an unexpected application of Implicit Computational Complexity (ICC) to parallelize loops in imperative programs. Thanks to a lightweight dependency analysis, our algorithm allows splitting a loop into multiple loops that can be run in parallel, resulting in gains in terms of execution time similar to state-of-the-art automatic parallelization tools when both are applicable. Our graph-based algorithm is intuitive, language-agnostic, proven correct, and applicable to all types of loops, even if their loop iteration space is unknown statically or at compile time, if they are not in canonical form or if they contain loop-carried dependency. As contributions we deliver the computational technique, proof of its preservation of semantic correctness, and experimental results to quantify the expected performance gains. Our benchmarks also show that the technique could be seamlessly integrated into compiler passes or other automatic parallelization suites. We assert that this original and automatable loop transformation method was discovered thanks to the "orthogonal" approach offered by ICC.

cs.PL↗

arXiv2022

mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity

Implicit Computational Complexity (ICC) drives better understanding of complexity classes, but it also guides the development of resources-aware languages and static source code analyzers. Among the methods developed, the mwp-flow analysis certifies polynomial bounds on the size of the values manipulated by an imperative program. This result is obtained by bounding the transitions between states instead of focusing on states in isolation, as most static analyzers do, and is not concerned with termination or tight bounds on values. Those differences, along with its built-in compositionality, make the mwp-flow analysis a good target for determining how ICC-inspired techniques diverge compared with more traditional static analysis methods. This paper's contributions are threefold: we fine-tune the internal machinery of the original analysis to make it tractable in practice; we extend the analysis to function calls and leverage its machinery to compute the result of the analysis efficiently; and we implement the resulting analysis as a lightweight tool to automatically perform data-size analysis of C programs. This documented effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that furthermore decorrelates the problem of deciding if a bound exist with the problem of computing it.

cs.FL↗

arXiv2022

Agafonov's Proof of Agafonov's Theorem: A Modern Account and New Insights

We give a modern account of Agafonov's original proof of his eponymous theorem. The original proof was only reported in Russian in a journal not widely available, and the work most commonly cited in western literature is instead the English translation of a summary version containing no proofs, and the main proof relied heavily on material well-known in Russian mathematical circles of the day, which perhaps obscures the main thrust of argumentation for modern readers.Our present account recasts Aganofov's arguments using more basic building blocks than in the original proof, and contains some further embellishments to Agafonov's original arguments, made in the interest of clarity. We posit that the modern account provides new insight to the underlying phenomena of the theorem.We also provides some historical context to Agafonov's work, including a short description of some of the ideas that led to Agafonov's own proof, especially emphasizing the important work of Postnikova.

cs.DM↗

arXiv2021

A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory

Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to be closed for essentially two reasons, which we address here by suitably modifying the model. Firstly, a naive closure is too large to be well-defined, which can be overcome by restricting to polynomials which are finitary. Secondly, the resulting putative closure fails to properly take the 2-categorical structure in account. We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets. For those, the constructions involved into composition have to be performed up to homotopy, which is conveniently handled in the setting of homotopy type theory: we use it here to formally perform the constructions required to build our cartesian bicategory, in Agda. Notably, this requires us introducing an axiomatization in a small universe of the type of finite types, as an appropriate higher inductive type of natural numbers and bijections.

cs.LO↗

arXiv2021

An extended and more practical mwp flow analysis

We improve and refine a method for certifying that the values' sizes computed by an imperative program will be bounded by polynomials in the program's inputs' sizes. Our work ''tames'' the non-determinism of the original analysis, and offers an innovative way of completing the analysis when a non-polynomial growth is found. We furthermore enrich the analyzed language by adding function definitions and calls, allowing to compose the analysis of different libraries and offering generally more modularity. The implementation of our improved method, discussed in a tool paper (https://hal.archives-ouvertes.fr/hal-03269121), also required to reason about the efficiency of some of the needed operations on the matrices produced by the analysis. It is our hope that this work will enable and facilitate static analysis of source code to guarantee its correctness with respect to resource usages.

cs.LO↗

arXiv2021

Lower bounds for algebraic machines, semantically

This paper presents a new semantic method for proving lower bounds in computational complexity. We use it to prove that maxflow, a PTIME complete problem, is not computable in polylogarithmic time on parallel random access machines (PRAMs) working with integers, showing that NCZ \neq PTIME, where NCZ is the complexity class defined by such machines, and PTIME is the standard class of polynomial time computable problems (on, say, a Turing machine). On top of showing this new separation result, we show our method captures previous lower bounds results from the literature: Steele and Yao's lower bounds for algebraic decision trees, Ben-Or's lower bounds for algebraic computation trees, Cucker's proof that NC is not equal to PTIME on the reals, and Mulmuley's lower bounds for "PRAMs without bit operations".

cs.CC↗

arXiv2020

Stellar Resolution: Multiplicatives

We present a new asynchronous model of computation named Stellar Resolution based on first-order unification. This model of computation is obtained as a formalisation of Girard's transcendental syntax programme, sketched in a series of three articles. As such, it is the first step towards a proper formal treatment of Girard's proposal to tackle first-order logic in a proofs-as-program approach. After establishing formal definitions and basic properties of stellar resolution, we explain how it generalises traditional models of computation, such as logic programming and combinatorial models such as Wang tilings. We then explain how it can represent multiplicative proof-structures, their cut-elimination and the correctness criterion of Danos and Regnier. Further use of realisability techniques lead to dynamic semantics for Multiplicative Linear Logic, following previous Geometry of Interaction models.

cs.LO↗