Documentation

Studies.Charlow2018

Charlow 2018: a modular theory of pronouns and binding #

The standard theory of pronouns ([HK98]) makes every meaning depend on an assignment and composes by handing one assignment to both daughters. [Cha18] factors this into two operations: a lift ρ x := λg. x for meanings that do not depend on the assignment, and an application m ⊛ n := λg. m g (n g) used only where it is needed. Together they make assignment-dependent meanings an applicative functor. A flattener μ m := λg. m g g for pronouns whose value is an intension then makes them a monad. These are the pure, <*> and joinM of Lean's reader monad, so the laws the paper lists are the reader monad's own. Abstraction becomes an ordinary operation on meanings where the standard rule can only have it as a special rule, and paycheck pronouns and binding reconstruction follow from pronouns whose values are intensions.

Those analyses store intensions in assignments. Assignments that can store every intension exist only over a one-element domain, by Cantor's diagonal argument. This is the difficulty the paper cites in section 5, whose type-homogeneous assignments avoid it: two composed reader applicatives derive the paycheck reading with no flattener. The pronouns of variable-free semantics ([Jac99b]) use the same applicative at the entity type.

Main results #

Implementation notes #

ρ, ⊛ and μ are not defined here: they are pure, <*> and joinM of ReaderM (Assignment E), and the composition of two applicatives (Fig. 5) is mathlib's Functor.Comp. For section 4, G is an abstract type of assignments with lookups for individual variables and for variables over individual concepts, and a shift g^{i→x} for each; each derivation assumes only the laws it uses, for the one intension it stores. As in the paper, likes x y is "y likes x".

TODO #

References #

Abstraction under the standard theory #

The standard rule interprets a branching node by giving both daughters the same assignment, ⟦α β⟧ := λg. ⟦α⟧ g (⟦β⟧ g) (6). Binding needs the sister of Λᵢ evaluated at shifted assignments, which the rule never supplies.

source
theorem Charlow2018.not_exists_abstraction_denotation {E : Type} [Nontrivial E] (i : ℕ) :
¬∃ (L : Assignment E → Prop → E → Prop), ∀ (α : Assignment E → Prop), (fun (g : Assignment E) => L g (α g)) = HeimKratzer.lambdaAbsG i α

No denotation for Λᵢ binds under the standard rule (section 2.2): whatever L is, λg. L g (⟦α⟧ g) sees ⟦α⟧ only at g, while binding needs λg. λx. ⟦α⟧ g^{i→x}.

The reader applicative #

The lift ρ (11) and application ⊛ (12) are the pure and <*> of the reader monad, and the four laws of section 3.3 are its LawfulApplicative instance. Abstraction is the operation Λᵢ f := λg. λx. f g^{i→x} (13), lambdaAbsG.

Applicatives elsewhere in semantics #

source
theorem Charlow2018.hamblin_seq {α β : Type} (m : Set (α → β)) (n : Set α) :
m <*> n = {b : β | ∃ f ∈ m, ∃ x ∈ n, f x = b}

Hamblin's pointwise application {f x | f ∈ m, x ∈ n} (15) is the <*> of sets.

The flattener #

A pronoun whose value is an intension has type g → g → e (18). The flattener μ m := λg. m g g (19) is the reader monad's joinM. Section 4.3 states the monad laws with ρ, ⊛ and μ; they hold in every lawful monad.

source
theorem Charlow2018.joinM_joinM {M : Type → Type} [Monad M] [LawfulMonad M] {α : Type} (m : M (M (M α))) :
joinM (joinM m) = joinM (pure joinM <*> m)

Associativity: μ ∘ μ = λm. μ (ρ μ ⊛ m).

source
theorem Charlow2018.joinM_pure_seq_pure {M : Type → Type} [Monad M] [LawfulMonad M] {α : Type} (m : M α) :
joinM (pure pure <*> m) = m

Identity: λm. μ (ρ ρ ⊛ m) = λm. m; the other half, μ ∘ ρ = id, is joinM_pure.

Higher-order variables #

For the analyses of section 4 an assignment values both individual variables and variables over individual concepts. Here G is a type of assignments, ind i and con i look up variable i of each sort, and shift i x and shiftCon i n are the shifted assignments g^{i→x}.

source
def Charlow2018.abstraction {G α β : Type} (shift : α → G → G) (f : ReaderM G β) :
ReaderM G (α → β)

Abstraction Λᵢ f := λg. λx. f g^{i→x} (13), given the shift x ↦ g^{i→x}.

