structure Semantics.Reference.Binding.InterpState (m : Montague.Model) : Type

Semantic interpretation state: current assignment + pending abstractions.

• assignment : Montague.Variables.Assignment m
• abstractionStack : List ℕ

def Semantics.Reference.Binding.InterpState.initial {m : Montague.Model} (g : Montague.Variables.Assignment m) : InterpState m

Initial interpretation state with a given assignment.

Equations

• Semantics.Reference.Binding.InterpState.initial g = { assignment := g, abstractionStack := [] }

def Semantics.Reference.Binding.InterpState.pushAbstraction {m : Montague.Model} (state : InterpState m) (idx : ℕ) : InterpState m

Push an abstraction index onto the stack.

Equations

• state.pushAbstraction idx = { assignment := state.assignment, abstractionStack := idx :: state.abstractionStack }

def Semantics.Reference.Binding.interpretBoundPronoun {m : Montague.Model} (state : InterpState m) (varIdx : ℕ) : m.Entity

Interpret a bound pronoun: read from assignment at the variable index.

Equations

• Semantics.Reference.Binding.interpretBoundPronoun state varIdx = state.assignment varIdx

def Semantics.Reference.Binding.interpretBinder {m : Montague.Model} {τ : Montague.Ty} (varIdx : ℕ) (body : InterpState m → m.interpTy τ) (state : InterpState m) : m.interpTy (Montague.Ty.e ⇒ τ)

Interpret a binder: create a function that updates the assignment.

Equations

• Semantics.Reference.Binding.interpretBinder varIdx body state x = body { assignment := state.assignment.update varIdx x, abstractionStack := state.abstractionStack }

def Semantics.Reference.Binding.bindingWellFormed {m : Montague.Model} (state : InterpState m) (varIdx : ℕ) : Bool

A binding is semantically well-formed if the binder's scope includes the bindee.

Equations

• Semantics.Reference.Binding.bindingWellFormed state varIdx = decide (varIdx ∈ state.abstractionStack)

def Semantics.Reference.Binding.interpretBindingConfig {m : Montague.Model} (bc : Interfaces.BindingSemantics.BindingConfig) (_g : Montague.Variables.Assignment m) : Bool

Interpret a binding configuration as a semantic check.

Equations

• Semantics.Reference.Binding.interpretBindingConfig bc _g = bc.wellFormed

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 {m : Montague.Model} (n : ℕ) (body : m.Entity → Bool) (binder : m.Entity) (g : Montague.Variables.Assignment m) : Bool

H&K interpretation of binding.

Equations

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

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

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 {m : Montague.Model} (n : ℕ) (body : m.Entity → m.Entity → Bool) (binder : m.Entity) (g : Montague.Variables.Assignment m) : body (g.update n binder n) (g.update 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)

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 → Bool) : cpsTransform f k e = k (f e)

CPS transform preserves binding semantics.

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

W is the semantic content of binding in both frameworks.

structure Semantics.Reference.Binding.EvalContext (Entity : Type) : Type

Evaluation context tracks which binders are "active".

• activeBinders : List Entity
• position : ℕ

def Semantics.Reference.Binding.instReprEvalContext.repr {Entity✝ : Type} [Repr Entity✝] : EvalContext Entity✝ → ℕ → Std.Format

Equations

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

instance Semantics.Reference.Binding.instReprEvalContext {Entity✝ : Type} [Repr Entity✝] : Repr (EvalContext Entity✝)

Equations

• Semantics.Reference.Binding.instReprEvalContext = { reprPrec := Semantics.Reference.Binding.instReprEvalContext.repr }

def Semantics.Reference.Binding.canBind {Entity : Type} [DecidableEq Entity] (ctx : EvalContext Entity) (binder : Entity) : Bool

A pronoun can be bound only if its binder is active.

Equations

• Semantics.Reference.Binding.canBind ctx binder = decide (binder ∈ ctx.activeBinders)

def Semantics.Reference.Binding.crossover (pronounPos binderPos : ℕ) : Bool

Crossover: pronoun position < binder position → binding fails.

Equations

• Semantics.Reference.Binding.crossover pronounPos binderPos = decide (pronounPos < binderPos)

def Semantics.Reference.Binding.strictReading {Entity : Type} (vp : Entity → Entity → Bool) (antecedent ellipsisSite : Entity) : Bool

Strict reading: pronoun resolves to original antecedent.

Equations

• Semantics.Reference.Binding.strictReading vp antecedent ellipsisSite = vp ellipsisSite antecedent

def Semantics.Reference.Binding.sloppyReading {Entity : Type} (vp : Entity → Entity → Bool) (ellipsisSite : Entity) : Bool

Sloppy reading: pronoun re-binds to new subject.

Equations

• Semantics.Reference.Binding.sloppyReading vp ellipsisSite = Semantics.Reference.Binding.W vp ellipsisSite

structure Semantics.Reference.Binding.VPEAmbiguity (Entity : Type) : Type

VPE ambiguity: both readings available.

• vp : Entity → Entity → Bool
• antecedentSubj : Entity
• ellipsisSite : Entity

def Semantics.Reference.Binding.VPEAmbiguity.strictValue {Entity : Type} (a : VPEAmbiguity Entity) : Bool

Equations

• a.strictValue = Semantics.Reference.Binding.strictReading a.vp a.antecedentSubj a.ellipsisSite

def Semantics.Reference.Binding.VPEAmbiguity.sloppyValue {Entity : Type} (a : VPEAmbiguity Entity) : Bool

Equations

• a.sloppyValue = Semantics.Reference.Binding.sloppyReading a.vp a.ellipsisSite

Binding as cylindric algebra substitution

The connection between Heim & Kratzer's binding mechanism and cylindric algebra (@cite{henkin-monk-tarski-1971}):

• 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.binder_scope_is_existsClosure {m : Montague.Model} (n : ℕ) (body : InterpState m → Prop) (state : InterpState m) : (∃ (x : m.Entity), body { assignment := state.assignment.update n x, abstractionStack := state.abstractionStack }) ↔ Montague.Variables.existsClosure n (fun (g : Montague.Variables.Assignment m) => body { assignment := g, abstractionStack := state.abstractionStack }) state.assignment

Existential quantifier scope at index n is cylindrification.

(∃n.φ)(g) = ∃x. φ(g[n↦x]) where the binder at n creates the scope via interpretBinder.

theorem Semantics.Reference.Binding.binding_eq_resolve {m : Montague.Model} (κ l : ℕ) (φ : Montague.Variables.Assignment m → Prop) (g : Montague.Variables.Assignment m) : φ (g.update κ (g l)) = Montague.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 {m : Montague.Model} (κ l : ℕ) (g : Montague.Variables.Assignment m) (h : κ ≠ l) : Montague.Variables.diag κ l (g.update κ (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.