Theoretical Computer Science

Motivation

Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by $H_n$. The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most $f$, giving an $f$-approximation.

Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.

Setting

An instance consists of a finite type $E$ of elements, a finite type $S$ indexing available sets, an assignment $s \mapsto A_s \subseteq E$, and a nonnegative cost $c : S \to \mathbb{R}$. Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are

The frequency of an element is the number of sets containing it, and $f$ denotes the maximum frequency over all elements.

The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given $C$ covers is strictly stronger than coverability of the family.

Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when $E$ is empty, $f = 0$ and the $f$-approximation bound reads $\mathrm{cost}(C) \le 0$, which the certificate's tightness clause forces to be $0 \le 0$ rather than anything false.

Formalization targets

The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.

A primal-dual certificate is a pair $(C, y)$ where $C \subseteq S$ covers $E$, $y$ is dual-feasible, and every $s \in C$ has a tight dual constraint, $\sum_{e \in A_s} y_e = c_s$.

Goal — the primal-dual $f$-approximation

For any primal-dual certificate $(C,y)$ and any fractional cover $x$,

Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover $C$ costs at most $f$ times the fractional optimum and a fortiori at most $f$ times the integral optimum.

The double-counting step

The one substantive step of the goal is split out as its own target: for a primal-dual certificate,

Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most $f$ times. With this and weak duality, the goal is two lines.

The greedy bound

A greedy certificate at ratio $\rho$ is a cover $C$ and a nonnegative $y$ with $\sum_{s \in C} c_s = \sum_{e} y_e$ and $\sum_{e \in A_s} y_e \le \rho\, c_s$ for every $s$. For such a certificate and any fractional cover $x$,

Instantiating $\rho = H_n$ is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.

Set-cover weak duality and LP attainment

Every dual packing is bounded by every fractional cover, $\sum_e y_e \le \sum_s c_s x_s$; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.

Significance

This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no $f$-approximation result to build on.

Difficulty

The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.

Formalization scope

Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.

Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.2, pp. 10–14. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Vijay V. Vazirani, Approximation Algorithms, Springer, 2001, Chapters 2 and 15 — the standard treatment of the greedy and primal-dual set-cover analyses.

Motivation

An online algorithm must commit to decisions before it knows the rest of its input, and it is judged by competitive analysis: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.

This mission formalizes the chapter where the method is introduced on its smallest example, the ski-rental problem. A customer needs skis for an unknown number of days: renting costs $1$ per day and buying costs $B$ once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic $2$-competitive algorithm, and a randomized algorithm whose competitive ratio tends to $e/(e-1)$, due to Karlin, Manasse, McGeoch and Owicki (1994). The primal-dual derivation of both is the content of Chapter 3.

Setting

An instance is a pair $(B, k)$: the purchase price $B$, a positive integer, and the number $k \ge 0$ of ski days, which the online algorithm does not know. An offline solution either buys at once, paying $B$, or rents on every day, paying $k$; so the offline optimum is

Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The primal is a covering program with one buy variable $x$ and one rent variable $z_j$ per day $j$:

Its dual is a packing program with one variable $y_j$ per day:

The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.

The fractional primal-dual algorithm maintains $x$, initially $0$. On each new day, while $x < 1$ it sets $z_j \leftarrow 1 - x$, then raises

and sets $y_j \leftarrow 1$; once $x$ has reached $1$ it does nothing further. The free parameter $c$ is then pinned to the value that makes $x$ reach exactly $1$ after $B$ days,

Formalization targets

Goal — the fractional algorithm's competitive ratio at finite $B$

The coefficient is the exact finite-$B$ ratio $1 + 1/c$, left in closed form rather than replaced by a constant. This is deliberate: $\left(1+\frac1B\right)^B$ increases to $e$, so $c < e - 1$ and therefore $1 + 1/c > e/(e-1)$ for every finite $B$. A goal asserting $e/(e-1)$-competitiveness at finite $B$ would be false, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.

Asymptotic companion — where $e/(e-1)$ actually lives

The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.

Parallel target — the deterministic algorithm

Chapter 3's other result, independent of the fractional development.

Significance

The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the derivation: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.

On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision 0df444a, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.

