We derive from a given section-retraction List α → α the combinatory algebra structure on Set α.

class Listing (α : Type) : Type

An encoding of lists of α's as α.

• fromList : List α → α
• toList : α → List α
• eq_list : ∀ (xs : List α), Listing.toList (Listing.fromList xs) = xs

instance Listing.inhabited {α : Type} [Listing α] : Inhabited α

A set equipped with Listing has as its canonical element the encoding of [].

Equations

• Listing.inhabited = { default := Listing.fromList [] }

@[reducible]

def toSet {α : Type} [Listing α] (x : α) : Set α

[x] qua subset of elements listed by x.

Equations

• toSet x a = List.Mem a (Listing.toList x)

@[simp]

theorem eq_toSet_fromList {α : Type} [Listing α] {ys : List α} : toSet (Listing.fromList ys) = fun (a : α) => List.Mem a ys

def Listing.pair {α : Type} [Listing α] (x y : α) : α

We encode pairs as lists of length two.

Equations

• Listing.pair x y = Listing.fromList [x, y]

def Listing.fst {α : Type} [Listing α] (x : α) : α

The first projection from a pair.

Equations

• Listing.fst x = (Listing.toList x).head!

def Listing.snd {α : Type} [Listing α] (x : α) : α

The second projection from a pair.

Equations

• Listing.snd x = (Listing.toList x).get! 1

theorem Listing.eq_fst_pair {α : Type} [Listing α] (x y : α) : Listing.fst (Listing.pair x y) = x

Computation rule for the first projection from a pair.

theorem Listing.eq_snd_pair {α : Type} [Listing α] (x y : α) : Listing.snd (Listing.pair x y) = y

Computation rule for the second projection from a pair.

def GraphModel.continuous {α : Type} [Listing α] (f : Set α → Set α) : Prop

A map Set α → Set α is continuous when its values are determined on finite subsets. This is continuity in the sense of Scott topology, but we avoid developing a general theory of domains, so we will specialize all definitions to the situation at hand.

Equations

• GraphModel.continuous f = ∀ (S : Set α) (x : α), x ∈ f S ↔ ∃ (y : α), toSet y ⊆ S ∧ x ∈ f (toSet y)

def GraphModel.monotone {α : Type} (f : Set α → Set α) : Prop

Monotonicity of a map Set α → Set α with respect to subset inclusion.

Equations

• GraphModel.monotone f = ∀ (S T : Set α), S ⊆ T → f S ⊆ f T

theorem GraphModel.continuous_monotone {α : Type} [Listing α] {f : Set α → Set α} : GraphModel.continuous f → GraphModel.monotone f

A continuous map is monotone

def GraphModel.continuous₂ {α : Type} [Listing α] (f : Set α → Set α → Set α) : Prop

Continuity of a binary map

Equations

• GraphModel.continuous₂ f = ∀ (S T : Set α) (x : α), x ∈ f S T ↔ ∃ (y : α) (z : α), toSet y ⊆ S ∧ toSet z ⊆ T ∧ x ∈ f (toSet y) (toSet z)

def GraphModel.monotone₂ {α : Type} (f : Set α → Set α → Set α) : Prop

Monotonicity of a binary map.

Equations

• GraphModel.monotone₂ f = ∀ (S S' T T' : Set α), S ⊆ S' → T ⊆ T' → f S T ⊆ f S' T'

theorem GraphModel.continuous₂_monotone₂ {α : Type} [Listing α] {f : Set α → Set α → Set α} : GraphModel.continuous₂ f → GraphModel.monotone₂ f

A continuous binary map is monotone.

theorem GraphModel.continuous₂_separately {α : Type} [Listing α] (f : Set α → Set α → Set α) : (∀ (S : Set α), GraphModel.continuous (f S)) → (∀ (T : Set α), GraphModel.continuous fun (S : Set α) => f S T) → GraphModel.continuous₂ f

If a binary map is continuous in each arguments separately, then it is continuous.

theorem GraphModel.continuous₂_fst {α : Type} [Listing α] (h : Set α → Set α → Set α) : GraphModel.continuous₂ h → ∀ (S : Set α), GraphModel.continuous (h S)

A continuous binary map is continuous as a map of its first argument

theorem GraphModel.continuous₂_snd {α : Type} [Listing α] (h : Set α → Set α → Set α) : GraphModel.continuous₂ h → ∀ (T : Set α), GraphModel.continuous fun (S : Set α) => h S T

A continuous binary map is contunuous as a map of its second argument

def GraphModel.continuous_id {α : Type} [Listing α] : GraphModel.continuous id

The identity map is continuous.

Equations

• ⋯ = ⋯

def GraphModel.continuous_const {α : Type} [Listing α] (T : Set α) : GraphModel.continuous fun (x : Set α) => T

A constant map is continuous.

Equations

• ⋯ = ⋯

