On free completely iterative algebras

Jiri Adamek

arxiv: 1906.11166 · v2 · pith:QUV4TI3Inew · submitted 2019-06-26 · 💻 cs.LO

On free completely iterative algebras

Jiri Adamek This is my paper

Pith reviewed 2026-05-25 15:09 UTC · model grok-4.3

classification 💻 cs.LO

keywords finitary set functorsfree algebrascompletely iterative algebraspartial ordersconservative completionbicontinuous functorsrecursive equationsomega-chains

0 comments

The pith

For every finitary set functor free algebras carry a canonical partial order whose conservative completion is the free completely iterative algebra when the functor is bicontinuous.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that free algebras for any finitary set functor come with a natural partial order. When the functor is bicontinuous the conservative completion of that order forms a complete partial order that is exactly the free completely iterative algebra, and the operations extend uniquely and continuously. For arbitrary finitary functors the free algebra and the free completely iterative algebra are posets that share this same conservative completion. Solutions to recursive equations in the free completely iterative algebra arise as the least upper bound of an omega-chain of approximate solutions already present in the free algebra. This supplies an order-theoretic bridge between ordinary free algebras and their iterative versions.

Core claim

Free algebras for finitary set functors F carry a canonical partial order. If F is bicontinuous, the cpo obtained as the conservative completion of the free algebra is the free completely iterative algebra, and its algebra structure is the unique continuous extension of the structure on the free algebra. For general finitary functors the free algebra and the free completely iterative algebra are posets sharing the same conservative completion. For every recursive equation in the free completely iterative algebra there is an omega-chain of approximate solutions in the free algebra whose join solves the equation.

What carries the argument

The conservative completion of the canonical partial order on the free algebra, which carries a continuous algebra structure precisely when the functor is bicontinuous.

If this is right

The algebra structure on the conservative completion is the unique continuous extension of the free algebra structure.
Free algebras and free completely iterative algebras share the same conservative completion for every finitary functor.
Every recursive equation in the free completely iterative algebra is solved by the join of an omega-chain of approximations taken from the free algebra.
The partial order on the free algebra is canonical for every finitary set functor.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The construction may give a uniform way to obtain iterative algebras from ordinary free algebras in settings where bicontinuous functors arise naturally.
The omega-chain approximations suggest an iterative computation procedure that stays inside the free algebra until the limit step.
The shared completion for general finitary functors indicates that the order structure is intrinsic rather than dependent on bicontinuity.

Load-bearing premise

The conservative completion of the partial order on the free algebra exists and the algebra operations extend continuously to it under the bicontinuity assumption on the functor.

What would settle it

A bicontinuous finitary set functor for which the conservative completion of its free algebra fails to satisfy the universal property of the free completely iterative algebra.

read the original abstract

For every finitary set functor F we demonstrate that free algebras carry a canonical partial order. In case F is bicontinuous, we prove that the cpo obtained as the conservative completion of the free algebra is the free completely iterative algebra. Moreover, the algebra structure of the latter is the unique continuous extension of the algebra structure of the free algebra. For general finitary functors the free algebra and the free completely iterative algebra are proved to be posets sharing the same conservative completion. And for every recursive equation e in the free completely iterative algebra we present an omega-chain of approximate solutions in the free algebra whose join is the solution of e.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Adamek shows free algebras for finitary set functors get a canonical poset, with conservative completion yielding the free completely iterative algebra when F is bicontinuous, plus omega-chain approximations for solutions.

read the letter

The core result is that every finitary set functor F makes its free algebra a poset in a canonical way. When F is bicontinuous the conservative completion of that poset is exactly the free completely iterative algebra, and the algebra map extends uniquely and continuously. For general finitary F the two algebras share the same completion. The paper also gives an explicit omega-chain of approximations in the free algebra whose join solves any recursive equation in the iterative one. These constructions look like genuine extensions of the existing theory on iterative algebras rather than restatements. The proofs appear to rest on standard properties of finitary functors and poset completions without introducing fitted parameters or circular definitions. The limitation to set functors and finitary cases keeps the scope modest, but within that scope the claims are stated cleanly. The weakest point is that the conservative completion must be shown to preserve the algebra operations compatibly; the abstract treats this as the main theorem rather than an assumption, so the paper stands or falls on whether the details go through. No internal contradictions jump out from the stated results. This is narrow categorical algebra work aimed at people already using free algebras and coalgebraic semantics. It is worth sending to a serious referee because the constructions are explicit and the claims are checkable against prior literature on iterative algebras.

Referee Report

0 major / 1 minor

Summary. The paper proves that every finitary set functor F equips its free algebra with a canonical partial order. When F is bicontinuous, the conservative completion of this poset yields the free completely iterative algebra, whose algebra structure is the unique continuous extension of the free algebra's structure. For arbitrary finitary F the free algebra and free CIA are posets with identical conservative completions. Solutions of recursive equations in the free CIA arise as joins of explicit omega-chains of approximations taken from the free algebra.

Significance. The results supply a uniform, order-theoretic bridge between free algebras and completely iterative algebras for finitary functors, derived from standard properties of functors and posets without fitted parameters or ad-hoc axioms. This strengthens the categorical and domain-theoretic foundations of iterative structures used in coalgebraic semantics and recursive program models.

minor comments (1)

