KNASTER-TARSKI a monotone map on a lattice — its fixed points are themselves a lattice
On a complete lattice (a set with all meets and joins), any monotone map f (order-preserving: x≤y ⇒ f(x)≤f(y)) has fixed points — and they form a complete lattice of their own, with a least and a greatest. No continuity, no metric, no iteration required for existence; order alone forces it. The least fixed point is the meet of everything f pushes down (∧{x : f(x)≤x}), and it is exactly what an inductive definition means — the smallest set closed under a rule. It is the backbone of program semantics, dataflow analysis, and the theory of recursion.
THE TECHNIQUE monotone f on a complete lattice ⇒ least & greatest fixed points
The demo runs a monotone bitmask map upward from ⊥ to its least fixed point — the closure under the rule: live demo
HISTORY & CREDIT Knaster 1928 · Tarski 1955
“Fixed points need distance and convergence.” — on a lattice, order alone gives them, with a least and a greatest; an inductive definition just is a least fixed point. cited
1928 · Bronisław Knaster (with Tarski) — the lattice-theoretic result for the special case. 1955 · Alfred Tarski — the general theorem: the fixed points form a complete lattice. means · the least fixed point = the smallest set closed under a rule = an inductive definition.
Order-preserving on a lattice is enough — fixed points exist, and the least one is what ‘defined inductively’ means. Knaster / Tarski
RECOMMEND FOR I-13 the least fixed point, on the compiler
On the canonical compiler, a monotone bitmask map from ⊥=1 closes upward to its least fixed point 7 (all three bits) — the closure:
$ i13 run f_knastertarski.i13 # monotone S -> S | (S<<1), capped
RUN OK · 92 step(s) · peak stack 4 · call depth 3
lfp = 7 -- least fixed point: the closure of the rule from the bottom
Recommend, with a keeper note: Knaster–Tarski gives fixed points from order alone, and the least one is the meaning of an inductive definition — i13 closes to 7. It is tempting: a least fixed point is a canonical choice among many, and canonicalization was this campaign's live keeper question. But B42 settled it: the unique least fixed point of a monotone map is a normal form reached order-independently — that is the confluence (crdt) axis, not a new one. Existence-by-order is witnessed; least-fixed-point-as-canonical-form is confluence. Doubly covered. The dart that shows why the batch's target is already on the map.