mathlib documentation

order.omega_complete_partial_order

Omega Complete Partial Orders #

An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

The concept of an omega-complete partial order (ωCPO) is useful for the formalization of the semantics of programming languages. Its notion of supremum helps define the meaning of recursive procedures.

Main definitions #

Instances of omega_complete_partial_order #

References #

def preorder_hom.bind {α : Type u_1} [preorder α] {β γ : Type u_2} (f : α →ₘ part β) (g : α →ₘ β → part γ) :
α →ₘ part γ

part.bind as a monotone function

Equations
@[simp]
theorem preorder_hom.bind_coe {α : Type u_1} [preorder α] {β γ : Type u_2} (f : α →ₘ part β) (g : α →ₘ β → part γ) (x : α) :
(f.bind g) x = f x >>= g x
def omega_complete_partial_order.chain (α : Type u) [preorder α] :
Type u

A chain is a monotone sequence.

See the definition on page 114 of [Gun92].

Equations
@[instance]
Equations

map function for chain

Equations
@[simp]
theorem omega_complete_partial_order.chain.map_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) (f : α →ₘ β) :
(c.map f) = f c
theorem omega_complete_partial_order.chain.mem_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f : α →ₘ β} (x : α) :
x cf x c.map f
theorem omega_complete_partial_order.chain.exists_of_mem_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f : α →ₘ β} {b : β} :
b c.map f(∃ (a : α), a c f a = b)
theorem omega_complete_partial_order.chain.mem_map_iff {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f : α →ₘ β} {b : β} :
b c.map f ∃ (a : α), a c f a = b
theorem omega_complete_partial_order.chain.map_comp {α : Type u} {β : Type v} {γ : Type u_1} [preorder α] [preorder β] [preorder γ] (c : omega_complete_partial_order.chain α) {f : α →ₘ β} (g : β →ₘ γ) :
(c.map f).map g = c.map (g.comp f)
theorem omega_complete_partial_order.chain.map_le_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f g : α →ₘ β} (h : f g) :
c.map f c.map g

chain.zip pairs up the elements of two chains that have the same index

Equations
@[simp]
theorem omega_complete_partial_order.chain.zip_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (c₀ : omega_complete_partial_order.chain α) (c₁ : omega_complete_partial_order.chain β) (x : ) :
(c₀.zip c₁) x = (c₀ x, c₁ x)
@[class]
structure omega_complete_partial_order (α : Type u_1) :
Type u_1

An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

See the definition on page 114 of [Gun92].

