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 roption.

Main definition

class has_fix
roption.fix

source

@[class]

structure has_fix (α : Type u_3) :

Type u_3

fix : (α → α) → α

has_fix α gives us a way to calculate the fixed point of function of type α → α.

Instances

source

def roption.fix.approx {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), roption (β a)) → Π (a : α), roption (β a)) :

stream (Π (a : α), roption (β 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

roption.fix.approx f i.succ = f (roption.fix.approx f i)
roption.fix.approx f 0 = ⊥

source

def roption.fix_aux {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), roption (β a)) → Π (a : α), roption (β a)) {p : ℕ → Prop} (i : nat.upto p) (g : Π (j : nat.upto p), i < j → Π (a : α), roption (β a)) (a : α) :

roption (β a)

loop body for finding the fixed point of f

Equations

roption.fix_aux f i g = f (λ (x : α), roption.assert (¬p i.val) (λ (h : ¬p i.val), g (i.succ h) _ x))

source

def roption.fix {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), roption (β a)) → Π (a : α), roption (β a)) (x : α) :

roption (β 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

roption.fix f x = roption.assert (∃ (i : ℕ), (roption.fix.approx f i x).dom) (λ (h : ∃ (i : ℕ), (roption.fix.approx f i x).dom), _.fix (roption.fix_aux f) nat.upto.zero x)

source

theorem roption.fix_def {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), roption (β a)) → Π (a : α), roption (β a)) {x : α} (h' : ∃ (i : ℕ), (roption.fix.approx f i x).dom) :

roption.fix f x = roption.fix.approx f (nat.find h').succ x

source

theorem roption.fix_def' {α : Type u_1} {β : α → Type u_2} (f : (Π (a : α), roption (β a)) → Π (a : α), roption (β a)) {x : α} (h' : ¬∃ (i : ℕ), (roption.fix.approx f i x).dom) :

roption.fix f x = roption.none

source

@[instance]

def roption.has_fix {α : Type u_1} :

has_fix (roption α)

Equations

roption.has_fix = {fix := λ (f : roption α → roption α), roption.fix (λ (x : unit → roption α) (u : unit), f (x u)) ()}

source

@[instance]

def pi.roption.has_fix {α : Type u_1} {β : Type u_2} :

has_fix (α → roption β)

Equations

pi.roption.has_fix = {fix := roption.fix (λ (a : α), β)}