Example 6.2 (Scott 1981, PRG-19, §6) — the generalisation A ≅ Aⁿ + Aⁿ

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture VI. After the staple equations B ≅ B + B and C ≅ {{Λ}} + C + C (see Example62.lean/Example62C.lean), Scott proposes "a simple, yet interesting generalization of B": for any n, the domain equation

A ≅ Aⁿ + Aⁿ,

where Aⁿ is the n-fold cartesian power. He solves it concretely over Σ* = {0,1}* as the least family

A = {Σ*} ∪ ⋃_{i∈{0,1}} { i ⋃_{j<n} 1ʲ0 X_j ∣ X_j ∈ A for all j < n },

so a neighbourhood (other than the master Σ*) is a tag bit i (Scott's +/−, here true/false) followed by n slots, slot j reached behind the self-delimiting prefix 1ʲ0. An element of A (other than ⊥) is thus ±⟨a₀, …, a_{n-1}⟩: an n-tuple of elements of A, in one of two copies.

This module delivers:

• npow V n — the flat n-fold product Vⁿ over Fin n × β, with neighbourhoods the proper products prodN X = ⋃_j {j} × X_j. (Closure under intersection is componentwise — no tags, so no non-emptiness needed.)
• Asys n hn — Scott's domain A over {0,1}* (the inductive family MemA), a neighbourhood system under 0 < n (so there is a coordinate to witness non-emptiness, Scott's ∅ ∉ A). The slot encoding is embTuple, parsed via the uniqueness lemma slotPre_inj.
• A_domain_equation — the order-isomorphism aaEquiv : |A| ≃o |Aⁿ + Aⁿ|, i.e. Asys n hn ≅ᴰ sum (npow A n) (npow A n) …, mirroring Example61.dsharpEquiv.

For n = 1 this recovers B ≅ B + B (one slot per copy); the tree picture and the automata-theory aside (eventually-periodic trees ↔ regular events) are formalised in Example62Regular.lean.

