A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions
Wojciech Różowski
TL;DR
This paper addresses quantifying the distance between languages denoted by regular expressions through the shortest-distinguishing-word metric, and provides a sound and complete quantitative axiomatisation REG built on a quantitative equational theory. By grounding the distance in Brzozowski derivatives, coalgebraic behavioural metrics, and a Banach-space–style lifting of pseudometrics, it shows how to derive distance reasoning without explicit fixpoint rules, relying instead on the infinitary Cont rule and the $\lambda$-Pref axiom. Completeness is achieved by reducing the problem to finite subautomata and applying Kleene fixpoint theory to compute the distance as the infimum of iterative overapproximations, with nonexpansive automata homomorphisms preserving distances. The work unifies language-distance notions with algebraic reasoning, offering a framework extendable to broader coalgebraic distances and to languages with recursive constructs, and pointing toward future work on GKAT/ProbGKAT and related quantitative logics. Overall, the paper advances foundational understanding of quantitative reasoning about regular languages and automata, enabling precise, axiomatic justification of behavioural distances.
Abstract
Deterministic automata have been traditionally studied through the point of view of language equivalence, but another perspective is given by the canonical notion of shortest-distinguishing-word distance quantifying the of states. Intuitively, the longer the word needed to observe a difference between two states, then the closer their behaviour is. In this paper, we give a sound and complete axiomatisation of shortest-distinguishing-word distance between regular languages. Our axiomatisation relies on a recently developed quantitative analogue of equational logic, allowing to manipulate rational-indexed judgements of the form $e \equiv_\varepsilon f$ meaning term $e$ is approximately equivalent to term $f$ within the error margin of $\varepsilon$. The technical core of the paper is dedicated to the completeness argument that draws techniques from order theory and Banach spaces to simplify the calculation of the behavioural distance to the point it can be then mimicked by axiomatic reasoning.