Instances
def omega_complete_partial_order.lift {α : Type u} {β : Type v} [omega_complete_partial_order α] [partial_order β] (f : β →ₘ α) (ωSup₀ : omega_complete_partial_order.chain β → β) (h : ∀ (x y : β), f x f yx y) (h' : ∀ (c : omega_complete_partial_order.chain β), f (ωSup₀ c) = omega_complete_partial_order.ωSup (c.map f)) :

Transfer a omega_complete_partial_order on β to a omega_complete_partial_order on α using a strictly monotone function f : β →ₘ α, a definition of ωSup and a proof that f is continuous with regard to the provided ωSup and the ωCPO on α.

Equations
def omega_complete_partial_order.subtype {α : Type u_1} [omega_complete_partial_order α] (p : α → Prop) (hp : ∀ (c : omega_complete_partial_order.chain α), (∀ (i : α), i cp i)p (omega_complete_partial_order.ωSup c)) :

A subset p : α → Prop of the type closed under ωSup induces an omega_complete_partial_order on the subtype {a : α // p a}.

Equations

A monotone function f : α →ₘ β is continuous if it distributes over ωSup.

In order to distinguish it from the (more commonly used) continuity from topology (see topology/basic.lean), the present definition is often referred to as "Scott-continuity" (referring to Dana Scott). It corresponds to continuity in Scott topological spaces (not defined here).

Equations
def omega_complete_partial_order.continuous' {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) :
Prop

continuous' f asserts that f is both monotone and continuous.

Equations
theorem part.eq_of_chain {α : Type u} {c : omega_complete_partial_order.chain (part α)} {a b : α} (ha : part.some a c) (hb : part.some b c) :
a = b
def part.ωSup {α : Type u} (c : omega_complete_partial_order.chain (part α)) :
part α

The (noncomputable) ωSup definition for the ω-CPO structure on part α.

Equations
theorem part.ωSup_eq_some {α : Type u} {c : omega_complete_partial_order.chain (part α)} {a : α} (h : part.some a c) :
theorem part.ωSup_eq_none {α : Type u} {c : omega_complete_partial_order.chain (part α)} (h : ¬∃ (a : α), part.some a c) :
theorem part.mem_chain_of_mem_ωSup {α : Type u} {c : omega_complete_partial_order.chain (part α)} {a : α} (h : a part.ωSup c) :
theorem pi.omega_complete_partial_order.flip₁_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [Π (x : α), omega_complete_partial_order (β x)] [omega_complete_partial_order γ] (f : Π (x : α), γ → β x) (a : α) (hf : omega_complete_partial_order.continuous' (λ (x : γ) (y : α), f y x)) :
theorem pi.omega_complete_partial_order.flip₂_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [Π (x : α), omega_complete_partial_order (β x)] [omega_complete_partial_order γ] (f : γ → Π (x : α), β x) (hf : ∀ (x : α), omega_complete_partial_order.continuous' (λ (g : γ), f g x)) :
def prod.ωSup {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (c : omega_complete_partial_order.chain × β)) :
α × β

The supremum of a chain in the product ω-CPO.

Equations
@[instance]

Any complete lattice has an ω-CPO structure where the countable supremum is a special case of arbitrary suprema.

Equations
theorem complete_lattice.supr_continuous {α : Type u} {β : Type v} [omega_complete_partial_order α] [complete_lattice β] {ι : Sort u_1} {f : ι → α →ₘ β} (h : ∀ (i : ι), omega_complete_partial_order.continuous (f i)) :
theorem complete_lattice.Sup_continuous' {α : Type u} {β : Type v} [omega_complete_partial_order α] [complete_lattice β] (s : set (α → β)) (hc : ∀ (f : α → β), f somega_complete_partial_order.continuous' f) :
@[instance]
Equations
structure omega_complete_partial_order.continuous_hom (α : Type u) (β : Type v) [omega_complete_partial_order α] [omega_complete_partial_order β] :
Type (max u v)

A monotone function on ω-continuous partial orders is said to be continuous if for every chain c : chain α, f (⊔ i, c i) = ⊔ i, f (c i). This is just the bundled version of preorder_hom.continuous.

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
theorem omega_complete_partial_order.continuous_hom.congr_fun {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] {f g : α →𝒄 β} (h : f = g) (x : α) :
f x = g x
theorem omega_complete_partial_order.continuous_hom.congr_arg {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α →𝒄 β) {x y : α} (h : x = y) :
f x = f y
theorem omega_complete_partial_order.continuous_hom.apply_mono {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] {f g : α →𝒄 β} {x y : α} (h₁ : f g) (h₂ : x y) :
f x g y
def omega_complete_partial_order.continuous_hom.of_fun {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) (g : α →𝒄 β) (h : f = g) :
α →𝒄 β

Construct a continuous function from a bare function, a continuous function, and a proof that they are equal.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.of_fun_apply {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) (g : α →𝒄 β) (h : f = g) (ᾰ : α) :

Construct a continuous function from a monotone function with a proof of continuity.

Equations
def omega_complete_partial_order.continuous_hom.comp {α : Type u} {β : Type v} {γ : Type u_3} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] (f : β →𝒄 γ) (g : α →𝒄 β) :
α →𝒄 γ

The composition of continuous functions.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.comp_apply {α : Type u} {β : Type v} {γ : Type u_3} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] (f : β →𝒄 γ) (g : α →𝒄 β) (ᾰ : α) :
(f.comp g) = f (g ᾰ)
@[ext]
theorem omega_complete_partial_order.continuous_hom.ext {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) (h : ∀ (x : α), f x = g x) :
f = g
@[simp]
theorem omega_complete_partial_order.continuous_hom.comp_assoc {α : Type u} {β : Type v} {γ : Type u_3} {φ : Type u_4} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] [omega_complete_partial_order φ] (f : γ →𝒄 φ) (g : β →𝒄 γ) (h : α →𝒄 β) :
f.comp (g.comp h) = (f.comp g).comp h
@[simp]
theorem omega_complete_partial_order.continuous_hom.coe_apply {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (a : α) (f : α →𝒄 β) :
f a = f a

The application of continuous functions as a monotone function.

(It would make sense to make it a continuous function, but we are currently constructing a omega_complete_partial_order instance for α →𝒄 β, and we cannot use it as the domain or image of a continuous function before we do.)

Equations

The map from continuous functions to monotone functions is itself a monotone function.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.forall_forall_merge {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (c₀ : omega_complete_partial_order.chain →𝒄 β)) (c₁ : omega_complete_partial_order.chain α) (z : β) :
(∀ (i j : ), (c₀ i) (c₁ j) z) ∀ (i : ), (c₀ i) (c₁ i) z

When proving that a chain of applications is below a bound z, it suffices to consider the functions and values being selected from the same index in the chains.

This lemma is more specific than necessary, i.e. c₀ only needs to be a chain of monotone functions, but it is only used with continuous functions.

@[simp]
theorem omega_complete_partial_order.continuous_hom.forall_forall_merge' {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (c₀ : omega_complete_partial_order.chain →𝒄 β)) (c₁ : omega_complete_partial_order.chain α) (z : β) :
(∀ (j i : ), (c₀ i) (c₁ j) z) ∀ (i : ), (c₀ i) (c₁ i) z
@[instance]
Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.flip_apply {β : Type v} {γ : Type u_3} [omega_complete_partial_order β] [omega_complete_partial_order γ] {α : Type u_1} (f : α → β →𝒄 γ) (x : β) (y : α) :
def omega_complete_partial_order.continuous_hom.flip {β : Type v} {γ : Type u_3} [omega_complete_partial_order β] [omega_complete_partial_order γ] {α : Type u_1} (f : α → β →𝒄 γ) :
β →𝒄 α → γ

A family of continuous functions yields a continuous family of functions.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.bind_apply {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : α →𝒄 part β) (g : α →𝒄 β → part γ) (ᾰ : α) :
(f.bind g) = (f.bind g)
def omega_complete_partial_order.continuous_hom.bind {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : α →𝒄 part β) (g : α →𝒄 β → part γ) :

part.bind as a continuous function.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.map_apply {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : β → γ) (g : α →𝒄 part β) (x : α) :
@[simp]
theorem omega_complete_partial_order.continuous_hom.seq_apply {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : α →𝒄 part (β → γ)) (g : α →𝒄 part β) (x : α) :
(f.seq g) x = f x <*> g x