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 #
def
Part.Fix.approx
{α : Type u_1}
{β : α → Type u_2}
(f : ((a : α) → Part (β a)) → (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 => g (Nat.Upto.succ i h) (_ : ↑i < Nat.succ ↑i) x
noncomputable 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:
fix f = f (fix f)
(is a fixed point)∀ X, f X ≤ X → fix f ≤ X∀ X, f X ≤ X → fix f ≤ X≤ X → fix f ≤ X→ fix f ≤ X≤ X
(least fixed point)
Equations
- Part.fix f x = Part.assert (∃ i, (Part.Fix.approx f i x).Dom) fun h => WellFounded.fix (_ : WellFounded (Nat.Upto.GT fun x => (Part.Fix.approx f x x).Dom)) (Part.fixAux f) Nat.Upto.zero x
theorem
Part.fix_def
{α : Type u_2}
{β : α → Type u_1}
(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