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

class LeanPool.PartialCombinatoryAlgebras.Listing (α : Type) : Type

An encoding of lists of α's as α.

• fromList : List α → α

  Encode a list as a single element.

• toList : α → List α

  Decode an element back into a list.

• eq_list (xs : List α) : toList (fromList xs) = xs

  Encoding followed by decoding is the identity.

@[implicit_reducible]

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

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

Equations

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

@[reducible]

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

[x] qua subset of elements listed by x.

Equations

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

@[simp]

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

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

We encode pairs as lists of length two.

Equations

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

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

The first projection from a pair.

Equations

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

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

The second projection from a pair.

Equations

• LeanPool.PartialCombinatoryAlgebras.Listing.snd x = (LeanPool.PartialCombinatoryAlgebras.Listing.toList x)[1]!

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

Computation rule for the first projection from a pair.

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

Computation rule for the second projection from a pair.

def LeanPool.PartialCombinatoryAlgebras.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

• One or more equations did not get rendered due to their size.

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

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

Equations

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

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

A continuous map is monotone

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

Continuity of a binary map

Equations

• One or more equations did not get rendered due to their size.

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

Monotonicity of a binary map.

Equations

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

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

A continuous binary map is monotone.

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

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

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

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

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

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

theorem LeanPool.PartialCombinatoryAlgebras.GraphModel.continuous_id {α : Type} [Listing α] : continuous id

The identity map is continuous.

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

A constant map is continuous.

theorem LeanPool.PartialCombinatoryAlgebras.GraphModel.continuous_finite {α : Type} [Listing α] {f : Set α → Set α} (ys : List α) (S : Set α) : 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 LeanPool.PartialCombinatoryAlgebras.GraphModel.continuous_compose {α : Type} [Listing α] (f g : Set α → Set α) : continuous f → continuous g → continuous (f ∘ g)

The composition of continuous maps is continuous.

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

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

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

The graph of a function

Equations

• One or more equations did not get rendered due to their size.

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

Currying combined with graph is continuous

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

Combinatory application on the graph model

Equations

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

@[reducible]

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

Equations

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

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

Application is monotone.

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

Application is monotone in the first argument.

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

Application is monotone in the second argument.

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

Application is continuous in the first argument.

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

Application is continuous in the second argument.

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

Application is continuous.

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

The graph of a continuous map applied (via apply) recovers the map.

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

The K combinator of the graph model.

Equations

• One or more equations did not get rendered due to their size.

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

The graph-model K combinator satisfies the K equation.

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

The S combinator of the graph model.

Equations

• One or more equations did not get rendered due to their size.

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

Continuity component used in eq_S.

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

Continuity component used in eq_S.

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

Continuity component used in eq_S.

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

The graph-model S combinator satisfies the S equation.

@[implicit_reducible]

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

The graph model

Equations

• One or more equations did not get rendered due to their size.