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)
Instances For
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)
: