Lawful fixed point operators
This module defines the laws required of a has_fix instance, using the theory of
omega complete partial orders (ωCPO). Proofs of the lawfulness of all has_fix instances in
control.fix are provided.
Main definition
- class
lawful_fix
@[class]
- to_has_fix : has_fix α
- fix_eq : ∀ {f : α →ₘ α}, omega_complete_partial_order.continuous f → has_fix.fix ⇑f = ⇑f (has_fix.fix ⇑f)
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).
Instances
theorem
lawful_fix.fix_eq'
{α : Type u_1}
[omega_complete_partial_order α]
[lawful_fix α]
{f : α → α}
(hf : omega_complete_partial_order.continuous' f) :
has_fix.fix f = f (has_fix.fix f)
theorem
roption.fix.approx_mono'
{α : Type u_1}
{β : α → Type u_2}
(f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a))
{i : ℕ} :
roption.fix.approx ⇑f i ≤ roption.fix.approx ⇑f i.succ
theorem
roption.fix.approx_mono
{α : Type u_1}
{β : α → Type u_2}
(f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a))
⦃i j : ℕ⦄
(hij : i ≤ j) :
roption.fix.approx ⇑f i ≤ roption.fix.approx ⇑f j
theorem
roption.fix.mem_iff
{α : Type u_1}
{β : α → Type u_2}
(f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a))
(a : α)
(b : β a) :
b ∈ roption.fix ⇑f a ↔ ∃ (i : ℕ), b ∈ roption.fix.approx ⇑f i a
theorem
roption.fix.approx_le_fix
{α : Type u_1}
{β : α → Type u_2}
(f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a))
(i : ℕ) :
roption.fix.approx ⇑f i ≤ roption.fix ⇑f
theorem
roption.fix.exists_fix_le_approx
{α : Type u_1}
{β : α → Type u_2}
(f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a))
(x : α) :
∃ (i : ℕ), roption.fix ⇑f x ≤ roption.fix.approx ⇑f i x
def
roption.fix.approx_chain
{α : Type u_1}
{β : α → Type u_2}
(f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a)) :
omega_complete_partial_order.chain (Π (a : α), roption (β a))
The series of approximations of fix f (see approx) as a chain
Equations
- roption.fix.approx_chain f = {to_fun := roption.fix.approx ⇑f, monotone' := _}
theorem
roption.fix.le_f_of_mem_approx
{α : Type u_1}
{β : α → Type u_2}
(f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a))
{x : Π (a : α), roption (β a)}
(hx : x ∈ roption.fix.approx_chain f) :
theorem
roption.fix.approx_mem_approx_chain
{α : Type u_1}
{β : α → Type u_2}
(f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a))
{i : ℕ} :
theorem
roption.fix_eq_ωSup
{α : Type u_1}
{β : α → Type u_2}
(f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a)) :
theorem
roption.fix_eq
{α : Type u_1}
{β : α → Type u_2}
{f : (Π (a : α), roption (β a)) →ₘ Π (a : α), roption (β a)}
(hc : omega_complete_partial_order.continuous f) :
roption.fix ⇑f = ⇑f (roption.fix ⇑f)
theorem
roption.to_unit_cont
{α : Type u_1}
(f : roption α →ₘ roption α)
(hc : omega_complete_partial_order.continuous f) :
@[instance]
Equations
- roption.lawful_fix = {to_has_fix := roption.has_fix α, fix_eq := _}
@[instance]
Equations
- pi.lawful_fix = {to_has_fix := pi.roption.has_fix β, fix_eq := _}
@[simp]
theorem
pi.monotone_curry_to_fun
(α : 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) :
⇑(pi.monotone_curry α β γ) f x y = sigma.curry f x y
def
pi.monotone_curry
(α : Type u_1)
(β : α → Type u_2)
(γ : Π (a : α), β a → Type u_3)
[Π (x : α) (y : β x), preorder (γ x y)] :
sigma.curry as a monotone function.
Equations
- pi.monotone_curry α β γ = {to_fun := sigma.curry γ, monotone' := _}
def
pi.monotone_uncurry
(α : Type u_1)
(β : α → Type u_2)
(γ : Π (a : α), β a → Type u_3)
[Π (x : α) (y : β x), preorder (γ x y)] :
sigma.uncurry as a monotone function.
Equations
- pi.monotone_uncurry α β γ = {to_fun := sigma.uncurry (λ (a : α) (b : β a), γ a b), monotone' := _}
@[simp]
theorem
pi.monotone_uncurry_to_fun
(α : Type u_1)
(β : α → Type u_2)
(γ : Π (a : α), β a → Type u_3)
[Π (x : α) (y : β x), preorder (γ x y)]
(f : Π (x : α) (y : (λ (a : α), β a) x), (λ (a : α) (b : β a), γ a b) x y)
(x : Σ (a : α), β a) :
⇑(pi.monotone_uncurry α β γ) f x = sigma.uncurry f x
theorem
pi.continuous_curry
(α : Type u_1)
(β : α → Type u_2)
(γ : Π (a : α), β a → Type u_3)
[Π (x : α) (y : β x), omega_complete_partial_order (γ x y)] :
theorem
pi.continuous_uncurry
(α : Type u_1)
(β : α → Type u_2)
(γ : Π (a : α), β a → Type u_3)
[Π (x : α) (y : β x), omega_complete_partial_order (γ x y)] :
@[instance]
def
pi.has_fix
{α : Type u_1}
{β : α → Type u_2}
{γ : Π (a : α), β a → Type u_3}
[has_fix (Π (x : sigma β), γ x.fst x.snd)] :
has_fix (Π (x : α) (y : β x), γ x y)
Equations
- pi.has_fix = {fix := λ (f : (Π (x : α) (y : β x), γ x y) → Π (x : α) (y : β x), γ x y), sigma.curry (has_fix.fix (sigma.uncurry ∘ f ∘ sigma.curry))}
theorem
pi.uncurry_curry_continuous
{α : Type u_1}
{β : α → Type u_2}
{γ : Π (a : α), β a → Type u_3}
[Π (x : α) (y : β x), omega_complete_partial_order (γ x y)]
{f : (Π (x : α) (y : β x), γ x y) →ₘ Π (x : α) (y : β x), γ x y}
(hc : omega_complete_partial_order.continuous f) :
omega_complete_partial_order.continuous ((pi.monotone_uncurry α β γ).comp (f.comp (pi.monotone_curry α β γ)))
@[instance]
def
pi.pi.lawful_fix'
{α : Type u_1}
{β : α → Type u_2}
{γ : Π (a : α), β a → Type u_3}
[Π (x : α) (y : β x), omega_complete_partial_order (γ x y)]
[lawful_fix (Π (x : sigma β), γ x.fst x.snd)] :
lawful_fix (Π (x : α) (y : β x), γ x y)