Exercise 5.8 (Scott 1981, PRG-19, §5) — combinatory completeness

(For combinator nuts.) Table 5.5 was meant to show how combinators could be defined in terms of λ-expressions. Can the tables be turned to show that with enough combinators available, every λ-expression can be defined by combining combinators, using σ(τ) as the only mode of combination?

The answer is yes: this is the classical theorem of combinatory completeness (bracket abstraction). With the three combinators

I = λx.x,        K = λx,y.x,        S = λf,g,x. f(x)(g(x))

available, every λ-abstraction can be eliminated in favour of pure application of combinators. We formalise this in the neighbourhood-system framework as follows.

• Dom packages a token type with its neighbourhood system, and Dom.arrow A B is the function domain (A → B) (its carrier is ApproximableMap A.sys B.sys).
• I, K, S are realised as concrete elements (Ielem, Kelem, Selem) of the appropriate function domains, with their value equations Ielem_apply, Kelem_apply, Selem_apply proved through the project's curry/eval/projection API.
• Poly X A is the intrinsically-typed syntax of λ-bodies with one free variable of type X: the variable itself, closed constants (any element — "enough combinators available"), and application. Its denotation Poly.denote t : |X| → |A| is the open term as a function of the variable, i.e. the body whose abstraction λx.t we wish to express.
• CL A is the syntax of variable-free combinator expressions: constants and application only (σ(τ) is the only mode of combination). Its denotation CL.denote : |A| is a single element.
• bracket : Poly X A → CL (X.arrow A) is bracket abstraction: it turns an open body t into a closed combinator expression, using only application together with the constants I, K, S and the constants already occurring in t — exactly Scott's challenge.

The completeness theorem is bracket_spec:

(bracket t).denote, applied to x, equals t.denote x       for every x.

i.e. the variable-free combinator expression bracket t denotes precisely the function λx.t. By induction on t this is driven by the three combinator identities, turning the table around as Scott asks.

Everything is data; the combinators are built from idMap, curry, proj, eval and are choice-free.

A generic round-trip for the function-space representation.

theorem Domain.Neighborhood.Exercise508.toApproxMap_toFilter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) : toApproxMap (toFilter f) = f

toApproxMap ∘ toFilter = id: the representation of a function-space element by an approximable map is a left inverse of toFilter (this is funSpaceEquiv unfolded).

The S combinator as an approximable map.

S = λf, g, x. f(x)(g(x)). We build the uncurried body Sbody(⟨⟨F, G⟩, x⟩) = eval(eval(F, x), eval(G, x)) out of projections, pairing and eval, then curry twice.

def Domain.Neighborhood.Exercise508.Sbody {αx : Type u_4} {αa : Type u_5} {αb : Type u_6} (Vx : NeighborhoodSystem αx) (Va : NeighborhoodSystem αa) (Vb : NeighborhoodSystem αb) : ApproximableMap (prod (prod (funSpace Vx (funSpace Va Vb)) (funSpace Vx Va)) Vx) Vb

The uncurried body of S: with F : 𝒟ₓ → (𝒟ₐ → 𝒟_b), G : 𝒟ₓ → 𝒟ₐ, x : 𝒟ₓ, Sbody⟨⟨F, G⟩, x⟩ = (F x)(G x), expressed using only proj, pair and eval.

Equations

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

def Domain.Neighborhood.Exercise508.Smap {αx : Type u_4} {αa : Type u_5} {αb : Type u_6} (Vx : NeighborhoodSystem αx) (Va : NeighborhoodSystem αa) (Vb : NeighborhoodSystem αb) : ApproximableMap (funSpace Vx (funSpace Va Vb)) (funSpace (funSpace Vx Va) (funSpace Vx Vb))

S = λf, g, x. f(x)(g(x)), the curried form (𝒟ₓ → (𝒟ₐ → 𝒟_b)) → ((𝒟ₓ → 𝒟ₐ) → (𝒟ₓ → 𝒟_b)).

Equations

• Domain.Neighborhood.Exercise508.Smap Vx Va Vb = Domain.Neighborhood.curry (Domain.Neighborhood.curry (Domain.Neighborhood.Exercise508.Sbody Vx Va Vb))

theorem Domain.Neighborhood.Exercise508.Smap_apply {αx : Type u_4} {αa : Type u_5} {αb : Type u_6} {Vx : NeighborhoodSystem αx} {Va : NeighborhoodSystem αa} {Vb : NeighborhoodSystem αb} (F : (funSpace Vx (funSpace Va Vb)).Element) (G : (funSpace Vx Va).Element) (x : Vx.Element) : (toApproxMap ((toApproxMap ((Smap Vx Va Vb).toElementMap F)).toElementMap G)).toElementMap x = (toApproxMap ((toApproxMap F).toElementMap x)).toElementMap ((toApproxMap G).toElementMap x)

The defining equation of S: S(F)(G)(x) = F(x)(G(x)).

Domains as data, and the function-domain constructor.

structure Domain.Neighborhood.Exercise508.Dom : Type 1

A domain: a token type together with its neighbourhood system. Bundling lets us build an intrinsically-typed syntax of combinator terms. We work over Type (universe 0), which covers all the concrete domains of these lectures (N, T, C, …) and their products/function spaces.

• carrier : Type

  The token type.

• sys : NeighborhoodSystem self.carrier

  The neighbourhood system on carrier.

def Domain.Neighborhood.Exercise508.Dom.arrow (A B : Dom) : Dom

The function domain (A → B); its carrier is ApproximableMap A.sys B.sys and its system is the function space funSpace A.sys B.sys.

Equations

