Nominal denotations

A pronoun, a definite description, a demonstrative and a bound variable are one kind of thing: a presuppositional, context-relative individual denotation, differing only in the selector that chooses the individual (the assignment value, the iota, the demonstratum) and in the intrinsic presupposition (φ-features, uniqueness, deixis), as Büring argues. A Nominal is that common shape. Resolving it against a scope is presupOfReferent of the selector at a context (Nominal.resolve), so a definite built from presupOfReferent is a resolved Nominal.ofReferent by rfl (ofReferent_resolve), and the full denotation restricts the resolved one to where the intrinsic presupposition holds (Nominal.toTrivalent), which is where a pronoun's φ-features project. A character is the total nominal with no presupposition (Character.toNominal), and it is directly referential exactly when that nominal's selector is rigid at every context (Character.isDirectlyReferential_iff). Nominal Ctx W is the presupposition-projecting partiality monad, lawful (instLawfulMonad): bind threads the partial referent and projects the continuation's presupposition through definedness of the head, so a re-selection such as possessive-of composes as a Kleisli arrow while the head's presupposition rides along.

Implementation notes

The selector is Option-valued against a context; the dynamic case, where a selector returns a family of referents, is the functor-parameterised generalisation of this signature and is left to the first dynamic consumer that needs it.

References

• [Bur12]
• [HK98]

structure Reference.Nominal (Ctx : Type u_1) (W : Type u_2) (E : Type u_3) : Type (max (max u_1 u_2) u_3)

A presuppositional, context-relative individual denotation.

presup is the intrinsic presupposition beyond definedness — φ-features for a pronoun, deixis for a demonstrative, vacuous for a definite (whose only presupposition is that the selector is defined). selector is the partial choice of referent (g i, ι, the demonstratum) at a context and world.

• presup : Ctx → W → Prop

  Intrinsic presupposition beyond definedness (φ-features, deixis).

• selector : Ctx → W → Option E

  The partial referent selector.

def Reference.Nominal.ofReferent {W : Type u_2} {E : Type u_3} (referent : W → Option E) : Nominal Unit W E

The simplest nominal is a context-free referent selector with no intrinsic presupposition, a bare iota or definite. (ofReferent r).resolve scope ⟨⟩ unfolds to presupOfReferent r scope, so any presupOfReferent-built denotation is an ofReferent resolved (ofReferent_resolve).

Equations

• Reference.Nominal.ofReferent referent = { presup := fun (x : Unit) (x_1 : W) => True, selector := fun (x : Unit) => referent }

noncomputable def Reference.Nominal.resolve {Ctx : Type u_1} {W : Type u_2} {E : Type u_3} (nd : Nominal Ctx W E) (scope : E → W → Prop) (c : Ctx) : W → SignType

Resolving a nominal against a scope at context c gives the trivalent proposition defined where a referent is selected and applying scope to it there. It is presupOfReferent over nd.selector c, so any presupOfReferent-built denotation is a resolve, by rfl.

Equations

• nd.resolve scope c = Presupposition.presupOfReferent (nd.selector c) scope

theorem Reference.Nominal.ofReferent_resolve {W : Type u_2} {E : Type u_3} (referent : W → Option E) (scope : E → W → Prop) : (ofReferent referent).resolve scope PUnit.unit = Presupposition.presupOfReferent referent scope

An ofReferent resolved is exactly the canonical presupOfReferent — the bridge every definite denotation folds across.

noncomputable def Reference.Nominal.toTrivalent {Ctx : Type u_1} {W : Type u_2} {E : Type u_3} (nd : Nominal Ctx W E) (scope : E → W → Prop) (c : Ctx) : W → SignType

The full denotation is resolve restricted to where the intrinsic presupposition holds, the two presuppositions conjoined. For a definite the intrinsic presupposition is vacuous, so toTrivalent and resolve agree; for a pronoun the conjoined presupposition is where the φ-features project.

Equations

• nd.toTrivalent scope c = {w : W | nd.presup c w}.indicator (nd.resolve scope c)

@[simp]

theorem Reference.Nominal.resolve_eq_zero_iff {Ctx : Type u_1} {W : Type u_2} {E : Type u_3} {nd : Nominal Ctx W E} {scope : E → W → Prop} {c : Ctx} {w : W} : nd.resolve scope c w = 0 ↔ nd.selector c w = none

