Lawful fixed point operators

This module defines the laws required of a Fix instance, using the theory of omega complete partial orders (ωCPO). Proofs of the lawfulness of all Fix instances in Control.Fix are provided.

Main definition

• class LawfulFix

class LawfulFix (α : Type u_3) [OmegaCompletePartialOrder α] extends Fix α : Type u_3

Intuitively, a fixed point operator fix is lawful if it satisfies fix f = f (fix f) for all f, but this is inconsistent / uninteresting in most cases due to the existence of "exotic" functions f, such as the function that is defined iff its argument is not, familiar from the halting problem. Instead, this requirement is limited to only functions that are Continuous in the sense of ω-complete partial orders, which excludes the example because it is not monotone (making the input argument less defined can make f more defined).

• fix : (α → α) → α
• fix_eq {f : α → α} : OmegaCompletePartialOrder.ωScottContinuous f → Fix.fix f = f (Fix.fix f)

theorem Part.Fix.approx_mono' {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {i : ℕ} : approx (⇑f) i ≤ approx (⇑f) i.succ

theorem Part.Fix.approx_mono {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) ⦃i j : ℕ⦄ (hij : i ≤ j) : approx (⇑f) i ≤ approx (⇑f) j

theorem Part.Fix.mem_iff {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a) : b ∈ Part.fix (⇑f) a ↔ ∃ (i : ℕ), b ∈ approx (⇑f) i a

theorem Part.Fix.approx_le_fix {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (i : ℕ) : approx (⇑f) i ≤ Part.fix ⇑f

theorem Part.Fix.exists_fix_le_approx {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (x : α) : ∃ (i : ℕ), Part.fix (⇑f) x ≤ approx (⇑f) i x

def Part.Fix.approxChain {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) : OmegaCompletePartialOrder.Chain ((a : α) → Part (β a))

The series of approximations of fix f (see approx) as a Chain

Equations

• Part.Fix.approxChain f = { toFun := Part.Fix.approx ⇑f, monotone' := ⋯ }

theorem Part.Fix.le_f_of_mem_approx {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {x : (a : α) → Part (β a)} : x ∈ approxChain f → x ≤ f x

theorem Part.Fix.approx_mem_approxChain {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {i : ℕ} : approx (⇑f) i ∈ approxChain f

theorem Part.fix_eq_ωSup {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) : Part.fix ⇑f = OmegaCompletePartialOrder.ωSup (Fix.approxChain f)

theorem Part.fix_le {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {X : (a : α) → Part (β a)} (hX : f X ≤ X) : Part.fix ⇑f ≤ X

theorem Part.fix_eq_ωSup_of_ωScottContinuous {α : Type u_1} {β : α → Type u_2} {g : ((a : α) → Part (β a)) → (a : α) → Part (β a)} (hc : OmegaCompletePartialOrder.ωScottContinuous g) : Part.fix g = OmegaCompletePartialOrder.ωSup (Fix.approxChain { toFun := g, monotone' := ⋯ })

theorem Part.fix_eq_of_ωScottContinuous {α : Type u_1} {β : α → Type u_2} {g : ((a : α) → Part (β a)) → (a : α) → Part (β a)} (hc : OmegaCompletePartialOrder.ωScottContinuous g) : Part.fix g = g (Part.fix g)

def Part.toUnitMono {α : Type u_1} (f : Part α →o Part α) : (Unit → Part α) →o Unit → Part α

toUnit as a monotone function

Equations

• Part.toUnitMono f = { toFun := fun (x : Unit → Part α) (u : Unit) => f (x u), monotone' := ⋯ }

@[simp]

theorem Part.toUnitMono_coe {α : Type u_1} (f : Part α →o Part α) (x : Unit → Part α) (u : Unit) : (toUnitMono f) x u = f (x u)

theorem Part.ωScottContinuous_toUnitMono {α : Type u_1} (f : Part α → Part α) (hc : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous ⇑(toUnitMono { toFun := f, monotone' := ⋯ })

noncomputable instance Part.lawfulFix {α : Type u_1} : LawfulFix (Part α)

Equations

• Part.lawfulFix = { toFix := Part.hasFix, fix_eq := ⋯ }

noncomputable instance Pi.lawfulFix {α : Type u_1} {β : Type u_3} : LawfulFix (α → Part β)

Equations

• Pi.lawfulFix = { toFix := Pi.Part.hasFix, fix_eq := ⋯ }

def Pi.monotoneCurry (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3) [(x : α) → (y : β x) → Preorder (γ x y)] : ((x : (a : α) × β a) → γ x.fst x.snd) →o (a : α) → (b : β a) → γ a b

Sigma.curry as a monotone function.

Equations

• Pi.monotoneCurry α β γ = { toFun := Sigma.curry, monotone' := ⋯ }

@[simp]

theorem Pi.monotoneCurry_coe (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3) [(x : α) → (y : β x) → Preorder (γ x y)] (f : (x : (a : α) × β a) → γ x.fst x.snd) (x : α) (y : β x) : (monotoneCurry α β γ) f x y = Sigma.curry f x y

def Pi.monotoneUncurry (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3) [(x : α) → (y : β x) → Preorder (γ x y)] : ((a : α) → (b : β a) → γ a b) →o (x : (a : α) × β a) → γ x.fst x.snd

Sigma.uncurry as a monotone function.

Equations

• Pi.monotoneUncurry α β γ = { toFun := Sigma.uncurry, monotone' := ⋯ }

@[simp]

theorem Pi.monotoneUncurry_coe (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3) [(x : α) → (y : β x) → Preorder (γ x y)] (f : (x : α) → (y : β x) → γ x y) (x : Sigma β) : (monotoneUncurry α β γ) f x = Sigma.uncurry f x

theorem Pi.ωScottContinuous_curry (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3) [(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)] : OmegaCompletePartialOrder.ωScottContinuous ⇑(monotoneCurry α β γ)

theorem Pi.ωScottContinuous_uncurry (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3) [(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)] : OmegaCompletePartialOrder.ωScottContinuous ⇑(monotoneUncurry α β γ)

instance Pi.hasFix {α : Type u_1} {β : α → Type u_2} {γ : (a : α) → β a → Type u_3} [Fix ((x : Sigma β) → γ x.fst x.snd)] : Fix ((x : α) → (y : β x) → γ x y)

Equations

• Pi.hasFix = { fix := fun (f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y) => Sigma.curry (Fix.fix (Sigma.uncurry ∘ f ∘ Sigma.curry)) }

theorem Pi.uncurry_curry_ωScottContinuous {α : Type u_1} {β : α → Type u_2} {γ : (a : α) → β a → Type u_3} [(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)] {f : ((a : α) → (b : β a) → γ a b) → (a : α) → (b : β a) → γ a b} (hc : OmegaCompletePartialOrder.ωScottContinuous f) : OmegaCompletePartialOrder.ωScottContinuous ⇑((monotoneUncurry α β γ).comp ({ toFun := f, monotone' := ⋯ }.comp (monotoneCurry α β γ)))

instance Pi.lawfulFix' {α : Type u_1} {β : α → Type u_2} {γ : (a : α) → β a → Type u_3} [(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)] [LawfulFix ((x : Sigma β) → γ x.fst x.snd)] : LawfulFix ((x : α) → (y : β x) → γ x y)

Equations

• Pi.lawfulFix' = { toFix := Pi.hasFix, fix_eq := ⋯ }