Interval Domain

definition example

The interval domain $\mathbb{IR}$ is the Topological Space whose points are the finite closed intervals

$$\mathbb{IR}:=\{[d,u]\subseteq \mathbb{R}\mid d\le u\},$$

with topology generated by the basic open sets $o_{[a,b]}:=\{[d,u]\in \mathbb{IR}\mid a<d\le u<b\}$ for $a<b$: a subset is open iff it is a union of basic opens. Sheaves on $\mathbb{IR}$ are the behavior types.

Sources: 7 Sketches §7.5.1, Exercises 7.76, 7.77; §7.5.2; §7.6 (domain theory, [Gie+03], [AJ94]).

• $o_{[0,5]}$ contains every interval inside $(0,5)$. Note $o_{[0,5]}\cup o_{[4,8]}\ne o_{[0,8]}$: the interval $[2,6]$ lies in the right-hand side but in neither piece of the left (7S Exercise 7.76). This is exactly why $\mathbb{IR}$, not $\mathbb{R}$, is the right site for statements that take time to evaluate: “the stock market did not drop more than 10 points” can be true on $(0,5)$ and on $(4,8)$ without being true on $(0,8)$.
• $\mathbb{R}$ embeds as the subspace $\{[d,u]\mid d=u\}$, and the subspace topology agrees with the usual one on $\mathbb{R}$ (7S Exercise 7.77): $o_{[a,b]}\cap \mathbb{R}=(a,b)$.
• A sheaf $S$ on $\mathbb{IR}$ is determined by its values on basic opens, and these vary continuously: $S(o_{[a,b]})\cong {\lim }_{ϵ>0}S(o_{[a-ϵ,b+ϵ]})$.
• The name comes from domain theory (Dana Scott): intervals ordered by reverse inclusion form a continuous domain whose Scott topology this is.

JuliaLeanHaskell

Docs: plain Julia — Catlab has no dedicated API for this; related: Catlab v0.16 docs · GATlab standard library

# points of 𝕀ℝ as pairs (d, u), basic opens as predicates
struct Interval; d::Float64; u::Float64; end
basic(a, b) = I -> a < I.d <= I.u < b        # o_[a,b]
I = Interval(2, 6)
basic(0, 8)(I)                               # true
basic(0, 5)(I) || basic(4, 8)(I)             # false: o_[0,5] ∪ o_[4,8] ≠ o_[0,8]

import Mathlib
-- Mathlib has no interval domain; nonempty compact intervals can be modelled as
example : Type := { p : ℝ × ℝ // p.1 ≤ p.2 }
#check @TopologicalSpace.generateFrom       -- topology generated by the basic opens o_[a,b]
#check @Set.Icc

data Interval = Interval { lo :: Double, hi :: Double }
basicOpen :: Double -> Double -> Interval -> Bool
basicOpen a b (Interval d u) = a < d && d <= u && u < b
-- basicOpen 0 8 (Interval 2 6) == True; basicOpen 0 5 i || basicOpen 4 8 i == False