theorem GraphModel.continuous_finite {α : Type} [Listing α] {f : Set α → Set α} (ys : List α) (S : Set α) : GraphModel.continuous f → (∀ y ∈ ys, y ∈ f S) → ∃ (z : α), toSet z ⊆ S ∧ ∀ y ∈ ys, y ∈ f (toSet z)

If f is continuous then any finite subset of f S is already a subset of some f S' where S' ⊆ S is finite (in the statement S' is toSet z). The lemma is used in the theorem showing that composition preserves continuity.

theorem GraphModel.continuous_compose {α : Type} [Listing α] (f g : Set α → Set α) : GraphModel.continuous f → GraphModel.continuous g → GraphModel.continuous (f ∘ g)

The composition of continuous maps is continuous.

theorem GraphModel.continuous₂_compose {α : Type} [Listing α] (f g : Set α → Set α) (h : Set α → Set α → Set α) : GraphModel.continuous f → GraphModel.continuous g → GraphModel.continuous₂ h → GraphModel.continuous fun (U : Set α) => h (f U) (g U)

The composition of a binary continuous map and continuous maps is continuous.

def GraphModel.graph {α : Type} [Listing α] (f : Set α → Set α) : Set α

The graph of a function

Equations

• GraphModel.graph f x = (Listing.fst x ∈ f (toSet (Listing.snd x)))

def GraphModel.continuous_graph {α : Type} [Listing α] (f : Set α → Set α → Set α) : GraphModel.continuous₂ f → GraphModel.continuous fun (S : Set α) => GraphModel.graph (f S)

Currying combined with graph is continuous

Equations

• ⋯ = ⋯

def GraphModel.apply {α : Type} [Listing α] (S : Set α) : Set α → Set α

Combinatory application on the graph model

Equations

• GraphModel.apply S T x = ∃ (y : α), toSet y ⊆ T ∧ Listing.pair x y ∈ S

@[reducible]

instance GraphModel.Listing.hasDot {α : Type} [Listing α] : HasDot (Set α)

Equations

• GraphModel.Listing.hasDot = { dot := GraphModel.apply }

theorem GraphModel.apply.monotone₂ {α : Type} [Listing α] : GraphModel.monotone₂ GraphModel.apply

Application is monotone.

theorem GraphModel.apply.monotone_fst {α : Type} [Listing α] {T : Set α} : GraphModel.monotone fun (S : Set α) => GraphModel.apply S T

Application is monotone in the first argument.

theorem GraphModel.apply.monotone_snd {α : Type} [Listing α] {S : Set α} : GraphModel.monotone (GraphModel.apply S)

Application is monotone in the second argument.

theorem GraphModel.apply.continuous_fst {α : Type} [Listing α] (T : Set α) : GraphModel.continuous (GraphModel.apply T)

Application is continuous in the first argument.

theorem GraphModel.apply.continuous_snd {α : Type} [Listing α] (S : Set α) : GraphModel.continuous fun (T : Set α) => GraphModel.apply T S

Application is continuous in the second argument.

theorem GraphModel.apply.continuous₂ {α : Type} [Listing α] : GraphModel.continuous₂ GraphModel.apply

Application is continuous.

theorem GraphModel.eq_apply_graph {α : Type} [Listing α] (f : Set α → Set α) : GraphModel.continuous f → GraphModel.apply (GraphModel.graph f) = f

def GraphModel.K {α : Type} [Listing α] : Set α

Equations

• GraphModel.K = GraphModel.graph fun (A : Set α) => GraphModel.graph fun (x : Set α) => A

theorem GraphModel.eq_K {α : Type} [Listing α] {A B : Set α} : GraphModel.K ⬝ A ⬝ B = A

def GraphModel.S {α : Type} [Listing α] : Set α

Equations

• GraphModel.S = GraphModel.graph fun (A : Set α) => GraphModel.graph fun (B : Set α) => GraphModel.graph fun (C : Set α) => A ⬝ C ⬝ (B ⬝ C)

theorem GraphModel.S.continuous₁ {α : Type} [Listing α] {B C : Set α} : GraphModel.continuous fun (A : Set α) => A ⬝ C ⬝ (B ⬝ C)

theorem GraphModel.S.continuous₂ {α : Type} [Listing α] {A C : Set α} : GraphModel.continuous fun (B : Set α) => A ⬝ C ⬝ (B ⬝ C)

theorem GraphModel.S.continuous₃ {α : Type} [Listing α] {A B : Set α} : GraphModel.continuous fun (C : Set α) => A ⬝ C ⬝ (B ⬝ C)

theorem GraphModel.eq_S {α : Type} [Listing α] {A B C : Set α} : GraphModel.S ⬝ A ⬝ B ⬝ C = A ⬝ C ⬝ (B ⬝ C)

instance GraphModel.isCA {α : Type} [Listing α] : CA (Set α)

The graph model

Equations

• GraphModel.isCA = CA.mk GraphModel.K GraphModel.S ⋯ ⋯