Fixed point #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
has_fix α gives us a way to calculate the fixed point
of function of type α → α.
Instances of this typeclass
Instances of other typeclasses for has_fix
- has_fix.has_sizeof_inst
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 i.succ = f (part.fix.approx f i)
- part.fix.approx f 0 = ⊥
def
part.fix_aux
{α : 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.fix_aux f i g = f (λ (x : α), part.assert (¬p i.val) (λ (h : ¬p i.val), g (i.succ h) _ x))
@[protected]
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(least fixed point)
Equations
- part.fix f x = part.assert (∃ (i : ℕ), (part.fix.approx f i x).dom) (λ (h : ∃ (i : ℕ), (part.fix.approx f i x).dom), _.fix (part.fix_aux f) nat.upto.zero x)