Documentation

Mathlib.Control.Fix

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 (α : Type u_1) :
Type u_1
  • fix f represents the computation of a fixed point for f.

    fix : (αα) → α

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

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

    1. fix f = f (fix f) (is a fixed point)
    2. ∀ 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
    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) :
    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.none
    noncomputable instance Part.instFixPart {α : Type u_1} :
    Fix (Part α)
    Equations
    • Part.instFixPart = { fix := fun f => Part.fix (fun x u => f (x u)) () }
    noncomputable instance Pi.Part.hasFix {α : Type u_1} {β : Type u_2} :
    Fix (αPart β)
    Equations
    • Pi.Part.hasFix = { fix := Part.fix }