Difficulty

The offline problem is trivial, and a newcomer's first move — prove $\min(B,k)$ is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:

The optimum is never observed. The algorithm's cost must be compared against $\min(B,k)$ without $k$ being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.

The growth law is piecewise. The update fires only while $x < 1$. Summing the per-day increments therefore does not telescope uniformly: days before $x$ reaches $1$ contribute $1 + 1/c$ each and later days contribute nothing, and the index at which the switch happens is exactly $B$ — which is a theorem about the recurrence, not an assumption.

The constant is forced, not chosen. $c = (1+1/B)^B - 1$ is not a free tuning parameter; it is the unique value for which the geometric sequence $x_j = \bigl((1+1/B)^j - 1\bigr)/c$ hits $1$ at $j = B$, which is in turn what makes the dual solution feasible ($\sum_j y_j \le B$). Dual feasibility and the choice of $c$ are the same fact.

Formalization scope

Conventions this development commits to. The purchase price is a natural number $B$ with $0 < B$, because Chapter 3 uses $B$ simultaneously as a price, as a day index ("buy skis on the $B$th day"), and as the exponent in $(1+1/B)^B$; costs are real numbers, with $B$ and $k$ coerced. Days are indexed from $0$, so day $j+1$ of the prose is index $j$, and Fin k indexes the $k$ days. Real division is total, so $1/0 = 0$; the hypothesis $0 < B$ is what keeps every reciprocal in the development genuine, and without it $c$ would evaluate to $0$ and the recurrence would collapse to the constant zero sequence. The algorithm's x < 1 guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day $B$.

A documented discrepancy in the source. The prose on p. 17 relaxes the integer program by letting $x$ and each $z_j$ range over $[0,1]$; Figure 3.1 on p. 18 prints only $x \ge 0$, $z_j \ge 0$. This mission takes the prose version, $0 \le x \le 1$ and $0 \le z_j \le 1$, as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value $\min(B,k)$, so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.

Ruling out a trivializing formalization. The offline optimum is defined independently, as $\min(B,k)$, and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to $(1+1/c)$ times the number of days on which $x < 1$ — so it cannot be weakened into vacuity without becoming false.

Infrastructure, and what is reusable. The development needs only Mathlib big operators over Fin k, basic real analysis for the limit, and IsLeast. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.

Out of scope here. The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold $\alpha \in [0,1]$ uniformly and buying on the day whose increment of $x$ contains $\alpha$. That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental. Contributions here should not anticipate it.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008. Chapter 3, pp. 17–19. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024
• Anna R. Karlin, Mark S. Manasse, Lyle A. McGeoch and Susan Owicki, Competitive randomized algorithms for nonuniform problems, Algorithmica 11(6), 1994, 542–571. https://doi.org/10.1007/BF01294260
• Allan Borodin and Ran El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

Comparing undecidable problems

Computability theory studies which questions admit algorithms and how the unsolvable questions compare with one another. A decision problem can be represented by a set of natural numbers: the question on input $n$ is whether $n$ belongs to the set. Even when there is no algorithm that always answers this question, there may be an algorithm that eventually recognizes every positive instance. Understanding the relative difficulty of such problems is the setting of the Friedberg–Muchnik theorem.

The original paper by Richard M. Friedberg appeared in 1957 under the title Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944). It supplies the historical paper source for this formalization. A. A. Muchnik's independent contribution appeared in Russian in 1956. Friedberg, PNAS 43(2), 236–238; Muchnik, Math-Net bibliography, 1956 entry.

Sets, enumeration, and oracle access

A set $A\subseteq\mathbb N$ is computably enumerable, abbreviated c.e., if membership has a semidecision procedure: on input $n$, the procedure halts exactly when $n\in A$. The older terminology is recursively enumerable, abbreviated r.e. The Lean predicate CEnumerable A uses Mathlib's REPred for this property. A computable set has a decision procedure that terminates on every input and answers membership correctly; this is expressed separately by ComputableSet A using ComputablePred.

For each set $A$, define its characteristic function by

An oracle for $A$ answers requests for this function's values. It always supplies an answer, even if membership in $A$ cannot be computed without an oracle. The declaration setOracle A represents this total function inside Mathlib's type of partial functions from natural numbers to natural numbers.

Write $A\le_T B$ when an algorithm with access to the membership oracle for $B$ computes $\chi_A$ on every input. This is Turing reducibility, expressed by SetTuringReducible A B. The algorithm may make several queries, with later queries depending on earlier answers. Incomparability requires both $A\not\le_T B$ and $B\not\le_T A$; it is stronger than saying the two sets merely have different degrees. These conventions specify the mathematical reading of the supplied Lean definitions.

Formalization target

The goal is the following unconditional existence statement:

Its Lean name is Computability.friedberg_muchnik. No enumeration, pair of sets, or oracle program is supplied as a hypothesis. Both sets must be obtained as witnesses to the conclusion. The statement matches Theorem 26.2 in Arnold W. Miller's Lecture notes in Recursion Theory, Section 26, with the theorem on page 51 and its proof on pages 51–54. Miller, December 3, 2008 version.

Mathematical and formal significance

The target establishes that the c.e. problems have incomparable levels of computational difficulty. Its witnesses cannot be computable: a computable membership procedure would also work in the presence of any other oracle simply by making no queries, contradicting the required nonreducibility. The stronger historical consequence is a positive solution of Post's problem: a c.e. degree can lie strictly between the computable degree and the halting degree. Miller records this consequence separately as Corollary 26.3 on page 54. Miller, Section 26.

The mathematical theorem is established; the work requested here is its Lean 4 formalization. A completed development must construct witnesses, prove their computable enumerability, and exclude oracle computations in each direction using Mathlib's actual reducibility relation. The provided goal currently ends in sorry. Successful compilation of this statement checks its formulation and imports; it does not constitute a proof of the existence result.

Difficulty of simultaneous requirements

The main obstacle is preserving decisions about oracle computations while both sets are still being enumerated. An additional element in one set can change an oracle answer used by an earlier computation, undermining the attempt to separate the other set from it. There are infinitely many candidate programs in both directions. Thus a formal treatment has to justify the eventual stability of the relevant computations as well as the effectiveness of the enumeration. This is the setting of the finite injury argument developed in Miller's proof of Theorem 26.2. Miller, pages 51–54.

Formalization scope

The sets are arbitrary Set ℕ, including the natural number zero in their ambient domain. The oracle answers use natural numbers, with one for membership and zero for nonmembership. Classical reasoning is used to define the oracle for an arbitrary set; it supplies no assertion that this function is computable. Each oracle is nevertheless total. Replacing it with a partial membership recognizer would change the meaning of the target.

The foundation consists of Mathlib.Computability.RE and Mathlib.Computability.TuringDegree, together with the supplied definitions in namespace Computability. SetTuringEquivalent records reducibility in both directions. degreeOfSet maps a characteristic-function oracle to its Turing degree, and CEnumerableDegree says that a degree has a c.e. representative. These additional definitions are retained as useful interfaces, while the root theorem itself is expressed directly with sets and TuringIncomparable.

A complete proof will need representations of effective finite stages and oracle computations, and lemmas relating those representations to the imported predicates. Such infrastructure can support later formalizations involving oracle use, computable enumerations, and priority constructions. Contributions should establish these connections with Mathlib's definitions and finish the unconditional target. The theorem must not be replaced by mere degree inequality, weakened reducibility, or a conditional assertion that assumes the required incomparable sets already exist.

Selected references

• Richard M. Friedberg, Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944), Proceedings of the National Academy of Sciences of the USA 43(2), 236–238, 1957. DOI; free archived paper.
• A. A. Muchnik, On the unsolvability of the problem of reducibility in the theory of algorithms (Russian: Неразрешимость проблемы сводимости теории алгоритмов), Doklady Akademii Nauk SSSR 108(2), 194–197, 1956. Math-Net bibliography, 1956 entry.
• Arnold W. Miller, Lecture notes in Recursion Theory, University of Wisconsin–Madison, version dated December 3, 2008, Section 26, Theorem 26.2, pages 51–54. Author-hosted PDF.

Motivation

Classical Eilenberg correspondence theorems connect algebraic descriptions of finite-state behavior with language-theoretic closure principles. The version developed by Juan Climent Vidal and Enric Cosme Llópez replaces one-sorted monoids by many-sorted algebras, so that operations may accept arguments of several prescribed sorts and return a value of another sort. This is the natural algebraic setting for typed term languages: a signature records the permitted input and output sorts of each operation, and a language is a family of sets indexed by sorts. The paper proves that two ways of organizing finite-state behavior—through finite-index congruences and through regular languages—determine the same ordered structure. The source is the final section of Climent Vidal and Cosme Llópez, Eilenberg theorems for many-sorted formations, published in the Houston Journal of Mathematics 45(2), 2019.

The companion manuscript A Kleene theorem for free many-sorted algebras develops the free-term and recognizability infrastructure used by this formalization. It supplies a concrete Lean representation of sorted signatures, free algebras, homomorphisms, terms, and finite many-sorted carriers. The present mission begins from that reusable core and formalizes the formation-level theorem of the HJM paper, rather than repeating the already completed Kleene development.

Setting

Fix a finite type of sorts $S$ and an $S$-sorted signature $\Sigma$. For an $S$-sorted set $X$, write $T_\Sigma(X)$ for the free $\Sigma$-algebra on $X$. A congruence $\Phi$ on a many-sorted algebra is a family of equivalence relations $\Phi_s$, one on each carrier sort, compatible with every basic operation. Its index is finite when the entire sorted quotient family

is finite. A sorted language $L$ is $\Phi$-saturated when membership in $L_s$ is constant on every $\Phi_s$-class. The syntactic congruence $\Omega(L)$ is the greatest algebra congruence that saturates $L$, and $L$ is regular when $\Omega(L)$ has finite index.

A finite-index congruence formation $\mathfrak F$ selects, for every variable family $X$, a nonempty filter $\mathfrak F(X)$ of finite-index congruences on $T_\Sigma(X)$. The selection is closed under intersections, upward inclusion, and pullback along homomorphisms whose composite with the relevant quotient projection is surjective at every sort.

A regular-language formation $\mathcal L$ selects regular languages in each $T_\Sigma(X)$. It contains every language saturated by the universal congruence; whenever $L,K\in\mathcal L(X)$ it contains every language saturated by $\Omega(L)\cap\Omega(K)$; and it satisfies the corresponding pullback-saturation condition for quotient-surjective homomorphisms.

The two constructions are

and

Formalization targets

The capstone is the paper's final formation theorem: the ordered sets of finite-index congruence formations and regular-language formations are order-isomorphic, with the isomorphism fixed to be exactly the two displayed constructions.

The milestones establish the universal property of the syntactic congruence, closure of finite-index congruences under the filter operations, the well-definedness of each construction, and the two recovery identities

These identities determine the inverse maps and prevent the goal from being satisfied by an unrelated abstract order equivalence.

Significance

The theorem packages a family of finite quotients and a family of regular languages as interchangeable data. On the algebraic side, closure is expressed by filters of congruences and quotient-surjective pullbacks. On the language side, the same information is expressed through saturation by syntactic congruences. The result therefore gives a systematic translation between quotient-based and language-based classifications in a typed, many-sorted setting.

Formalizing the theorem adds congruence, quotient-index, saturation, syntactic-congruence, and formation interfaces to the existing free many-sorted algebra library. These components are reusable for future formalizations of recognizability, Myhill–Nerode principles, finite algebra formations, and varieties or pseudovarieties of typed algebras. The mathematical theorem is already proved in the cited 2019 paper; the remaining task is to produce machine-checked Lean proofs of the source-faithful statements.

Difficulty

The two maps are simple to write down but their inverse laws are not pointwise tautologies. A finite-index congruence must be reconstructed from the family of all languages it saturates, and a language formation must be reconstructed from all selected finite-index congruences. In the many-sorted case, finiteness applies to the entire quotient family, including its support across sorts, and intersections and pullbacks must preserve this global condition. The quotient-surjectivity premise is also essential: replacing it by ordinary surjectivity of the original homomorphism would change the formation axiom.

