def Semantics.Reference.Binding.W {A B : Type} (κ : A → A → B) (x : A) : B

Duplicator combinator W = λκ λx. κ x x.

Equations

• Semantics.Reference.Binding.W κ x = κ x x

def Semantics.Reference.Binding.hkBinding {E : Type} (n : ℕ) (body : E → Prop) (binder : E) (g : Core.Assignment E) : Prop

H&K interpretation of binding.

Equations

• Semantics.Reference.Binding.hkBinding n body binder g = body (Function.update g n binder n)

def Semantics.Reference.Binding.bsBinding {Entity : Type} (body : Entity → Entity → Prop) (binder : Entity) : Prop

B&S interpretation of binding (continuation-based).

Equations

• Semantics.Reference.Binding.bsBinding body binder = Semantics.Reference.Binding.W body binder

theorem Semantics.Reference.Binding.hk_bs_reflexive_equiv {E : Type} (n : ℕ) (body : E → E → Prop) (binder : E) (g : Core.Assignment E) : body (Function.update g n binder n) (Function.update g n binder n) = W body binder

H&K and B&S agree for reflexive binding: both produce body(binder, binder).

@[reducible, inline]

abbrev Semantics.Reference.Binding.Reader (E A : Type) : Type

The Reader monad (H&K assignments are Reader computations).

Equations

• Semantics.Reference.Binding.Reader E A = (E → A)

@[implicit_reducible]

instance Semantics.Reference.Binding.instMonadReader {E : Type} : Monad (Reader E)

Reader is a monad.

Equations

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

def Semantics.Reference.Binding.cpsTransform {E A R : Type} (f : Reader E A) : (A → R) → E → R

CPS transform: Reader → Continuation-expecting function.

Equations

• Semantics.Reference.Binding.cpsTransform f k e = k (f e)

theorem Semantics.Reference.Binding.cps_preserves_semantics {E A : Type} (f : Reader E A) (e : E) (k : A → Prop) : cpsTransform f k e = k (f e)

CPS transform preserves binding semantics.

theorem Semantics.Reference.Binding.binding_is_contraction {A : Type} (rel : A → A → Prop) (x : A) : (fun (x_1 : Unit) => rel x x) () = W rel x

W is the semantic content of binding in both frameworks.

Binding as cylindric algebra substitution

The connection between Heim & Kratzer's binding mechanism and cylindric algebra ([HMT71]):

• Binder at index n creates fun x => body(g[n↦x]), the function whose existential closure is cylindrification cₙ
• Bound pronoun at index n reads g(n), a register projection
• Binding resolution (pronoun κ bound by binder l) = cylindric substitution σ^κ_l(φ) = fun g => φ(g[κ↦g(l)])

These are not mere analogies: H&K's assignment update g[n↦x] IS the cylindric set algebra's coordinate update, and their quantifier scope ∃x.φ(g[n↦x]) IS cylindrification cₙ(φ).

theorem Semantics.Reference.Binding.binding_eq_resolve {E : Type} (κ l : ℕ) (φ : Core.Assignment E → Prop) (g : Core.Assignment E) : φ (Function.update g κ (g l)) = Intensional.Variables.resolve κ l φ g

Binding links pronoun κ to binder l by substituting g(l) for g(κ).

After binding, g(κ) = g(l), which is the diagonal element Dκl. The semantic effect on a predicate φ is φ(g[κ↦g(l)]), which is cylindric substitution σ^κ_l(φ).

theorem Semantics.Reference.Binding.binding_establishes_diagonal {E : Type} (κ l : ℕ) (g : Core.Assignment E) (h : κ ≠ l) : Intensional.Variables.diag κ l (Function.update g κ (g l))

After binding, the bound pronoun and its binder agree: (g[κ↦g(l)])(κ) = (g[κ↦g(l)])(l). This is the diagonal condition Dκl that cylindric substitution enforces.