control.fix

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
• part.fix
@[class]
structure has_fix (α : Type u_3) :
Type u_3

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)) :
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
• = f i)
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
@[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:

1. fix f = f (fix f) (is a fixed point)
2. ∀ X, f X ≤ X → fix f ≤ X (least fixed point)
Equations
@[protected]
theorem part.fix_def {α : Type u_1} {β : α Type u_2} (f : (Π (a : α), part (β a)) Π (a : α), part (β a)) {x : α} (h' : (i : ), i x).dom) :
x = (nat.find h').succ x
theorem part.fix_def' {α : Type u_1} {β : α Type u_2} (f : (Π (a : α), part (β a)) Π (a : α), part (β a)) {x : α} (h' : ¬ (i : ), i x).dom) :
@[protected, instance]
def part.has_fix {α : Type u_1} :
Equations
@[protected, instance]
def pi.part.has_fix {α : Type u_1} {β : Type u_2} :
has_fix part β)
Equations