The syntactic congruence creates a second layer of care. It must be characterized as the greatest compatible sorted equivalence saturating a language, not merely as the kernel of the language's characteristic function, which need not itself respect the algebra operations. Thus an argument that treats saturation as an arbitrary set-theoretic equivalence misses the algebraic compatibility required by the theorem.

Formalization scope

The Lean development uses the existing MSKleene representation of sorted sets, signatures, argument tuples, algebras, homomorphisms, terms, and free algebras. Congruences are sort-indexed setoids with explicit compatibility for every signature operation. Their order is inclusion of relations. Intersection and the universal congruence are concrete constructions, while pullback is defined along an algebra homomorphism.

Finite index is represented by finiteness of the sigma-type of all quotient carriers, matching the paper's finite sorted-set convention; it is not weakened to separate finiteness of each inhabited component. The sort type is assumed finite in the finite-index filter and formation correspondence theorems, as required in the final section of the source. Languages are arbitrary sorted subsets of free term algebras, including empty components. No nonemptiness assumption on variable carriers or algebra sorts is added.

The syntactic congruence is defined internally as the supremum-style least upper bound of all congruences saturating a language, rather than postulated together with its universal property. The formation structures contain only the source closure axioms. In particular, neither correspondence map nor either inverse identity is stored as a structure field; doing so would trivialize the capstone. Contributions are welcome on the foundational universal-property and finite-index lemmas, the two formation constructors, and the recovery identities that assemble into the final order isomorphism.

Selected references

• Juan Climent Vidal and Enric Cosme Llópez, Eilenberg theorems for many-sorted formations, Houston Journal of Mathematics 45(2), 2019, pp. 351–416. arXiv:1604.04792
• Samuel Eilenberg, Automata, Languages, and Machines, Volume B, Academic Press, 1976.
• Adolfo Ballester-Bolinches, Jean-Éric Pin, and Xaro Soler-Escrivà, Formations of finite monoids and formal languages: Eilenberg's variety theorem revisited, Forum Mathematicum 26, 2014, pp. 1737–1761.

Motivation

Kleene's theorem (Kleene 1956; McNaughton–Yamada 1960) is a cornerstone of formal language theory: over a free monoid, the languages recognized by finite automata are exactly the regular ones — those built from finite languages by union, concatenation, and the Kleene star. Mezei and Wright (1967) lifted recognizability off strings, calling a subset of an arbitrary algebra recognizable when it is the preimage of a subset of a finite algebra under a homomorphism. Replacing strings by terms — finite trees labelled by operation symbols — gives the theory of recognizable tree languages and finite tree automata of Gécseg and Steinby (1984), where the Kleene correspondence reappears with a tree concatenation and an iteration operation in the role of the star.

Many computational structures are inherently many-sorted: typed lambda calculi, structured programming languages, process calculi, XML schemas — data and operations organized into distinct sorts. In the many-sorted setting a signature assigns to each operation symbol the sorts of its arguments and of its value, variables carry sorts, and a language is a sort-indexed family of term sets. The predecessor of this mission, Climent Vidal–Cosme Llópez 2020 (CVCL20), established that recognizability over free many-sorted algebras is preserved — and, where applicable, reflected — by substitution, iteration, quotient, inverse tree-homomorphic image, and direct linear image, via finite-index congruences. What CVCL20 left open is the regular side: whether a natural class of many-sorted regular expressions captures exactly the recognizable languages. This mission closes that gap.

Setting

Fix a finite set of sorts $S$. An $S$-sorted set $A = (A_s)_{s\in S}$ is a family of sets; it is finite when $\coprod_{s\in S} A_s$ is finite. An $S$-sorted signature $\Sigma$ assigns to each pair $(\mathbf{s}, s) \in S^\star \times S$ a set $\Sigma_{\mathbf{s},s}$ of operation symbols of arity $\mathbf{s}$ and coarity $s$. A $\Sigma$-algebra $\mathbf{A}$ is an $S$-sorted set $A$ together with, for each $\sigma \in \Sigma_{\mathbf{s},s}$, an operation $\sigma^{\mathbf A}\colon A_{\mathbf s} \to A_s$, where $A_{\mathbf s} = \prod_{j} A_{s_j}$. A homomorphism commutes with all operations sortwise.

