Definition 7.1 (Scott 1981, PRG-19, §7) — computable presentations / effectively

given domains

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19, Lecture VII, Computability in effectively given domains.

Scott's idea: the finite elements of |𝒟| are the ones initially known, and to know a finite element is to know how it is related to the other finite elements. As finite elements are in one-one correspondence with neighbourhoods (Definition 1.7), the data reduces to recursive calculations with neighbourhoods. This forces at most a countable infinity of neighbourhoods.

Definition 7.1. A neighbourhood system 𝒟 has a computable presentation provided we can write 𝒟 = {Xₙ ∣ n ∈ ℕ}, where the two relations

• (i) Xₙ ∩ Xₘ = X_k, and
• (ii) ∃ k. X_k ⊆ Xₙ and X_k ⊆ Xₘ

are recursively decidable (in n, m, k and in n, m respectively).

Recursion theory: we roll our own and reject Mathlib here. "Recursively decidable" is modelled by Domain.Recursive.RecDecidable — the existence of a primitive-recursive {0,1}-valued characteristic function, with tuples coded by Nat.pair. We deliberately do not use Mathlib's recursion theory (ComputablePred / Primrec / Partrec): in Mathlib v4.30.0 essentially all of its correctness lemmas are proved with grind/lia or the @[simp] lemma Nat.unpair_pair, which open Classical, so they audit with Classical.choice. This project's discipline is to keep constructions choice-free (⊆ {propext, Quot.sound}), so we rebuilt the slice of recursion theory we need (choice-free Nat.sqrt correctness, the Nat.pair/unpair round-trips, and primitive-recursive id/+/*) in Domain/Neighborhood/Recursive.lean. Relation (i) is the ternary interEq predicate (RecDecidable₃); relation (ii) is the binary consistency predicate (RecDecidable₂). The enumeration X is the only data the structure carries (a plain ℕ → Set α), so building a presentation stays choice-free.

The intuitive content (Scott's prose): (i) lets us locate the intersection of two neighbourhoods in the standard list, and (ii) is the consistency condition — the necessary and sufficient condition for the intersection to exist in 𝒟. Scott immediately remarks the biconditional Xₙ ⊆ Xₘ ↔ Xₙ ∩ Xₘ = Xₙ, which makes the inclusion relation decidable from (i); we record this as ComputablePresentation.incl_computable, and equality of neighbourhoods as eq_computable.

A neighbourhood system is effectively given when it admits such a presentation (NeighborhoodSystem.IsEffectivelyGiven). The one-point system 𝟙 is the sanity inhabitant (unitSys_isEffectivelyGiven).

structure Domain.Neighborhood.ComputablePresentation {α : Type u_1} (V : NeighborhoodSystem α) : Type u_1

Definition 7.1 (Scott 1981, PRG-19). A computable presentation of a neighbourhood system V over a token type α: an enumeration X : ℕ → Set α whose range is exactly 𝒟 (mem_X and surj), such that Scott's two relations on the integer indices are recursively decidable:

• interEq_computable is (i): the ternary relation Xₙ ∩ Xₘ = X_k;
• cons_computable is (ii): the binary consistency relation ∃ k. X_k ⊆ Xₙ ∩ Xₘ (Scott's X_k ⊆ Xₙ and X_k ⊆ Xₘ).

Only the enumeration X is data; the remaining fields are Props, so a presentation is built choice-free.

• X : ℕ → Set α

  The enumeration 𝒟 = {Xₙ ∣ n ∈ ℕ}.

• mem_X (n : ℕ) : V.mem (self.X n)

  Every Xₙ is a neighbourhood.

• surj {Y : Set α} : V.mem Y → ∃ (n : ℕ), self.X n = Y

  The enumeration is onto 𝒟: every neighbourhood appears as some Xₙ.

• interEq_computable : Recursive.RecDecidable₃ fun (n m k : ℕ) => self.X n ∩ self.X m = self.X k

  7.1(i) — Xₙ ∩ Xₘ = X_k is recursively decidable in n, m, k.

• cons_computable : Recursive.RecDecidable₂ fun (n m : ℕ) => ∃ (k : ℕ), self.X k ⊆ self.X n ∩ self.X m

  7.1(ii) — consistency ∃ k. X_k ⊆ Xₙ ∩ Xₘ is recursively decidable in n, m.

• inter : ℕ → ℕ → ℕ

  A primitive-recursive intersection function: an index of Xₙ ∩ Xₘ whenever that intersection is a neighbourhood (i.e. consistent). This makes explicit the operation that 7.1(i) is about: in Scott's general-recursive reading of "recursively decidable" the index can be recovered from interEq_computable by an (unbounded) search μk. Xₙ ∩ Xₘ = X_k, but that search is not primitive recursive; for the function-space presentation (Theorem 7.5) we need to form component intersections primitively, so we carry the function as part of the data of an ("acceptable") computable presentation. Off the consistent domain inter n m may be junk.

• inter_primrec : Nat.Primrec fun (t : ℕ) => self.inter (Nat.unpair t).1 (Nat.unpair t).2

  The intersection function is primitive recursive (on the Nat.pair coding of n, m).

• inter_spec {n m : ℕ} : (∃ (k : ℕ), self.X k ⊆ self.X n ∩ self.X m) → self.X (self.inter n m) = self.X n ∩ self.X m

  inter n m indexes Xₙ ∩ Xₘ whenever that intersection is consistent.

• masterIdx : ℕ

  A fixed index of the master neighbourhood Δ (used to seed finite intersections).

• masterIdx_spec : self.X self.masterIdx = V.master

  X masterIdx = Δ.

theorem Domain.Neighborhood.ComputablePresentation.incl_computable {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) : Recursive.RecDecidable₂ fun (n m : ℕ) => P.X n ⊆ P.X m

Scott's biconditional after 7.1. "The inclusion relation between neighbourhoods is itself decidable in terms of the indices", because Xₙ ⊆ Xₘ ↔ Xₙ ∩ Xₘ = Xₙ. We obtain the decision by reindexing (n, m) ↦ (n, m, n) into relation (i).

theorem Domain.Neighborhood.ComputablePresentation.eq_computable {α : Type u_1} {V : NeighborhoodSystem α} (P : ComputablePresentation V) : Recursive.RecDecidable₂ fun (n m : ℕ) => P.X n = P.X m

Equality of neighbourhoods is decidable from the indices: Xₙ = Xₘ ↔ Xₙ ⊆ Xₘ ∧ Xₘ ⊆ Xₙ, so equality is the conjunction of incl_computable with its swap.

def Domain.Neighborhood.NeighborhoodSystem.IsEffectivelyGiven {α : Type u_1} (V : NeighborhoodSystem α) : Prop

Definition 7.1 (Scott 1981, PRG-19) — effectively given. A neighbourhood system is effectively given when it admits a computable presentation.

Equations

• V.IsEffectivelyGiven = Nonempty (Domain.Neighborhood.ComputablePresentation V)

Sanity inhabitant: the one-point domain 𝟙 is effectively given.

def Domain.Neighborhood.unitPresentation : ComputablePresentation unitSys

The trivial presentation of the one-point system 𝟙 = unitSys: the constant enumeration Xₙ = Δ = univ. Both of Scott's relations are always true here (any two neighbourhoods are equal and consistent), hence trivially recursively decidable via the constant 1 decider.

Equations

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

theorem Domain.Neighborhood.unitSys_isEffectivelyGiven : unitSys.IsEffectivelyGiven

The one-point domain 𝟙 is effectively given.