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 #
- class
omega_complete_partial_order
ite
,map
,bind
,seq
as continuous morphisms
Instances of omega_complete_partial_order
#
part
- every
complete_lattice
- pi-types
- product types
monotone_hom
continuous_hom
(with notation →𝒄)- an instance of
omega_complete_partial_order (α →𝒄 β)
- an instance of
continuous_hom.of_fun
continuous_hom.of_mono
- continuous functions:
References #
A chain is a monotone sequence.
See the definition on page 114 of [Gun92].
Equations
Instances for omega_complete_partial_order.chain
Equations
Equations
- omega_complete_partial_order.chain.has_le = {le := λ (x y : omega_complete_partial_order.chain α), ∀ (i : ℕ), ∃ (j : ℕ), ⇑x i ≤ ⇑y j}
map
function for chain
chain.zip
pairs up the elements of two chains that have the same index
Equations
- c₀.zip c₁ = order_hom.prod c₀ c₁
- to_partial_order : partial_order α
- ωSup : omega_complete_partial_order.chain α → α
- le_ωSup : ∀ (c : omega_complete_partial_order.chain α) (i : ℕ), ⇑c i ≤ omega_complete_partial_order.ωSup c
- ωSup_le : ∀ (c : omega_complete_partial_order.chain α) (x : α), (∀ (i : ℕ), ⇑c i ≤ x) → omega_complete_partial_order.ωSup c ≤ x
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 of this typeclass
- complete_lattice.omega_complete_partial_order
- part.omega_complete_partial_order
- pi.omega_complete_partial_order
- prod.omega_complete_partial_order
- omega_complete_partial_order.order_hom.omega_complete_partial_order
- omega_complete_partial_order.continuous_hom.omega_complete_partial_order
- ωCPO.omega_complete_partial_order
- ωCPO.omega_complete_partial_order_equalizer
Instances of other typeclasses for omega_complete_partial_order
- omega_complete_partial_order.has_sizeof_inst
Transfer a omega_complete_partial_order
on β
to a omega_complete_partial_order
on α
using a strictly monotone function f : β →o α
, a definition of ωSup and a proof that f
is
continuous with regard to the provided ωSup
and the ωCPO on α
.
Equations
- omega_complete_partial_order.lift f ωSup₀ h h' = {to_partial_order := _inst_2, ωSup := ωSup₀, le_ωSup := _, ωSup_le := _}
A subset p : α → Prop
of the type closed under ωSup
induces an
omega_complete_partial_order
on the subtype {a : α // p a}
.
Equations
- omega_complete_partial_order.subtype p hp = omega_complete_partial_order.lift (order_hom.subtype.val p) (λ (c : omega_complete_partial_order.chain (subtype p)), ⟨omega_complete_partial_order.ωSup (c.map (order_hom.subtype.val p)), _⟩) _ _
A monotone function f : α →o β
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
continuous' f
asserts that f
is both monotone and continuous.
Equations
- omega_complete_partial_order.continuous' f = ∃ (hf : monotone f), omega_complete_partial_order.continuous {to_fun := f, monotone' := hf}
The (noncomputable) ωSup
definition for the ω
-CPO structure on part α
.
Equations
- part.omega_complete_partial_order = {to_partial_order := part.partial_order α, ωSup := part.ωSup α, le_ωSup := _, ωSup_le := _}
Equations
- pi.omega_complete_partial_order = {to_partial_order := pi.partial_order (λ (i : α), omega_complete_partial_order.to_partial_order), ωSup := λ (c : omega_complete_partial_order.chain (Π (a : α), β a)) (a : α), omega_complete_partial_order.ωSup (c.map (pi.eval_order_hom a)), le_ωSup := _, ωSup_le := _}
The supremum of a chain in the product ω
-CPO.
Equations
Equations
- prod.omega_complete_partial_order = {to_partial_order := prod.partial_order α β omega_complete_partial_order.to_partial_order, ωSup := prod.ωSup _inst_2, le_ωSup := _, ωSup_le := _}
Any complete lattice has an ω
-CPO structure where the countable supremum is a special case
of arbitrary suprema.
Equations
- complete_lattice.omega_complete_partial_order α = {to_partial_order := complete_semilattice_Inf.to_partial_order α (complete_lattice.to_complete_semilattice_Inf α), ωSup := λ (c : omega_complete_partial_order.chain α), ⨆ (i : ℕ), ⇑c i, le_ωSup := _, ωSup_le := _}
The ωSup
operator for monotone functions.
Equations
- omega_complete_partial_order.order_hom.ωSup c = {to_fun := λ (a : α), omega_complete_partial_order.ωSup (c.map (order_hom.apply a)), monotone' := _}
Equations
- omega_complete_partial_order.order_hom.omega_complete_partial_order = omega_complete_partial_order.lift order_hom.coe_fn_hom omega_complete_partial_order.order_hom.ωSup omega_complete_partial_order.order_hom.omega_complete_partial_order._proof_1 omega_complete_partial_order.order_hom.omega_complete_partial_order._proof_2
- to_order_hom : α →o β
- cont : omega_complete_partial_order.continuous {to_fun := self.to_order_hom.to_fun, monotone' := _}
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 order_hom.continuous
.
Instances for omega_complete_partial_order.continuous_hom
- omega_complete_partial_order.continuous_hom.has_sizeof_inst
- omega_complete_partial_order.continuous_hom.has_coe_to_fun
- omega_complete_partial_order.order_hom.has_coe
- omega_complete_partial_order.continuous_hom.partial_order
- omega_complete_partial_order.continuous_hom.inhabited
- omega_complete_partial_order.continuous_hom.omega_complete_partial_order
- ωCPO.omega_complete_partial_order.continuous_hom.category_theory.bundled_hom
Equations
- omega_complete_partial_order.continuous_hom.has_coe_to_fun α β = {coe := λ (f : α →𝒄 β), f.to_order_hom.to_fun}
Equations
Equations
- omega_complete_partial_order.continuous_hom.partial_order α β = partial_order.lift (λ (f : α →𝒄 β), f.to_order_hom.to_fun) _
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
Construct a continuous function from a bare function, a continuous function, and a proof that they are equal.
Equations
- omega_complete_partial_order.continuous_hom.of_fun f g h = {to_order_hom := {to_fun := f, monotone' := _}, cont := _}
Construct a continuous function from a monotone function with a proof of continuity.
Equations
- omega_complete_partial_order.continuous_hom.of_mono f h = {to_order_hom := {to_fun := ⇑f, monotone' := _}, cont := h}
The identity as a continuous function.
The composition of continuous functions.
function.const
is a continuous function.
The map from continuous functions to monotone functions is itself a monotone function.
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.
The ωSup
operator for continuous functions, which takes the pointwise countable supremum
of the functions in the ω
-chain.
Equations
- omega_complete_partial_order.continuous_hom.omega_complete_partial_order = omega_complete_partial_order.lift omega_complete_partial_order.continuous_hom.to_mono omega_complete_partial_order.continuous_hom.ωSup omega_complete_partial_order.continuous_hom.omega_complete_partial_order._proof_1 omega_complete_partial_order.continuous_hom.omega_complete_partial_order._proof_2
The application of continuous functions as a continuous function.
A family of continuous functions yields a continuous family of functions.
Equations
- omega_complete_partial_order.continuous_hom.flip f = {to_order_hom := {to_fun := λ (x : β) (y : α), ⇑(f y) x, monotone' := _}, cont := _}
part.bind
as a continuous function.
part.map
as a continuous function.
Equations
part.seq
as a continuous function.
Equations
- f.seq g = omega_complete_partial_order.continuous_hom.of_fun (λ (x : α), ⇑f x <*> ⇑g x) (f.bind (omega_complete_partial_order.continuous_hom.flip (flip omega_complete_partial_order.continuous_hom.map g))) _