• A.arrow B = { carrier := Domain.Neighborhood.ApproximableMap A.sys B.sys, sys := Domain.Neighborhood.funSpace A.sys B.sys }

The three combinators as elements of the appropriate function domains.

def Domain.Neighborhood.Exercise508.Ielem (X : Dom) : (X.arrow X).sys.Element

I = λx.x as an element of (X → X).

Equations

• Domain.Neighborhood.Exercise508.Ielem X = Domain.Neighborhood.toFilter (Domain.Neighborhood.ApproximableMap.idMap X.sys)

def Domain.Neighborhood.Exercise508.Kelem (A X : Dom) : (A.arrow (X.arrow A)).sys.Element

K = λx, y.x as an element of (A → (X → A)).

Equations

• Domain.Neighborhood.Exercise508.Kelem A X = Domain.Neighborhood.toFilter (Domain.Neighborhood.curry (Domain.Neighborhood.proj₀ A.sys X.sys))

def Domain.Neighborhood.Exercise508.Selem (X A B : Dom) : ((X.arrow (A.arrow B)).arrow ((X.arrow A).arrow (X.arrow B))).sys.Element

S = λf, g, x. f(x)(g(x)) as an element of ((X → (A → B)) → ((X → A) → (X → B))).

Equations

• Domain.Neighborhood.Exercise508.Selem X A B = Domain.Neighborhood.toFilter (Domain.Neighborhood.Exercise508.Smap X.sys A.sys B.sys)

theorem Domain.Neighborhood.Exercise508.Ielem_apply (X : Dom) (x : X.sys.Element) : (toApproxMap (Ielem X)).toElementMap x = x

I(x) = x.

theorem Domain.Neighborhood.Exercise508.Kelem_apply (A X : Dom) (c : A.sys.Element) (x : X.sys.Element) : (toApproxMap ((toApproxMap (Kelem A X)).toElementMap c)).toElementMap x = c

K(c)(x) = c.

theorem Domain.Neighborhood.Exercise508.Selem_apply (X A B : Dom) (F : (X.arrow (A.arrow B)).sys.Element) (G : (X.arrow A).sys.Element) (x : X.sys.Element) : (toApproxMap ((toApproxMap ((toApproxMap (Selem X A B)).toElementMap F)).toElementMap G)).toElementMap x = (toApproxMap ((toApproxMap F).toElementMap x)).toElementMap ((toApproxMap G).toElementMap x)

S(F)(G)(x) = F(x)(G(x)).

Syntax of λ-bodies with one free variable, and of variable-free

combinator expressions.

inductive Domain.Neighborhood.Exercise508.Poly (X : Dom) : Dom → Type 1

Poly X A: an open term of type A with a single free variable of type X. Constructors: the variable, a closed constant (any element of any domain — "enough combinators available"), and application. This is the syntax of λ-bodies whose abstraction we want to eliminate.

• var {X : Dom} : Poly X X

  The free variable.

• con {X A : Dom} (c : A.sys.Element) : Poly X A

  A closed constant c : |A| (in particular any available combinator).

• app {X A B : Dom} (f : Poly X (A.arrow B)) (a : Poly X A) : Poly X B

  Application f(a).

inductive Domain.Neighborhood.Exercise508.CL : Dom → Type 1

CL A: a variable-free combinator expression of type A. The only constructors are constants and application, so application (σ(τ)) is the sole mode of combination.

• con {A : Dom} (c : A.sys.Element) : CL A

  A closed constant.

• app {A B : Dom} (f : CL (A.arrow B)) (a : CL A) : CL B

  Application f(a).

def Domain.Neighborhood.Exercise508.Poly.denote {X A : Dom} : Poly X A → X.sys.Element → A.sys.Element

The denotation of an open term: the body as a function of its free variable.

Equations

• Domain.Neighborhood.Exercise508.Poly.var.denote x✝ = x✝
• (Domain.Neighborhood.Exercise508.Poly.con c).denote x✝ = c
• (f.app a).denote x✝ = (Domain.Neighborhood.toApproxMap (f.denote x✝)).toElementMap (a.denote x✝)

def Domain.Neighborhood.Exercise508.CL.denote {A : Dom} : CL A → A.sys.Element

The denotation of a variable-free combinator expression: a single element.

Equations

• (Domain.Neighborhood.Exercise508.CL.con c).denote = c
• (f.app a).denote = (Domain.Neighborhood.toApproxMap f.denote).toElementMap a.denote

Bracket abstraction.

def Domain.Neighborhood.Exercise508.bracket {X A : Dom} : Poly X A → CL (X.arrow A)

Bracket abstraction. Turn an open body t (a λ-body with one free variable) into a variable-free combinator expression denoting λx.t, using only application and the combinators I, K, S together with the constants already occurring in t:

• [x] x = I
• [x] c = K(c) (c a constant / closed term)
• [x] (f a) = S([x]f)([x]a).

Equations

• One or more equations did not get rendered due to their size.
• Domain.Neighborhood.Exercise508.bracket Domain.Neighborhood.Exercise508.Poly.var = Domain.Neighborhood.Exercise508.CL.con (Domain.Neighborhood.Exercise508.Ielem X)

theorem Domain.Neighborhood.Exercise508.bracket_spec {X A : Dom} (t : Poly X A) (x : X.sys.Element) : (toApproxMap (bracket t).denote).toElementMap x = t.denote x

Combinatory completeness (Exercise 5.8, Scott 1981, PRG-19). The variable-free combinator expression bracket t denotes exactly the function λx.t: applied to any x, it yields t.denote x.

Thus, with I, K, S (and the constants of t) available, every λ-abstraction can be defined by combining combinators using application as the only mode of combination — Scott's "turning of the tables".