Fixed point

This module defines a generic fix operator for defining recursive computations that are not necessarily well-founded or productive. An instance is defined for Part.

Main definition

• class Fix
• Part.fix

class Fix (α : Type u_3) : Type u_3

Fix α provides a fix operator to define recursive computation via the fixed point of function of type α → α.

• fix : (α → α) → α

  fix f represents the computation of a fixed point for f.

def Part.Fix.approx {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) : Stream' ((a : α) → Part (β a))

A series of successive, finite approximation of the fixed point of f, defined by approx f n = f^[n] ⊥. The limit of this chain is the fixed point of f.

Equations

• Part.Fix.approx f 0 = ⊥
• Part.Fix.approx f (Nat.succ i) = f (Part.Fix.approx f i)

def Part.fixAux {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) {p : ℕ → Prop} (i : Nat.Upto p) (g : (j : Nat.Upto p) → i < j → (a : α) → Part (β a)) (a : α) : Part (β a)

loop body for finding the fixed point of f

Equations

• Part.fixAux f i g = f fun (x : α) => Part.assert (¬p ↑i) fun (h : ¬p ↑i) => g (Nat.Upto.succ i h) ⋯ x

def Part.fix {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) (x : α) : Part (β x)

The least fixed point of f.

If f is a continuous function (according to complete partial orders), it satisfies the equations:

1. fix f = f (fix f) (is a fixed point)
2. ∀ X, f X ≤ X → fix f ≤ X (least fixed point)

Equations

• Part.fix f x = Part.assert (∃ (i : ℕ), (Part.Fix.approx f i x).Dom) fun (h : ∃ (i : ℕ), (Part.Fix.approx f i x).Dom) => WellFounded.fix ⋯ (Part.fixAux f) Nat.Upto.zero x

theorem Part.fix_def {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) {x : α} (h' : ∃ (i : ℕ), (Part.Fix.approx f i x).Dom) : Part.fix f x = Part.Fix.approx f (Nat.succ (Nat.find h')) x

theorem Part.fix_def' {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) {x : α} (h' : ¬∃ (i : ℕ), (Part.Fix.approx f i x).Dom) : Part.fix f x = Part.none

instance Part.hasFix {α : Type u_1} : Fix (Part α)

Equations

• Part.hasFix = { fix := fun (f : Part α → Part α) => Part.fix (fun (x : Unit → Part α) (u : Unit) => f (x u)) () }

instance Pi.Part.hasFix {α : Type u_1} {β : Type u_3} : Fix (α → Part β)

Equations

• Pi.Part.hasFix = { fix := Part.fix }