Lecture V (§5) — Table 5.5: a table of combinators

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture V, Typed λ-calculus. Table 5.5 summarizes how the standard combinators are defined by λ-notation. In the neighbourhood-system/approximable-map framework of these lectures, each combinator scheme is realized as a concrete approximable map, and Scott's λ-equations become the value equations of those maps (proved through the projection/pairing/eval/curry/fix API of Lecture III–IV).

Scott's table	here	value equation
P₀ = λx,y.x	P₀ = proj₀	P₀⟨x,y⟩ = x
P₁ = λx,y.y	P₁ = proj₁	P₁⟨x,y⟩ = y
pair = λx λy.⟨x,y⟩	pairC = curry I	pairC x y = ⟨x,y⟩
diag = λx.⟨x,x⟩	diag = ⟨I,I⟩	diag x = ⟨x,x⟩
funpair = λf λg λx.⟨f x, g x⟩	funpairC	funpairC f g x = ⟨f x, g x⟩
proj_i^n	base cases P₀,P₁	(scheme; see note)
inv_{i,j}^n	base case swapC	swapC⟨x,y⟩ = ⟨y,x⟩
eval = λf,x.f x	evalC = evalMap	evalC⟨f,x⟩ = f x
curry = λg λx λy.g(x,y)	curryC = ofIso	curryC g x y = g⟨x,y⟩
comp = λg,f λx.g(f x)	compC = curry …	compC⟨g,f⟩ = g ∘ f
const = λk λx.k	constC = curry proj₀	constC k x = k
fix = λf !x.f x	fixC = fixMap	fixC f = fix f

A note on n-ary schemes. Scott stresses that the table entries are schemes: n-tuple, proj_i^n, inv_{i,j}^n are families parameterized by an arity n. The framework models the n-fold product by iterating the binary product prod, so the n-ary combinators are obtained by iterating the binary ones recorded here (P₀/P₁ are proj_0^2/proj_1^2; pairC is the 2-tuple; swapC is inv_{0,1}^2). We give the binary base cases as concrete maps.

