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
• Part.fix
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
• = f ()
def Part.fixAux {α : Type u_1} {β : αType u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) {p : } (i : ) (g : (j : ) → 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, ().Dom) :
theorem Part.fix_def' {α : Type u_2} {β : αType u_1} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) {x : α} (h' : ¬i, ().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 }