The closed form of a diverging fixed point

Divergence is denoted directly, by the infinite iteration Relation.omega (Extra/Rel.lean), which is what the semantics in Core/*/Semantics/Process.lean use. This module is about the other denotation — the greatest fixed point the framework starts from — and about when the two agree:

gfp (λ x, Y ∪ X ∘ᵣ₁ x)  =  (X* ∘ᵣ₁ Y) ∪ X^∞

Nothing in the compiler or its refinement proofs may depend on that identity, and nothing does. It is stated here because the fixed-point presentation computes with it, and because writing down the exact hypothesis it needs is what justifies not taking the greatest fixed point as the definition in the first place.

Split from Extra/Rel.lean on the same principle as the rest of this library: Extra/ carries what the semantics need — ∘ᵣ₁, Monoid.partialProd, ωMonoid, Relation.omega — and everything whose only consumer is a refinement proof lives here.

Unfolding the infinite iteration

R^∞ = R ∘ᵣ₁ R^∞ is the one recursion equation Relation.omega might be expected to satisfy for free, and it does not: neither inclusion holds without ωMonoid.unfold. The states and steps line up on both sides regardless — the whole content is the trace, and a bare product operation says nothing about how the infinite product relates to its own tail. Taking ωProd _ := 1 on Multiplicative ℕ and R = {((), ofAdd 1, ())} makes the two sides {((), 1)} and {((), ofAdd 1)}, disjoint.

theorem Relation.omega_unfold {α : Type u_1} {ε : Type u_2} [Monoid ε] [ωMonoid ε] (R : Set (α × ε × α)) : omega R = R ∘ᵣ₁ omega R

The infinite iteration unfolds by one step. Both inclusions need the unfold law; see the section comment for the counterexample without it.

The identity, and the hypothesis it needs

Only one inclusion is unconditional. The functional is not contractive when X can step emitting nothing, so its greatest fixed point overshoots: at X = {(σ, 1, σ)} and Y = ∅ the functional is the identity and its greatest fixed point is ⊤, pairing σ with every trace whatsoever, while the right-hand side gives {(σ, 1)} — the trace that execution actually emits. The leak is entirely on the gfp side.

Relation.Productive is the exact boundary, not merely a convenient sufficient condition: it is what fails in that counterexample. It is deliberately not satisfied by the semantics this development compiles — while TRUE { x := x + 1 } diverges silently — which is why Algebra.diverging is Relation.omega and never a greatest fixed point.

def Relation.Productive {α : Type u_1} {ε : Type u_2} [Monoid ε] (R : Set (α × ε × α)) : Prop

No infinite run of R emits nothing forever.

Stated as a negated existential rather than as "infinitely many steps emit something", because the run whose productivity is at stake is produced by dependent choice: its states are not known in advance, so there is nothing to quantify over positively.

Equations

• Relation.Productive R = ¬∃ (σ : ℕ → α), ∀ (i : ℕ), (σ i, 1, σ (i + 1)) ∈ R

def Relation.divFun {α : Type u_1} {ε : Type u_2} [Monoid ε] (X : Set (α × ε × α)) (Y : Set (α × ε)) : Set (α × ε) →o Set (α × ε)

The functional whose greatest fixed point is the other denotation of divergence: one X-step in front of the rest, or stop in Y.

Equations

• Relation.divFun X Y = { toFun := fun (x : Set (α × ε)) => Y ∪ X ∘ᵣ₁ x, monotone' := ⋯ }

@[simp]

theorem Relation.divFun_apply {α : Type u_1} {ε : Type u_2} [Monoid ε] {X : Set (α × ε × α)} {Y x : Set (α × ε)} : (divFun X Y) x = Y ∪ X ∘ᵣ₁ x

theorem Relation.closedForm_le_gfp {α : Type u_1} {ε : Type u_2} [Monoid ε] [ωMonoid ε] {X : Set (α × ε × α)} {Y : Set (α × ε)} : star X ∘ᵣ₁ Y ∪ omega X ≤ OrderHom.gfp (divFun X Y)

The closed form is below the greatest fixed point, unconditionally: it is a post-fixed point. This is the half of the identity that always holds.

theorem Relation.gfp_le_closedForm {α : Type u_1} {ε : Type u_2} [Monoid ε] [ωMonoid ε] {X : Set (α × ε × α)} {Y : Set (α × ε)} (prod : Productive X) : OrderHom.gfp (divFun X Y) ≤ star X ∘ᵣ₁ Y ∪ omega X

The converse inclusion, under productivity. Unfolding the fixed point greedily either reaches Y — a finite run, hence X* ∘ᵣ₁ Y — or never does, and dependent choice then produces an infinite run whose partial products are all left factors of the trace. Productivity turns that into an equality with the infinite product; without it the trace is never pinned down, which is exactly the counterexample.

theorem Relation.gfp_eq_closedForm {α : Type u_1} {ε : Type u_2} [Monoid ε] [ωMonoid ε] {X : Set (α × ε × α)} {Y : Set (α × ε)} (prod : Productive X) : OrderHom.gfp (divFun X Y) = star X ∘ᵣ₁ Y ∪ omega X

The paper's identity, with the hypothesis it needs.

Checks against the least fixed points

The semantics are the closed forms; these two identities say the closed forms denote what the least fixed points used to. They are checks, not machinery — nothing depends on them, and if either failed the redefinitions in Core/*/Semantics/Process.lean would be wrong.

There is no third identity. The greatest fixed point of the diverging functional is not Relation.omega, which is the whole point of Relation.gfp_eq_closedForm above and of that functional no longer being the definition.

theorem Relation.star.snoc {α : Type u_1} {ε : Type u_2} [Monoid ε] {R : Set (α × ε × α)} {a b c : α} {e e' : ε} (h : (a, e, b) ∈ star R) (h' : (b, e', c) ∈ R) : (a, e * e', c) ∈ star R

A run followed by one more step is a run. The ∘ᵣ₂ orientation: Relation.star.head extends a run on the left, and the reducing functional extends it on the right.

def Relation.starFun {α : Type u_1} {ε : Type u_2} [Monoid ε] (X : Set (α × ε × α)) : Set (α × ε × α) →o Set (α × ε × α)

The functional whose least fixed point used to define the reducing semantics: the empty execution, or a run followed by one more step.

Equations

• Relation.starFun X = { toFun := fun (Z : Set (α × ε × α)) => Relation.Idle ∪ Z ∘ᵣ₂ X, monotone' := ⋯ }

theorem Relation.lfp_starFun {α : Type u_1} {ε : Type u_2} [Monoid ε] (X : Set (α × ε × α)) : OrderHom.lfp (starFun X) = star X

step* is what μZ. Id ∪ Z ∘ᵣ₂ step denoted.

theorem Relation.lfp_divFun {α : Type u_1} {ε : Type u_2} [Monoid ε] (X : Set (α × ε × α)) (Y : Set (α × ε)) : OrderHom.lfp (divFun X Y) = star X ∘ᵣ₁ Y

step* ∘ᵣ₁ immediate is what μx. immediate ∪ step ∘ᵣ₁ x denoted. The least fixed point of the functional whose greatest one overshoots. This half needs no hypothesis at all.