All data is choice-free (#print axioms ⊆ {propext, Quot.sound}).

The flat n-fold product Vⁿ over Fin n × β.

def Domain.Neighborhood.Example62A.prodN {β : Type u_1} {n : ℕ} (X : Fin n → Set β) : Set (Fin n × β)

The proper product neighbourhood ⋃_{j<n} {j} × X_j: token (j, b) lies in it iff b ∈ X_j. This is the n-ary analogue of prodNbhd (Definition 3.1).

Equations

• Domain.Neighborhood.Example62A.prodN X = {p : Fin n × β | p.2 ∈ X p.1}

@[simp]

theorem Domain.Neighborhood.Example62A.mem_prodN {β : Type u_1} {n : ℕ} {X : Fin n → Set β} {p : Fin n × β} : p ∈ prodN X ↔ p.2 ∈ X p.1

theorem Domain.Neighborhood.Example62A.prodN_subset {β : Type u_1} {n : ℕ} {X X' : Fin n → Set β} : prodN X ⊆ prodN X' ↔ ∀ (j : Fin n), X j ⊆ X' j

theorem Domain.Neighborhood.Example62A.prodN_inter {β : Type u_1} {n : ℕ} {X X' : Fin n → Set β} : prodN X ∩ prodN X' = prodN fun (j : Fin n) => X j ∩ X' j

theorem Domain.Neighborhood.Example62A.prodN_injective {β : Type u_1} {n : ℕ} {X X' : Fin n → Set β} (h : prodN X = prodN X') (j : Fin n) : X j = X' j

def Domain.Neighborhood.Example62A.npow {β : Type u_1} (V : NeighborhoodSystem β) (n : ℕ) : NeighborhoodSystem (Fin n × β)

The n-fold product Vⁿ of a neighbourhood system V, over Fin n × β. Its neighbourhoods are exactly the proper products prodN X with each component X j ∈ V. Closure under intersection is componentwise (no tags to disambiguate, so no non-emptiness is needed here).

Equations

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

@[simp]

theorem Domain.Neighborhood.Example62A.npow_mem {β : Type u_1} {n : ℕ} {V : NeighborhoodSystem β} {W : Set (Fin n × β)} : (npow V n).mem W ↔ ∃ (X : Fin n → Set β), (∀ (j : Fin n), V.mem (X j)) ∧ W = prodN X

theorem Domain.Neighborhood.Example62A.npow_nonempty {β : Type u_1} {n : ℕ} {V : NeighborhoodSystem β} (hn : 0 < n) (hV : ∀ (X : Set β), V.mem X → X.Nonempty) (W : Set (Fin n × β)) : (npow V n).mem W → W.Nonempty

Under Scott's standing assumption ∅ ∉ V, no neighbourhood of Vⁿ is empty (provided 0 < n, so there is a coordinate to witness).

Scott's slot encoding i ⋃_{j<n} 1ʲ0 X_j over {0,1}*.

def Domain.Neighborhood.Example62A.slotPre (i : Bool) (j : ℕ) : ExampleB.Str

The slot prefix i 1ʲ 0: the leading tag bit i (Scott's +/−), then j ones, then a zero. Reaching component j of the tag-i tuple means matching this prefix.

Equations

• Domain.Neighborhood.Example62A.slotPre i j = i :: (List.replicate j true ++ [false])

theorem Domain.Neighborhood.Example62A.slot_list_inj (j j' : ℕ) (u v : ExampleB.Str) : List.replicate j true ++ false :: u = List.replicate j' true ++ false :: v → j = j' ∧ u = v

Parsing the 1ʲ0 body: the position of the first false pins down j and the remainder.

theorem Domain.Neighborhood.Example62A.slotPre_inj {i i' : Bool} {j j' : ℕ} {u v : ExampleB.Str} (h : slotPre i j ++ u = slotPre i' j' ++ v) : i = i' ∧ j = j' ∧ u = v

Uniqueness of slot decomposition. A token i 1ʲ 0 u determines the tag i, the index j, and the remainder u. This is what makes the slots pairwise disjoint.

def Domain.Neighborhood.Example62A.embTuple {n : ℕ} (i : Bool) (X : Fin n → Set ExampleB.Str) : Set ExampleB.Str

Scott's tag-i tuple neighbourhood i ⋃_{j<n} 1ʲ0 X_j: the union of the n slots, slot j holding X j behind the prefix i 1ʲ 0. (For i = false/true these are Scott's left/right copies, the −/+ summands.)

Equations

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

@[simp]

theorem Domain.Neighborhood.Example62A.mem_embTuple {n : ℕ} {i : Bool} {X : Fin n → Set ExampleB.Str} {w : ExampleB.Str} : w ∈ embTuple i X ↔ ∃ (j : Fin n), ∃ (w' : ExampleB.Str), w = slotPre i ↑j ++ w' ∧ w' ∈ X j

theorem Domain.Neighborhood.Example62A.nil_not_mem_embTuple {n : ℕ} {i : Bool} {X : Fin n → Set ExampleB.Str} : ¬[] ∈ embTuple i X

theorem Domain.Neighborhood.Example62A.embTuple_ne_univ {n : ℕ} {i : Bool} (X : Fin n → Set ExampleB.Str) : embTuple i X ≠ Set.univ

theorem Domain.Neighborhood.Example62A.embTuple_inter {n : ℕ} {i : Bool} (X X' : Fin n → Set ExampleB.Str) : embTuple i X ∩ embTuple i X' = embTuple i fun (j : Fin n) => X j ∩ X' j

theorem Domain.Neighborhood.Example62A.embTuple_inter_ne {n : ℕ} {i i' : Bool} (h : i ≠ i') (X X' : Fin n → Set ExampleB.Str) : embTuple i X ∩ embTuple i' X' = ∅

theorem Domain.Neighborhood.Example62A.embTuple_subset {n : ℕ} {i : Bool} {X X' : Fin n → Set ExampleB.Str} : embTuple i X ⊆ embTuple i X' ↔ ∀ (j : Fin n), X j ⊆ X' j

theorem Domain.Neighborhood.Example62A.embTuple_injective {n : ℕ} {i : Bool} {X X' : Fin n → Set ExampleB.Str} (h : embTuple i X = embTuple i X') (j : Fin n) : X j = X' j

theorem Domain.Neighborhood.Example62A.embTuple_nonempty {n : ℕ} {i : Bool} {X : Fin n → Set ExampleB.Str} (j : Fin n) (h : (X j).Nonempty) : (embTuple i X).Nonempty

theorem Domain.Neighborhood.Example62A.embTuple_ne {n : ℕ} {i i' : Bool} (h : i ≠ i') {X Y : Fin n → Set ExampleB.Str} (j : Fin n) (hX : (X j).Nonempty) : embTuple i X ≠ embTuple i' Y

The neighbourhood system A solving A ≅ Aⁿ + Aⁿ.

inductive Domain.Neighborhood.Example62A.MemA (n : ℕ) : Set ExampleB.Str → Prop

Scott's domain A as the least family of subsets of Σ* = {0,1}* containing (i) the master Σ* and (ii) every tag-i tuple i ⋃_{j<n} 1ʲ0 X_j built from components X j already in A:

A = {Σ*} ∪ ⋃_{i∈{0,1}} { i ⋃_{j<n} 1ʲ0 X_j ∣ X_j ∈ A }.

• univ {n : ℕ} : MemA n Set.univ
• tuple {n : ℕ} (i : Bool) {X : Fin n → Set ExampleB.Str} : (∀ (j : Fin n), MemA n (X j)) → MemA n (embTuple i X)

theorem Domain.Neighborhood.Example62A.memA_nonempty {n : ℕ} (hn : 0 < n) {W : Set ExampleB.Str} : MemA n W → W.Nonempty

Under 0 < n every neighbourhood of A is non-empty (Scott's ∅ ∉ A).

theorem Domain.Neighborhood.Example62A.tag_eq_of_subset {n : ℕ} (hn : 0 < n) {i i' : Bool} {Z V : Fin n → Set ExampleB.Str} (hZ : ∀ (j : Fin n), MemA n (Z j)) (hsub : embTuple i Z ⊆ embTuple i' V) : i = i'

A non-empty witness contained in a tag-i' tuple must carry the tag i'.

theorem Domain.Neighborhood.Example62A.memA_tuple_inv {n : ℕ} (hn : 0 < n) {i : Bool} {X : Fin n → Set ExampleB.Str} (h : MemA n (embTuple i X)) (j : Fin n) : MemA n (X j)

Inversion: the components of a tuple-shaped neighbourhood of A are themselves in A.

theorem Domain.Neighborhood.Example62A.memA_inter {n : ℕ} (hn : 0 < n) {X : Set ExampleB.Str} : MemA n X → ∀ {Y : Set ExampleB.Str}, MemA n Y → ∀ {Z : Set ExampleB.Str}, MemA n Z → Z ⊆ X ∩ Y → MemA n (X ∩ Y)

A is closed under consistent intersection. Scott's verification, by induction on the way X entered A: the cross case embTuple false · ∩ embTuple true · collapses to ∅ (killed by the non-empty witness), the same-tag case combines componentwise (recursing on the consistency witness's slots).

def Domain.Neighborhood.Example62A.Asys (n : ℕ) (hn : 0 < n) : NeighborhoodSystem ExampleB.Str

Scott's domain A packaged as a neighbourhood system over {0,1}* (needs 0 < n).

Equations

• Domain.Neighborhood.Example62A.Asys n hn = { mem := Domain.Neighborhood.Example62A.MemA n, master := Set.univ, master_mem := ⋯, inter_mem := ⋯, sub_master := ⋯ }

@[simp]

theorem Domain.Neighborhood.Example62A.Asys_mem {n : ℕ} {hn : 0 < n} {W : Set ExampleB.Str} : (Asys n hn).mem W ↔ MemA n W

@[simp]

theorem Domain.Neighborhood.Example62A.Asys_master {n : ℕ} {hn : 0 < n} : (Asys n hn).master = Set.univ

The domain equation A ≅ Aⁿ + Aⁿ.

@[reducible, inline]

abbrev Domain.Neighborhood.Example62A.Apow {n : ℕ} (hn : 0 < n) : NeighborhoodSystem (Fin n × ExampleB.Str)

The n-fold product Aⁿ = npow A n.

Equations

• Domain.Neighborhood.Example62A.Apow hn = Domain.Neighborhood.Example62A.npow (Domain.Neighborhood.Example62A.Asys n hn) n

theorem Domain.Neighborhood.Example62A.apowNe {n : ℕ} (hn : 0 < n) (W : Set (Fin n × ExampleB.Str)) : (Apow hn).mem W → W.Nonempty

@[reducible, inline]

abbrev Domain.Neighborhood.Example62A.AAsys {n : ℕ} (hn : 0 < n) : NeighborhoodSystem (Option (Fin n × ExampleB.Str ⊕ Fin n × ExampleB.Str))

The right-hand side of Scott's equation: the separated sum Aⁿ + Aⁿ.

Equations

• Domain.Neighborhood.Example62A.AAsys hn = Domain.Neighborhood.sum (Domain.Neighborhood.Example62A.Apow hn) (Domain.Neighborhood.Example62A.Apow hn) ⋯ ⋯

theorem Domain.Neighborhood.Example62A.apow_mem_prodN {n : ℕ} (hn : 0 < n) {X : Fin n → Set ExampleB.Str} (hX : ∀ (j : Fin n), MemA n (X j)) : (Apow hn).mem (prodN X)

theorem Domain.Neighborhood.Example62A.apow_mem_prodN_inv {n : ℕ} (hn : 0 < n) {X : Fin n → Set ExampleB.Str} (h : (Apow hn).mem (prodN X)) (j : Fin n) : MemA n (X j)

theorem Domain.Neighborhood.Example62A.aa_mem_inj₀ {n : ℕ} (hn : 0 < n) {X : Fin n → Set ExampleB.Str} (hX : ∀ (j : Fin n), MemA n (X j)) : (AAsys hn).mem (inj₀ (prodN X))

theorem Domain.Neighborhood.Example62A.aa_mem_inj₁ {n : ℕ} (hn : 0 < n) {Y : Fin n → Set ExampleB.Str} (hY : ∀ (j : Fin n), MemA n (Y j)) : (AAsys hn).mem (inj₁ (prodN Y))

theorem Domain.Neighborhood.Example62A.aa_mem_inj₀_inv {n : ℕ} (hn : 0 < n) {V : Set (Fin n × ExampleB.Str)} (h : (AAsys hn).mem (inj₀ V)) : (Apow hn).mem V

theorem Domain.Neighborhood.Example62A.aa_mem_inj₁_inv {n : ℕ} (hn : 0 < n) {V : Set (Fin n × ExampleB.Str)} (h : (AAsys hn).mem (inj₁ V)) : (Apow hn).mem V

theorem Domain.Neighborhood.Example62A.aa_mem_nonempty {n : ℕ} (hn : 0 < n) {W : Set (Option (Fin n × ExampleB.Str ⊕ Fin n × ExampleB.Str))} (h : (AAsys hn).mem W) : W.Nonempty

def Domain.Neighborhood.Example62A.toAA {n : ℕ} (hn : 0 < n) (z : (Asys n hn).Element) : (AAsys hn).Element

Forward half of A ≅ Aⁿ + Aⁿ. An element z of A is sent to the sum element recording, for each branch, whether z reaches the left copy 0X (left summand Aⁿ) or the right copy 1Y (right summand Aⁿ).

Equations

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

@[simp]

theorem Domain.Neighborhood.Example62A.toAA_mem_inj₀ {n : ℕ} (hn : 0 < n) {z : (Asys n hn).Element} {X : Fin n → Set ExampleB.Str} (hX : ∀ (j : Fin n), MemA n (X j)) : (toAA hn z).mem (inj₀ (prodN X)) ↔ z.mem (embTuple false X)

@[simp]

theorem Domain.Neighborhood.Example62A.toAA_mem_inj₁ {n : ℕ} (hn : 0 < n) {z : (Asys n hn).Element} {Y : Fin n → Set ExampleB.Str} (hY : ∀ (j : Fin n), MemA n (Y j)) : (toAA hn z).mem (inj₁ (prodN Y)) ↔ z.mem (embTuple true Y)

def Domain.Neighborhood.Example62A.fromAA {n : ℕ} (hn : 0 < n) (s : (AAsys hn).Element) : (Asys n hn).Element

Inverse half of A ≅ Aⁿ + Aⁿ.

Equations

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

@[simp]

theorem Domain.Neighborhood.Example62A.fromAA_mem_embF {n : ℕ} (hn : 0 < n) {s : (AAsys hn).Element} {X : Fin n → Set ExampleB.Str} (hX : ∀ (j : Fin n), MemA n (X j)) : (fromAA hn s).mem (embTuple false X) ↔ s.mem (inj₀ (prodN X))

@[simp]

theorem Domain.Neighborhood.Example62A.fromAA_mem_embT {n : ℕ} (hn : 0 < n) {s : (AAsys hn).Element} {Y : Fin n → Set ExampleB.Str} (hY : ∀ (j : Fin n), MemA n (Y j)) : (fromAA hn s).mem (embTuple true Y) ↔ s.mem (inj₁ (prodN Y))

theorem Domain.Neighborhood.Example62A.fromAA_toAA {n : ℕ} (hn : 0 < n) (z : (Asys n hn).Element) : fromAA hn (toAA hn z) = z

theorem Domain.Neighborhood.Example62A.toAA_fromAA {n : ℕ} (hn : 0 < n) (s : (AAsys hn).Element) : toAA hn (fromAA hn s) = s

def Domain.Neighborhood.Example62A.aaEquiv {n : ℕ} (hn : 0 < n) : (Asys n hn).Element ≃o (AAsys hn).Element

The isomorphism |A| ≃o |Aⁿ + Aⁿ|.

Equations

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

theorem Domain.Neighborhood.Example62A.A_domain_equation {n : ℕ} (hn : 0 < n) : Asys n hn ≅ᴰ AAsys hn

Example 6.2 (Scott 1981, PRG-19) — the domain equation A ≅ Aⁿ + Aⁿ. Scott's "simple, yet interesting generalization of B": the domain A over {0,1}* (whose non-⊥ elements are the two copies — left − and right + — of an n-tuple of elements of A) is isomorphic to the separated sum Aⁿ + Aⁿ of two copies of its own n-fold cartesian power.