All combinators are data; the genuinely first-order ones (P₀, P₁, pairC, diag, funpairC, swapC, evalC, constC, compC) are choice-free (#print axioms ⊆ {propext, Quot.sound}). curryC and fixC are built from the established ofIso/fixMap API.

P₀ = λx,y.x and P₁ = λx,y.y — the binary projections.

def Domain.Neighborhood.P₀ {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : ApproximableMap (prod V₀ V₁) V₀

Table 5.5 (Scott 1981, PRG-19). P₀ = λx,y.x, the first projection 𝒟₀ × 𝒟₁ → 𝒟₀.

Equations

• Domain.Neighborhood.P₀ V₀ V₁ = Domain.Neighborhood.proj₀ V₀ V₁

def Domain.Neighborhood.P₁ {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : ApproximableMap (prod V₀ V₁) V₁

Table 5.5 (Scott 1981, PRG-19). P₁ = λx,y.y, the second projection 𝒟₀ × 𝒟₁ → 𝒟₁.

Equations

• Domain.Neighborhood.P₁ V₀ V₁ = Domain.Neighborhood.proj₁ V₀ V₁

@[simp]

theorem Domain.Neighborhood.P₀_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (x : V₀.Element) (y : V₁.Element) : (P₀ V₀ V₁).toElementMap (pair x y) = x

@[simp]

theorem Domain.Neighborhood.P₁_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (x : V₀.Element) (y : V₁.Element) : (P₁ V₀ V₁).toElementMap (pair x y) = y

pair = λx λy.⟨x,y⟩ — the curried element pairing.

def Domain.Neighborhood.pairC {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : ApproximableMap V₀ (funSpace V₁ (prod V₀ V₁))

Table 5.5 (Scott 1981, PRG-19). pair = λx λy.⟨x,y⟩, as the curried map 𝒟₀ → (𝒟₁ → 𝒟₀ × 𝒟₁).

Equations

• Domain.Neighborhood.pairC V₀ V₁ = Domain.Neighborhood.curry (Domain.Neighborhood.ApproximableMap.idMap (Domain.Neighborhood.prod V₀ V₁))

theorem Domain.Neighborhood.pairC_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (x : V₀.Element) (y : V₁.Element) : (toApproxMap ((pairC V₀ V₁).toElementMap x)).toElementMap y = pair x y

diag = λx.⟨x,x⟩ — the diagonal.

def Domain.Neighborhood.diagC {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap V (prod V V)

Table 5.5 (Scott 1981, PRG-19). diag = λx.⟨x,x⟩, the diagonal 𝒟 → 𝒟 × 𝒟.

Equations

• Domain.Neighborhood.diagC V = Domain.Neighborhood.paired (Domain.Neighborhood.ApproximableMap.idMap V) (Domain.Neighborhood.ApproximableMap.idMap V)

@[simp]

theorem Domain.Neighborhood.diagC_apply {α : Type u_1} {V : NeighborhoodSystem α} (x : V.Element) : (diagC V).toElementMap x = pair x x

inv = λx,y.⟨y,x⟩ — the binary argument swap (base case of

inv_{i,j}^n).

def Domain.Neighborhood.swapC {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : ApproximableMap (prod V₀ V₁) (prod V₁ V₀)

Table 5.5 (Scott 1981, PRG-19). The base case inv_{0,1}^2 = λx,y.⟨y,x⟩ of the argument-swap scheme: 𝒟₀ × 𝒟₁ → 𝒟₁ × 𝒟₀.

Equations

• Domain.Neighborhood.swapC V₀ V₁ = Domain.Neighborhood.paired (Domain.Neighborhood.proj₁ V₀ V₁) (Domain.Neighborhood.proj₀ V₀ V₁)

@[simp]

theorem Domain.Neighborhood.swapC_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (x : V₀.Element) (y : V₁.Element) : (swapC V₀ V₁).toElementMap (pair x y) = pair y x

eval = λf,x.f x — evaluation.

def Domain.Neighborhood.evalC {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : ApproximableMap (prod (funSpace V₀ V₁) V₀) V₁

Table 5.5 (Scott 1981, PRG-19). eval = λf,x.f(x), evaluation (𝒟₀ → 𝒟₁) × 𝒟₀ → 𝒟₁ (this is Theorem 3.11's evalMap).

Equations

• Domain.Neighborhood.evalC V₀ V₁ = Domain.Neighborhood.evalMap V₀ V₁

theorem Domain.Neighborhood.evalC_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (funSpace V₀ V₁).Element) (x : V₀.Element) : (evalC V₀ V₁).toElementMap (pair φ x) = (toApproxMap φ).toElementMap x

const = λk λx.k — the constant-function combinator.

def Domain.Neighborhood.constC {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : ApproximableMap V₁ (funSpace V₀ V₁)

Table 5.5 (Scott 1981, PRG-19). const = λk λx.k, sending k ∈ |𝒟₁| to the constant map 𝒟₀ → 𝒟₁. Realized as curry(p₀).

Equations

• Domain.Neighborhood.constC V₀ V₁ = Domain.Neighborhood.curry (Domain.Neighborhood.proj₀ V₁ V₀)

theorem Domain.Neighborhood.constC_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (k : V₁.Element) (x : V₀.Element) : (toApproxMap ((constC V₀ V₁).toElementMap k)).toElementMap x = k

theorem Domain.Neighborhood.constC_eq_constMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (k : V₁.Element) : toApproxMap ((constC V₀ V₁).toElementMap k) = constMap V₀ k

const(k) is the constant map constMap of Lemma 3.6.

curry = λg λx λy.g(x,y) — currying as a combinator.

def Domain.Neighborhood.curryIso {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : (funSpace (prod V₀ V₁) V₂).Element ≃o (funSpace V₀ (funSpace V₁ V₂)).Element

The order-isomorphism |𝒟₀ × 𝒟₁ → 𝒟₂| ≃o |𝒟₀ → (𝒟₁ → 𝒟₂)| between the function-space domains, obtained from Theorem 3.10 (funSpaceEquiv) and Theorem 3.12 (curryEquiv).

Equations

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

def Domain.Neighborhood.curryC {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap (funSpace (prod V₀ V₁) V₂) (funSpace V₀ (funSpace V₁ V₂))

Table 5.5 (Scott 1981, PRG-19). curry = λg λx λy.g(x,y) as an approximable map (𝒟₀ × 𝒟₁ → 𝒟₂) → (𝒟₀ → (𝒟₁ → 𝒟₂)).

Equations

• Domain.Neighborhood.curryC V₀ V₁ V₂ = Domain.Neighborhood.ApproximableMap.ofIso (Domain.Neighborhood.curryIso V₀ V₁ V₂)

theorem Domain.Neighborhood.curryC_toApproxMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (φ : (funSpace (prod V₀ V₁) V₂).Element) : toApproxMap ((curryC V₀ V₁ V₂).toElementMap φ) = curry (toApproxMap φ)

curry(g) is the curried map of Theorem 3.12.

theorem Domain.Neighborhood.curryC_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (φ : (funSpace (prod V₀ V₁) V₂).Element) (x : V₀.Element) (y : V₁.Element) : (toApproxMap ((toApproxMap ((curryC V₀ V₁ V₂).toElementMap φ)).toElementMap x)).toElementMap y = (toApproxMap φ).toElementMap (pair x y)

comp = λg,f λx.g(f x) — composition as a combinator.

def Domain.Neighborhood.compMapTbl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap (prod (prod (funSpace V₁ V₂) (funSpace V₀ V₁)) V₀) V₂

The uncurried (g, f), x ↦ g(f(x)) over ((𝒟₁→𝒟₂) × (𝒟₀→𝒟₁)) × 𝒟₀ → 𝒟₂, built purely from projections, pairing and eval (this is the variable-free expression Scott alludes to).

Equations

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

def Domain.Neighborhood.compC {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap (prod (funSpace V₁ V₂) (funSpace V₀ V₁)) (funSpace V₀ V₂)

Table 5.5 (Scott 1981, PRG-19). comp = λg,f λx.g(f(x)) as an approximable map ((𝒟₁→𝒟₂) × (𝒟₀→𝒟₁)) → (𝒟₀ → 𝒟₂).

Equations

• Domain.Neighborhood.compC V₀ V₁ V₂ = Domain.Neighborhood.curry (Domain.Neighborhood.compMapTbl V₀ V₁ V₂)

theorem Domain.Neighborhood.compC_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (φ : (funSpace V₁ V₂).Element) (ψ : (funSpace V₀ V₁).Element) (x : V₀.Element) : (toApproxMap ((compC V₀ V₁ V₂).toElementMap (pair φ ψ))).toElementMap x = (toApproxMap φ).toElementMap ((toApproxMap ψ).toElementMap x)

theorem Domain.Neighborhood.compC_eq_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (φ : (funSpace V₁ V₂).Element) (ψ : (funSpace V₀ V₁).Element) : toApproxMap ((compC V₀ V₁ V₂).toElementMap (pair φ ψ)) = (toApproxMap φ).comp (toApproxMap ψ)

comp(g, f) = g ∘ f (Scott's infix g ∘ f).

funpair = λf λg λx.⟨f x, g x⟩.

def Domain.Neighborhood.funpairMapTbl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap (prod (prod (funSpace V₂ V₀) (funSpace V₂ V₁)) V₂) (prod V₀ V₁)

The uncurried (f, g), x ↦ ⟨f(x), g(x)⟩ over ((𝒟₂→𝒟₀) × (𝒟₂→𝒟₁)) × 𝒟₂ → 𝒟₀ × 𝒟₁.

Equations

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

def Domain.Neighborhood.funpairC {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap (funSpace V₂ V₀) (funSpace (funSpace V₂ V₁) (funSpace V₂ (prod V₀ V₁)))

Table 5.5 (Scott 1981, PRG-19). funpair = λf λg λx.⟨f(x), g(x)⟩, the curried operation (𝒟₂→𝒟₀) → ((𝒟₂→𝒟₁) → (𝒟₂ → 𝒟₀ × 𝒟₁)).

Equations

• Domain.Neighborhood.funpairC V₀ V₁ V₂ = Domain.Neighborhood.curry (Domain.Neighborhood.curry (Domain.Neighborhood.funpairMapTbl V₀ V₁ V₂))

theorem Domain.Neighborhood.funpairC_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (φ : (funSpace V₂ V₀).Element) (ψ : (funSpace V₂ V₁).Element) (x : V₂.Element) : (toApproxMap ((toApproxMap ((funpairC V₀ V₁ V₂).toElementMap φ)).toElementMap ψ)).toElementMap x = pair ((toApproxMap φ).toElementMap x) ((toApproxMap ψ).toElementMap x)

theorem Domain.Neighborhood.funpairC_eq_paired {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (φ : (funSpace V₂ V₀).Element) (ψ : (funSpace V₂ V₁).Element) : toApproxMap ((toApproxMap ((funpairC V₀ V₁ V₂).toElementMap φ)).toElementMap ψ) = paired (toApproxMap φ) (toApproxMap ψ)

funpair(f)(g) is the paired map ⟨f, g⟩ of Definition 3.3.

fix = λf !x.f x — the least fixed-point operator.

def Domain.Neighborhood.fixC {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (funSpace V V) V

Table 5.5 (Scott 1981, PRG-19). fix = λf.!x.f(x), the least fixed-point operator (𝒟 → 𝒟) → 𝒟 (Theorem 4.2's fixMap).

Equations

• Domain.Neighborhood.fixC V = Domain.Neighborhood.fixMap V

theorem Domain.Neighborhood.fixC_apply {α : Type u_1} {V : NeighborhoodSystem α} (φ : (funSpace V V).Element) : (fixC V).toElementMap φ = (toApproxMap φ).fixElement

theorem Domain.Neighborhood.fixC_fixed {α : Type u_1} {V : NeighborhoodSystem α} (φ : (funSpace V V).Element) : (toApproxMap φ).toElementMap ((fixC V).toElementMap φ) = (fixC V).toElementMap φ

fix(f) = f(fix(f)).