THE KLEENE FIXED POINT — a dart

KLEENE the least fixed point as a limit — start at nothing and apply the rule forever

Where Knaster–Tarski (dart 363) proves the least fixed point exists, Kleene builds it. For a map that is not just monotone but continuous (preserves limits of ascending chains), the least fixed point is the join of the chain ⊥ ≤ f(⊥) ≤ f²(⊥) ≤ … — start at nothing, apply the rule, and take the limit. This is the meaning given to a recursive definition in denotational semantics: a program that calls itself denotes the least fixed point of its own body, approached one unfolding at a time. Meaning by successive approximation, from the bottom up.

THE TECHNIQUE lfp = ⊔ fⁿ(⊥) — the join of the ascending chain from bottom

The demo climbs the Kleene chain ⊥, f(⊥), f²(⊥)… to the least fixed point: live demo

HISTORY & CREDIT Kleene · the first recursion theorem

“A recursive definition is circular.” — it denotes the least fixed point of its body, reached as the limit of finite unfoldings from ⊥. Circularity resolved by approximation. cited

Kleene · the first recursion theorem — a continuous functional has a least fixed point, ⊔ fⁿ(⊥).
Scott–Strachey · denotational semantics: a recursive program denotes that least fixed point.
vs Tarski · Tarski proves existence (order); Kleene constructs it (limit of a chain).

Nothing, then the rule once, then twice, and on to the limit — the least fixed point, built. What recursion means. Kleene

RECOMMEND FOR I-13 the ascending chain to the lfp, on the compiler

On the canonical compiler, the chain f(x)=min(x+2,10) from ⊥=0 climbs 0,2,4,6,8,10 to the least fixed point 10:

$ i13 run f_kleenefixedpoint.i13 # chain from bottom, f(x)=min(x+2,10) RUN OK · 192 step(s) · peak stack 4 · call depth 7 lfp = 10 -- the join of the ascending chain: least fixed point, constructed

Recommend: Kleene is the least fixed point constructed — the limit of the ascending chain from ⊥ — and it is what a recursive definition means; i13 climbs to 10. Not a keeper (like Knaster–Tarski, the least fixed point is a unique normal form reached from below — confluence, per B42). But the dart that names why i13's own recursion has meaning at all: every def denotes the least fixed point of its body.