The precise definition of 'conservative completion' and the statement of bicontinuity should be recalled in the introduction or a preliminary section for readers outside the immediate subfield.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and for the positive assessment and recommendation to accept.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper's claims rest on standard constructions for free algebras of finitary set functors, canonical partial orders induced by the algebra structure, and conservative completions of posets. These are derived from functorial properties and order-theoretic facts without any reduction of a result to a fitted parameter, self-definition, or load-bearing self-citation chain. The abstract and stated theorems present existence and uniqueness results as consequences of the given assumptions on F, with no equations or steps that equate outputs to inputs by construction. This is the expected outcome for a self-contained categorical proof paper.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The results rest on standard category-theoretic assumptions about finitary functors and the existence of free algebras and conservative completions in posets; no free parameters or invented entities are introduced.

axioms (2)

standard math Finitary set functors admit free algebras and preserve the relevant colimits or limits needed for their construction.
Invoked to guarantee the existence of the free algebra carrying the partial order.
domain assumption Bicontinuous functors allow the conservative completion to form a cpo compatible with continuous algebra operations.
Central to the identification of the completion with the free completely iterative algebra.

pith-pipeline@v0.9.0 · 5618 in / 1343 out tokens · 31445 ms · 2026-05-25T15:09:45.914742+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

For every finitary set functor F we demonstrate that free algebras carry a canonical partial order. In case F is bicontinuous, we prove that the cpo obtained as the conservative completion of the free algebra is the free completely iterative algebra.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

the algebra structure of the latter is the unique continuous extension of the algebra structure of the free algebra

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

12 extracted references · 12 canonical work pages · 1 internal anchor

[1]

Aczel and N

P. Aczel and N. Mendler. A ﬁnal coalgebra theorem. CSLI Lecture Notes , 14,

work page
[2]

Center for the Study of Languages and Information, Stan ford

work page
[3]

On free completely iterative algebras

J. Ad´ amek. On terminal coalgebras determined by initial algebra s. ArXive :1906.11166

work page internal anchor Pith review Pith/arXiv arXiv 1906
[4]

Ad´ amek

J. Ad´ amek. Free algebras and automata realizations in the langu age of cate- gories. Comment. Math. Univ. Carolinae , 15:589–602, 1974

work page 1974
[5]

Ad´ amek

J. Ad´ amek. Final colagebras are ideal completions if initial algebr as. J. Logic Comput., 2:217–242, 2002

work page 2002
[6]

Ad´ amek and S

J. Ad´ amek and S. Milius. Terminal coalgebras and free iterative t heories. In- formation and Computation , 204:1139–1172, 2006

work page 2006
[7]

Ad´ amek and V

J. Ad´ amek and V. Trnkov´ a.Automata and algebras in a category . Academic Publishers, 1990

work page 1990
[8]

Banaschewski and E

B. Banaschewski and E. Nelson. Completions of partially ordered sets. SIAM J. Comput. , 11:521–528, 1982

work page 1982
[9]

M. Barr. Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci., 124:182–192, 1994

work page 1994
[10]

C.C. Elgot. Monadic computation and iterative algebraic theories. In Logic Colloqium ’73 . North Holland Publ. Amsterdam, 1975

work page 1975
[11]

S. Milius. Completely iterative algebras and completely iterative mo nads. In- formation and Computation , 196:1–41, 2005

work page 2005
[12]

J. Worrell. On the ﬁnal sequence of a ﬁnitary set functor. Theoret. Comput. Sci., 338:184–199, 2005. ON FREE COMPLETELY ITERATIVE ALGEBRAS 27 Department of Mathematics, F aculty of Electrical Engineer ing, Czech Technical University in Prague, Czech Republic E-mail address : j.adamek@tu-bs.de

work page 2005

[1] [1]

Aczel and N

P. Aczel and N. Mendler. A ﬁnal coalgebra theorem. CSLI Lecture Notes , 14,

work page

[2] [2]

Center for the Study of Languages and Information, Stan ford

work page

[3] [3]

On free completely iterative algebras

J. Ad´ amek. On terminal coalgebras determined by initial algebra s. ArXive :1906.11166

work page internal anchor Pith review Pith/arXiv arXiv 1906

[4] [4]

Ad´ amek

J. Ad´ amek. Free algebras and automata realizations in the langu age of cate- gories. Comment. Math. Univ. Carolinae , 15:589–602, 1974

work page 1974

[5] [5]

Ad´ amek

J. Ad´ amek. Final colagebras are ideal completions if initial algebr as. J. Logic Comput., 2:217–242, 2002

work page 2002

[6] [6]

Ad´ amek and S

J. Ad´ amek and S. Milius. Terminal coalgebras and free iterative t heories. In- formation and Computation , 204:1139–1172, 2006

work page 2006

[7] [7]

Ad´ amek and V

J. Ad´ amek and V. Trnkov´ a.Automata and algebras in a category . Academic Publishers, 1990

work page 1990

[8] [8]

Banaschewski and E

B. Banaschewski and E. Nelson. Completions of partially ordered sets. SIAM J. Comput. , 11:521–528, 1982

work page 1982

[9] [9]

M. Barr. Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci., 124:182–192, 1994

work page 1994

[10] [10]

C.C. Elgot. Monadic computation and iterative algebraic theories. In Logic Colloqium ’73 . North Holland Publ. Amsterdam, 1975

work page 1975

[11] [11]

S. Milius. Completely iterative algebras and completely iterative mo nads. In- formation and Computation , 196:1–41, 2005

work page 2005

[12] [12]

J. Worrell. On the ﬁnal sequence of a ﬁnitary set functor. Theoret. Comput. Sci., 338:184–199, 2005. ON FREE COMPLETELY ITERATIVE ALGEBRAS 27 Department of Mathematics, F aculty of Electrical Engineer ing, Czech Technical University in Prague, Czech Republic E-mail address : j.adamek@tu-bs.de

work page 2005