Exercise 5.7 (Scott 1981, PRG-19, §5) — multi-variable λ and application from

one-variable forms

Scott asks for definitions of the two-variable abstraction and application

λx, y. τ        and        σ(x, y)

that use only the one-variable binder λv and applications to one argument at a time, with the combinators p₀, p₁, pair doing the bookkeeping. He then asks to generalise to many variables.

In the neighbourhood-system framework this is exactly the curry/uncurry isomorphism of Theorem 3.12 together with surjective pairing:

• a two-variable function σ : D₀ × D₁ → D₂ is applied "one argument at a time" through its curried form, σ(x, y) = (curry σ)(x)(y); conversely uncurry h turns one-argument-at-a-time application back into a single application to a pair, and is literally built from one-argument pieces: uncurry h = eval ∘ ⟨h ∘ p₀, p₁⟩ (uncurry_eq), using only eval, p₀, p₁, pair;
• the two-variable abstraction λx, y. τ is curry, characterised by (curry g)(x)(y) = g⟨x, y⟩, i.e. it binds one variable and returns a one-variable function;
• the projections and pairing are tied together by surjective pairing ⟨p₀ z, p₁ z⟩ = z, the fact that makes p₀, p₁, pair sufficient to encode the product.

We record these as the realisations Scott requests, and give the three-variable generalisation via nested currying D₀ × (D₁ × D₂) → D₃, illustrating the pattern for arbitrarily many variables.

No new axioms are introduced beyond the project's Element.ext / ext_of_toElementMap machinery already used by curry/uncurry.

Surjective pairing: p₀, p₁, pair recover any element of the product.

theorem Domain.Neighborhood.Exercise507.surjective_pairing {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (z : (prod V₀ V₁).Element) : pair ((proj₀ V₀ V₁).toElementMap z) ((proj₁ V₀ V₁).toElementMap z) = z

Surjective pairing. Every element z : D₀ × D₁ is recovered from its projections: ⟨p₀(z), p₁(z)⟩ = z. This is what makes p₀, p₁, pair enough to encode the product.

Application to one argument at a time.

theorem Domain.Neighborhood.Exercise507.uncurry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : ApproximableMap V₀ (funSpace V₁ V₂)) (x : V₀.Element) (y : V₁.Element) : (uncurry h).toElementMap (pair x y) = (toApproxMap (h.toElementMap x)).toElementMap y

One-argument-at-a-time application. For h : D₀ → (D₁ → D₂), applying the uncurried map to a pair is the same as applying h to x and then to y: (uncurry h)(⟨x, y⟩) = h(x)(y).

theorem Domain.Neighborhood.Exercise507.app_two_args {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (σ : ApproximableMap (prod V₀ V₁) V₂) (x : V₀.Element) (y : V₁.Element) : σ.toElementMap (pair x y) = (toApproxMap ((curry σ).toElementMap x)).toElementMap y

The combinator σ(x, y) (apply σ : D₀ × D₁ → D₂ to two arguments) is expressed through the one-variable curried form: σ(⟨x, y⟩) = (curry σ)(x)(y). The right-hand side uses only single-variable application.

Two-variable abstraction λx, y. τ.

theorem Domain.Neighborhood.Exercise507.lam_two_vars {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap (prod V₀ V₁) V₂) (x : V₀.Element) (y : V₁.Element) : (toApproxMap ((curry g).toElementMap x)).toElementMap y = g.toElementMap (pair x y)

Two-variable abstraction. λx, y. τ is curry, characterised by (curry g)(x)(y) = g⟨x, y⟩. It binds one variable x and returns the one-variable function λy. g⟨x, y⟩.

theorem Domain.Neighborhood.Exercise507.uncurry_lam_two_vars {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap (prod V₀ V₁) V₂) : uncurry (curry g) = g

The two encodings are mutually inverse: uncurrying the two-variable abstraction returns the original two-variable function.

Generalisation to three variables (the pattern for many variables).

def Domain.Neighborhood.Exercise507.curry₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₃ : NeighborhoodSystem δ} (g : ApproximableMap (prod (prod V₀ V₁) V₂) V₃) : ApproximableMap V₀ (funSpace V₁ (funSpace V₂ V₃))

Three-variable abstraction λx, y, z. τ, via nested currying on (D₀ × D₁) × D₂ → D₃. Each curry strips one variable, so a function of n variables is reached by `n

• 1` curryings — single-variable binders all the way down.

Equations

• Domain.Neighborhood.Exercise507.curry₃ g = Domain.Neighborhood.curry (Domain.Neighborhood.curry g)

theorem Domain.Neighborhood.Exercise507.curry₃_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₃ : NeighborhoodSystem δ} (g : ApproximableMap (prod (prod V₀ V₁) V₂) V₃) (x : V₀.Element) (y : V₁.Element) (z : V₂.Element) : (toApproxMap ((toApproxMap ((curry₃ g).toElementMap x)).toElementMap y)).toElementMap z = g.toElementMap (pair (pair x y) z)

The defining equation of curry₃: (λx, y, z. g)(x)(y)(z) = g⟨⟨x, y⟩, z⟩.