@[simp]

theorem Reference.Nominal.toTrivalent_eq_zero_iff {Ctx : Type u_1} {W : Type u_2} {E : Type u_3} {nd : Nominal Ctx W E} {scope : E → W → Prop} {c : Ctx} {w : W} : nd.toTrivalent scope c w = 0 ↔ nd.presup c w → nd.selector c w = none

Monad structure

Nominal Ctx W is the presupposition-projecting partiality monad: bind threads the partial referent (Option.bind) and accumulates presuppositions, projecting the continuation's presupposition through definedness of the head (Option.elim). This is what lets a re-selection (e.g. possessive-of) compose as a Kleisli arrow while a head's intrinsic presupposition (φ-features, deixis) rides along.

@[instance_reducible]

instance Reference.Nominal.instMonad {Ctx : Type u_1} {W : Type u_2} : Monad (Nominal Ctx W)

Equations

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

theorem Reference.Nominal.ext {Ctx : Type u_1} {W : Type u_2} {E : Type u_3} {nd₁ nd₂ : Nominal Ctx W E} (hp : nd₁.presup = nd₂.presup) (hs : nd₁.selector = nd₂.selector) : nd₁ = nd₂

A Nominal is determined by its presupposition and its selector.

theorem Reference.Nominal.ext_iff {Ctx : Type u_1} {W : Type u_2} {E : Type u_3} {nd₁ nd₂ : Nominal Ctx W E} : nd₁ = nd₂ ↔ nd₁.presup = nd₂.presup ∧ nd₁.selector = nd₂.selector

@[simp]

theorem Reference.Nominal.pure_selector {Ctx : Type u_1} {W : Type u_2} {α : Type u} (a : α) (c : Ctx) (w : W) : (pure a).selector c w = some a

@[simp]

theorem Reference.Nominal.pure_presup {Ctx : Type u_1} {W : Type u_2} {α : Type u} (a : α) (c : Ctx) (w : W) : (pure a).presup c w = True

@[simp]

theorem Reference.Nominal.bind_selector {Ctx : Type u_1} {W : Type u_2} {α β : Type u} (nd : Nominal Ctx W α) (k : α → Nominal Ctx W β) (c : Ctx) (w : W) : (nd >>= k).selector c w = (nd.selector c w).bind fun (e : α) => (k e).selector c w

@[simp]

theorem Reference.Nominal.bind_presup {Ctx : Type u_1} {W : Type u_2} {α β : Type u} (nd : Nominal Ctx W α) (k : α → Nominal Ctx W β) (c : Ctx) (w : W) : (nd >>= k).presup c w = (nd.presup c w ∧ (nd.selector c w).elim True fun (e : α) => (k e).presup c w)

instance Reference.Nominal.instLawfulMonad {Ctx : Type u_1} {W : Type u_2} : LawfulMonad (Nominal Ctx W)

In the monad laws left identity feeds a pure referent to its continuation, right identity re-selects by pure, and associativity is what makes possessive nesting (John's mother's friend) free.

Characters as nominals

def Reference.Character.toNominal {C : Type u_1} {W : Type u_2} {E : Type u_3} (χ : Character C W E) : Nominal C W E

A character is a nominal denotation that is total and has no presupposition.

Equations

• χ.toNominal = { presup := fun (x : C) (x_1 : W) => True, selector := fun (c : C) (w : W) => some (χ c w) }

@[simp]

theorem Reference.Character.toNominal_presup {C : Type u_1} {W : Type u_2} {E : Type u_3} (χ : Character C W E) (c : C) (w : W) : χ.toNominal.presup c w = True

@[simp]

theorem Reference.Character.toNominal_selector {C : Type u_1} {W : Type u_2} {E : Type u_3} (χ : Character C W E) (c : C) (w : W) : χ.toNominal.selector c w = some (χ c w)

theorem Reference.Character.isDirectlyReferential_iff {C : Type u_1} {W : Type u_2} {E : Type u_3} (χ : Character C W E) : χ.IsDirectlyReferential ↔ ∀ (c : C), IsRigid (χ.toNominal.selector c)

A character is directly referential iff its nominal's selector is rigid at every context, so that the referent does not vary with the world of evaluation.