Equations
Instances For
    source
    theorem Charlow2018.paycheck {E G : Type} (ind : ℕ → ReaderM G E) (con : ℕ → ReaderM G (ReaderM G E)) (shift : ℕ → E → G → G) (likes : E → E → Prop) (mom : E → E) (b : E) (g : G) (hg : con 1 g = pure mom <*> ind 0) (hcon : ∀ (x : E) (g : G), con 1 (shift 0 x g) = con 1 g) (hind : ∀ (x : E) (g : G), ind 0 (shift 0 x g) = x) :
    (abstraction (shift 0) (pure likes <*> joinM (con 1) <*> ind 0) <*> pure b) g = likes (mom b) b

    The paycheck reading (Fig. 6): Bill Λ₀ t₀ likes her₁, with her₁ anaphoric to an intension and flattened by μ. If the input assignment gives variable 1 the intension of his₀ mom, the sentence says that Bill likes Bill's mom.

    source
    theorem Charlow2018.reconstruction {E G : Type} (ind : ℕ → ReaderM G E) (con : ℕ → ReaderM G (ReaderM G E)) (shift : ℕ → E → G → G) (shiftCon : ℕ → ReaderM G E → G → G) (likes : E → E → Prop) (mom : E → E) (everyBoy : (E → Prop) → Prop) (g : G) (hstore : ∀ (g : G), con 1 (shiftCon 1 (pure mom <*> ind 0) g) = pure mom <*> ind 0) (hcon : ∀ (x : E) (g : G), con 1 (shift 0 x g) = con 1 g) (hind : ∀ (x : E) (g : G), ind 0 (shift 0 x g) = x) :
    (abstraction (shiftCon 1) (pure everyBoy <*> abstraction (shift 0) (pure likes <*> joinM (con 1) <*> ind 0)) <*> pure (pure mom <*> ind 0)) g = everyBoy fun (x : E) => likes (mom x) x

    Binding reconstruction (Fig. 7): [his₀ mom] Λ₁ every boy Λ₀ t₀ likes t₁. The fronted phrase's intension is stored at variable 1, the trace t₁ is flattened by μ, and the sentence says that every boy likes his own mom.

    source
    theorem Charlow2018.subsingleton_of_forall_store {E G : Type} (con : ℕ → ReaderM G (ReaderM G E)) (shiftCon : ℕ → ReaderM G E → G → G) [Nonempty G] (i : ℕ) (h : ∀ (n : ReaderM G E) (g : G), con i (shiftCon i n g) = n) :
    Subsingleton E

    Assignments that can store every intension exist only over a one-element domain. Storing makes the lookup con i a surjection from G onto G → E, which Cantor's diagonal argument rules out once E has two elements. This is why the laws above store only the intension a derivation needs, and the difficulty section 5.1 cites for such assignments.

    Type-homogeneous assignments #

    Section 5 gives each type r its own assignments, g_r := ℕ → r, which is Assignment r. A meaning that depends on assignments of two sorts lives in the composite of two reader applicatives.

    source
    @[reducible, inline]
    abbrev Charlow2018.ConceptThenIndividual (E : Type) :
    Type → Type

    Meanings that depend on an assignment of individual concepts and then on an assignment of individuals: the composite G_{G_e e} ∘ G_e of section 5.2.

    Equations
    Instances For
      source
      theorem Charlow2018.typed_paycheck {E : Type} (likes : E → E → Prop) (mom : E → E) (b : E) (g : Assignment (Assignment E → E)) (h : Assignment E) (hg : g 1 = fun (h : Assignment E) => mom (h 0)) :
      Functor.Comp.run (Functor.Comp.mk (HeimKratzer.lambdaAbsG 0 <$> ((pure likes <*> Functor.Comp.mk fun (g : Assignment (Assignment E → E)) (h : Assignment E) => g 1 h) <*> Functor.Comp.mk fun (x : Assignment (Assignment E → E)) (h : Assignment E) => h 0).run) <*> pure b) g h = likes (mom b) b

      The paycheck reading on type-homogeneous assignments (section 5.2): her₁ reads an intension from the outer assignment and evaluates it at the inner one, and Λ₀ binds the subject's trace in the inner layer. The meaning is λg. λh. likes (g₁ h^{0→b}) b, with no flattener.

      Variable-free pronouns #

      A variable-free pronoun is the identity λx. x (Fig. 8), composed with the same ρ and ⊛ at the entity type (section 6).