The free $\Sigma$-algebra $\mathbf T_\Sigma(X)$ on an $S$-sorted set $X$ of variables has as its sort-$s$ carrier $\mathrm T_\Sigma(X)_s$ the set of $(X,s)$-terms; every $S$-sorted map $X \to A$ extends uniquely to a homomorphism $\mathbf T_\Sigma(X) \to \mathbf A$. Following automata-theoretic tradition, subsets of $\mathrm T_\Sigma(X)$ are called languages. For a sort $s$, a language $L \subseteq \mathrm T_\Sigma(X)_s$ is $s$-recognizable when there are a finite $\Sigma$-algebra $\mathbf N$, a homomorphism $f\colon \mathbf T_\Sigma(X) \to \mathbf N$, and a subset $M \subseteq N_s$ with $L = f_s^{-1}[M]$. Write $\mathrm{Rec}_s(\mathbf T_\Sigma(X))$ for the set of all such $L$.

Two operations on languages, both performed sortwise, generate the regular expressions. Given a variable $z \in X_u$ and a language $L \subseteq \mathrm T_\Sigma(X)_u$, $z$-substitution $\left(\!\begin{smallmatrix}z\\ L\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s$ replaces, in every term of an input language of sort $s$, each occurrence of $z$ independently by a term of $L$. The $z$-iteration is $L^{\star z} = \bigcup_{i\in\mathbb N} L^{i\,z}$, where $L^{0\,z} = \{z\}$ and $L^{i+1\,z} = L^{i\,z} \cup \left(\!\begin{smallmatrix}z\\ L^{i\,z}\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s(L)$. For a finite $S$-sorted set $Z$, the regular signature $\mathrm{Reg}(S,\Sigma,Z)$ expands $\Sigma$ by an empty constant $\varnothing_s$, a binary sum $+_s$, a unary $z$-iteration $(\cdot)^{\star z}$ for each $z\in Z_s$, and a $z$-substitution operation for each $z\in Z_t$. Its terms are the regular expressions over $(S,\Sigma,Z)$; the power algebra $\mathbf T_\Sigma(Z)^\wp$ carries a canonical $\mathrm{Reg}(S,\Sigma,Z)$-algebra structure, and interpreting a regular expression there yields a language $\{R\}^{Z\sharp}_s$. A language $L\subseteq \mathrm T_\Sigma(X)_s$ is $s$-regular when $L = \{R\}^{Z\sharp}_s$ for some finite $Z\supseteq X$ and some regular expression $R$ of type $s$; write $\mathrm{Reg}_s(\mathbf T_\Sigma(X))$.

Formalization targets

Goal — the many-sorted Kleene theorem

The statement fixes no automaton model and no normal form for regular expressions: it asserts only that the two classes of languages coincide, at every sort, for every finite $S$, every finite $S$-sorted signature $\Sigma$, and every finite $S$-sorted set $X$. It splits into $\mathrm{Reg}_s \subseteq \mathrm{Rec}_s$ (Corollary 4.8) and $\mathrm{Rec}_s \subseteq \mathrm{Reg}_s$ (Proposition 4.10).

Significance

The result completes the Kleene–Myhill–Nerode correspondence on the side of universal algebra, uniformly over an arbitrary finite many-sorted signature: it names the exact operations — those of $\Sigma$, plus empty language, union, sortwise substitution, and sortwise iteration — that generate precisely the finite-state behaviours. Over non-free structures the correspondence is known to fail (recognizable but non-rational subsets of a monoid, Eilenberg 1974), which is what makes the free many-sorted algebra the natural home for an exact statement. The forward direction organizes the regular languages into a $\mathrm{Reg}$-algebra and instantiates the closure properties of CVCL20; the converse gives a constructive, syntactic procedure — from a recognizing homomorphism it builds a regular expression denoting the language — generalizing Lemma 2.5.7 of Gécseg–Steinby, itself descended from McNaughton–Yamada.

The paper is new (June 2026) and has no machine-checked proof. This mission produces the first formalization: a reusable Lean development of finite many-sorted universal algebra — signatures, algebras, free term algebras and their universal property, the Artinian subterm order, power algebras, recognizability, and the substitution/iteration calculus — together with the two inclusions and the state-elimination argument. Everything below the §4 headline results is infrastructure of independent value for many-sorted formal language theory.

Difficulty

The converse inclusion is the substance. The single-sorted proof eliminates automaton states one at a time along a single axis; the naive port to the many-sorted case — fix a linear order on all states and eliminate — loses track of the sort at which each elimination happens and does not terminate cleanly. The argument instead carries a sortwise budget: an $S$-sorted family $K \le N$ recording, for each sort $t$, the set $K_t$ of state values still admissible at internal subterms. The induction is on $\lVert\lVert K\rVert\rVert = \sum_{s\in S} k_s$, and each step removes the top state of one chosen sort, so the recursion branches over the sorts whose budget is nonzero and the key identity (Equation (E)) is a union over those sorts. The inductive invariant — the family of auxiliary languages $L_u(C,K,l)$ with its budget bookkeeping — is what separates the many-sorted argument from its ancestor; it is also the part Gécseg–Steinby declare "obvious from the construction" and this proof spells out in full (Claims C1–C6).

Formalization scope

Proposed Lean representation: $S$ a type with [Fintype S]; an $S$-sorted set as S → Type; a signature as a family List S → S → Type with finiteness where the theorems need it; the free algebra as an inductive term type; the power algebra with sort-$s$ carrier Set (T_Σ Z s); $s$-recognizability as the existence of a finite $\Sigma$-algebra, a homomorphism, and a subset whose sortwise preimage is the language. Committed conventions: $S$ finite throughout; $\Sigma$ finite and $X$ finite for the §4 results (so that only finitely many basic terms exist and the budget induction is well-founded); the regular operations are exactly $\{\varnothing, +, (\cdot)^{\star z}, z\text{-subst}\}$ together with the operations of $\Sigma$ — not an unrestricted Boolean or closure algebra, which would trivialize the statement.

A complete development needs: the many-sorted UA core (sorted sets and maps, signature, algebra, homomorphism, subalgebra, congruence); the free algebra with unique readability (Proposition 3.4) and universal property (Proposition 3.5); the Artinian subterm order (Proposition 3.6); the power algebra; recognizability and $s$-recognizability with the CVCL20 closure results (Propositions 3.29, 3.30, 3.33); the substitution and iteration calculus (Lemmas 3.23, 3.25, 3.28, Corollary 3.17, Lemma 3.18); and the §4 regular-expression layer (Definition 4.1, Proposition 4.3, Corollary 4.4, Definition 4.6). The UA core and the substitution calculus are reusable beyond this mission. Contributions are welcome at every level — the definitions, the closure results, the auxiliary claims C1–C6, and either inclusion.

Selected references

• L. Gong, R. Ruiz Mora, N. Sanmartín Vich, E. Cosme Llópez, A Kleene theorem for free many-sorted algebras, 2026.
• J. Climent Vidal, E. Cosme Llópez, Congruence-based proofs of the recognizability theorems for free many-sorted algebras, Journal of Logic and Computation 30(2) (2020), 561–633. https://arxiv.org/abs/1808.08217
• F. Gécseg, M. Steinby, Tree Automata, Akadémiai Kiadó, Budapest, 1984.
• R. McNaughton, H. Yamada, Regular expressions and state graphs for automata, IRE Transactions on Electronic Computers EC-9 (1960), 39–47.
• S. C. Kleene, Representation of events in nerve nets and finite automata, in Automata Studies, Princeton University Press, 1956, 3–42.
• J. Mezei, J. Wright, Algebraic automata and context-free sets, Information and Control 11 (1967), 3–29.
• S. Eilenberg, Automata, Languages, and Machines, Vol. A, Academic Press, New York, 1974.

Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every $n\ge 3$, an eventual quantitative upper bound, the conclusion $f(n)=n^{1/2+o(1)}$, and the exact affirmative answer to the original upper-bound question.

Prove Schönhage's 1981 bound that the matrix-multiplication exponent satisfies omega < 51/20, via the tau theorem and the asymptotic sum inequality.