Composition modes

The composition modes of Heim and Kratzer, with the intensional application of von Fintel and Heim and the event identification of Kratzer, are typed binary operations: a mode of type Mode σ₁ σ₂ τ composes a left daughter of type σ₁ and a right daughter of type σ₂ into a mother of type τ. Functional application, intensional application and event identification come in two orders, the function or role head being the left or the right daughter. The types of two daughters select the mode they compose by (Ty.mode?), the first that applies in the order functional application, intensional application, predicate modification, event identification.

A mode denotes an operation on the denotation domains (Mode.eval): application, application to the rigid intension of the argument, the intersection of two predicates, and event identification. Under an applicative effect a mode composes the daughters' computations in their linear order (Mode.evalM), whichever daughter is the function. In any family of values indexed by the types, Mode.combine? composes two values by the mode their types select.

Main definitions

• HeimKratzer.Mode: the composition modes as typed binary operations.
• Montague.Ty.mode?: the mode two daughters' types select.
• HeimKratzer.Mode.eval, HeimKratzer.Mode.evalM: the denotation of a mode, pure and under an applicative effect.
• HeimKratzer.Mode.combine?: composition by the selected mode in a family of values.

Main results

• HeimKratzer.Mode.combine?_map: composing commutes with every map of families that commutes with the modes.

References

• [HK98]
• [vFH11]
• [Kra96]

inductive HeimKratzer.Mode : Montague.Ty → Montague.Ty → Montague.Ty → Type

The composition modes are the typed binary operations of functional application, with the function as either daughter, of intensional application, which applies a daughter expecting an intension to the rigid intension of its sister in either order ([vFH11]), of predicate modification, and of event identification of a role head and an eventuality predicate in either order ([Kra96]).

• functionalLeft {σ τ : Montague.Ty} : Mode (σ ⇒ τ) σ τ
• functionalRight {σ τ : Montague.Ty} : Mode σ (σ ⇒ τ) τ
• intensionalLeft {σ τ : Montague.Ty} : Mode (σ.intens ⇒ τ) σ τ
• intensionalRight {σ τ : Montague.Ty} : Mode σ (σ.intens ⇒ τ) τ
• predicateModification : Mode (Montague.Ty.e ⇒ Montague.Ty.t) (Montague.Ty.e ⇒ Montague.Ty.t) (Montague.Ty.e ⇒ Montague.Ty.t)
• eventIdentificationLeft : Mode (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t) (Montague.Ty.e ⇒ Montague.Ty.t) (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t)
• eventIdentificationRight : Mode (Montague.Ty.e ⇒ Montague.Ty.t) (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t) (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t)

def HeimKratzer.instDecidableEqMode.decEq {a✝ a✝¹ a✝² : Montague.Ty} (x✝ x✝¹ : Mode a✝ a✝¹ a✝²) : Decidable (x✝ = x✝¹)

Equations

• HeimKratzer.instDecidableEqMode.decEq HeimKratzer.Mode.functionalLeft HeimKratzer.Mode.functionalLeft = isTrue ⋯
• HeimKratzer.instDecidableEqMode.decEq HeimKratzer.Mode.functionalRight HeimKratzer.Mode.functionalRight = isTrue ⋯
• HeimKratzer.instDecidableEqMode.decEq HeimKratzer.Mode.intensionalLeft HeimKratzer.Mode.intensionalLeft = isTrue ⋯
• HeimKratzer.instDecidableEqMode.decEq HeimKratzer.Mode.intensionalRight HeimKratzer.Mode.intensionalRight = isTrue ⋯
• HeimKratzer.instDecidableEqMode.decEq HeimKratzer.Mode.predicateModification HeimKratzer.Mode.predicateModification = isTrue HeimKratzer.instDecidableEqMode.decEq._proof_5
• HeimKratzer.instDecidableEqMode.decEq HeimKratzer.Mode.eventIdentificationLeft HeimKratzer.Mode.eventIdentificationLeft = isTrue HeimKratzer.instDecidableEqMode.decEq._proof_6
• HeimKratzer.instDecidableEqMode.decEq HeimKratzer.Mode.eventIdentificationRight HeimKratzer.Mode.eventIdentificationRight = isTrue HeimKratzer.instDecidableEqMode.decEq._proof_7

@[instance_reducible]

instance HeimKratzer.instDecidableEqMode {a✝ a✝¹ a✝² : Montague.Ty} : DecidableEq (Mode a✝ a✝¹ a✝²)

Equations

• HeimKratzer.instDecidableEqMode = HeimKratzer.instDecidableEqMode.decEq

Selection by the daughters' types

def HeimKratzer.Mode.functionalLeft? (σ₁ σ₂ : Montague.Ty) : Option ((τ : Montague.Ty) × Mode σ₁ σ₂ τ)

Forward functional application applies when the left daughter is a function on the right one.

Equations

• HeimKratzer.Mode.functionalLeft? (σ ⇒ τ) x✝ = if h : σ = x✝ then some ⟨τ, h ▸ HeimKratzer.Mode.functionalLeft⟩ else none
• HeimKratzer.Mode.functionalLeft? x✝¹ x✝ = none

def HeimKratzer.Mode.functionalRight? (σ₁ σ₂ : Montague.Ty) : Option ((τ : Montague.Ty) × Mode σ₁ σ₂ τ)

Backward functional application applies when the right daughter is a function on the left one.

Equations

• HeimKratzer.Mode.functionalRight? x✝ (σ ⇒ τ) = if h : σ = x✝ then some ⟨τ, h ▸ HeimKratzer.Mode.functionalRight⟩ else none
• HeimKratzer.Mode.functionalRight? x✝¹ x✝ = none

def HeimKratzer.Mode.intensionalLeft? (σ₁ σ₂ : Montague.Ty) : Option ((τ : Montague.Ty) × Mode σ₁ σ₂ τ)

Intensional application applies when the left daughter expects the intension of the right one.

Equations

• HeimKratzer.Mode.intensionalLeft? (σ.intens ⇒ τ) x✝ = if h : σ = x✝ then some ⟨τ, h ▸ HeimKratzer.Mode.intensionalLeft⟩ else none
• HeimKratzer.Mode.intensionalLeft? x✝¹ x✝ = none

def HeimKratzer.Mode.intensionalRight? (σ₁ σ₂ : Montague.Ty) : Option ((τ : Montague.Ty) × Mode σ₁ σ₂ τ)

Intensional application applies when the right daughter expects the intension of the left one.

Equations

• HeimKratzer.Mode.intensionalRight? x✝ (σ.intens ⇒ τ) = if h : σ = x✝ then some ⟨τ, h ▸ HeimKratzer.Mode.intensionalRight⟩ else none
• HeimKratzer.Mode.intensionalRight? x✝¹ x✝ = none

def HeimKratzer.Mode.predicateModification? (σ₁ σ₂ : Montague.Ty) : Option ((τ : Montague.Ty) × Mode σ₁ σ₂ τ)

Predicate modification applies to two predicates.

Equations

• HeimKratzer.Mode.predicateModification? (Montague.Ty.e ⇒ Montague.Ty.t) (Montague.Ty.e ⇒ Montague.Ty.t) = some ⟨Montague.Ty.e ⇒ Montague.Ty.t, HeimKratzer.Mode.predicateModification⟩
• HeimKratzer.Mode.predicateModification? x✝¹ x✝ = none

def HeimKratzer.Mode.eventIdentification? (σ₁ σ₂ : Montague.Ty) : Option ((τ : Montague.Ty) × Mode σ₁ σ₂ τ)

Event identification applies to a role head and an eventuality predicate, in either order.

Equations

• One or more equations did not get rendered due to their size.
• HeimKratzer.Mode.eventIdentification? x✝¹ x✝ = none

def Montague.Ty.mode? (σ₁ σ₂ : Ty) : Option ((τ : Ty) × HeimKratzer.Mode σ₁ σ₂ τ)

σ₁.mode? σ₂ is the mode by which a left daughter of type σ₁ and a right daughter of type σ₂ compose, the first that applies of functional application (the left daughter as the function first), intensional application, predicate modification and event identification, and none when none does.

Equations

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

@[simp]

theorem HeimKratzer.Mode.mode?_fn_left (σ τ : Montague.Ty) : (σ ⇒ τ).mode? σ = some ⟨τ, functionalLeft⟩

A function type applies to an argument of its domain, the function on the left.

theorem HeimKratzer.Mode.functionalLeft?_self_fn (σ τ : Montague.Ty) : functionalLeft? σ (σ ⇒ τ) = none

No type is its own argument type, so a type never applies to a function type from itself.

@[simp]

theorem HeimKratzer.Mode.mode?_fn_right (σ τ : Montague.Ty) : σ.mode? (σ ⇒ τ) = some ⟨τ, functionalRight⟩

A function type applies to an argument of its domain, the function on the right.

@[simp]

theorem HeimKratzer.Mode.mode?_predicateModification : (Montague.Ty.e ⇒ Montague.Ty.t).mode? (Montague.Ty.e ⇒ Montague.Ty.t) = some ⟨Montague.Ty.e ⇒ Montague.Ty.t, predicateModification⟩

Two predicates compose by predicate modification.

Denotation

def HeimKratzer.Mode.eval {E W D : Type} {σ₁ σ₂ τ : Montague.Ty} : Mode σ₁ σ₂ τ → Montague.Ty.Domain E W σ₁ D → Montague.Ty.Domain E W σ₂ D → Montague.Ty.Domain E W τ D

A mode denotes application, application to the rigid intension of the argument, the intersection of two predicates, or event identification.

Equations

• HeimKratzer.Mode.functionalLeft.eval f x✝ = f x✝
• HeimKratzer.Mode.functionalRight.eval x✝ f = f x✝
• HeimKratzer.Mode.intensionalLeft.eval f x✝ = f fun (x : W) => x✝
• HeimKratzer.Mode.intensionalRight.eval x✝ f = f fun (x : W) => x✝
• HeimKratzer.Mode.predicateModification.eval p q = Modifier.intersective p q
• HeimKratzer.Mode.eventIdentificationLeft.eval f p = ArgumentStructure.eventIdentification f p
• HeimKratzer.Mode.eventIdentificationRight.eval p f = ArgumentStructure.eventIdentification f p

def HeimKratzer.Mode.evalM {E W D : Type} {σ₁ σ₂ τ : Montague.Ty} {M : Type → Type} [Applicative M] (m : Mode σ₁ σ₂ τ) (a : M (Montague.Ty.Domain E W σ₁ D)) (b : M (Montague.Ty.Domain E W σ₂ D)) : M (Montague.Ty.Domain E W τ D)

The denotation of a mode under an applicative effect, which runs the left daughter's computation first.

Equations

• m.evalM a b = m.eval <$> a <*> b

@[simp]

theorem HeimKratzer.Mode.evalM_id {E W D : Type} {σ₁ σ₂ τ : Montague.Ty} (m : Mode σ₁ σ₂ τ) (a : Montague.Ty.Domain E W σ₁ D) (b : Montague.Ty.Domain E W σ₂ D) : m.evalM a b = m.eval a b

At the identity effect a mode denotes its pure denotation.

Composition in a family of values

def HeimKratzer.Mode.combine? {V : Montague.Ty → Type u_1} (op : {σ₁ σ₂ τ : Montague.Ty} → Mode σ₁ σ₂ τ → V σ₁ → V σ₂ → V τ) (d₁ d₂ : (ty : Montague.Ty) × V ty) : Option ((ty : Montague.Ty) × V ty)

Two values compose by the mode their types select, interpreted by op, and not at all when no mode applies.

Equations

• HeimKratzer.Mode.combine? op d₁ d₂ = Option.map (fun (p : (τ : Montague.Ty) × HeimKratzer.Mode d₁.fst d₂.fst τ) => ⟨p.fst, op p.snd d₁.snd d₂.snd⟩) (d₁.fst.mode? d₂.fst)

@[simp]

theorem HeimKratzer.Mode.combine?_map_fst {V : Montague.Ty → Type u_1} (op : {σ₁ σ₂ τ : Montague.Ty} → Mode σ₁ σ₂ τ → V σ₁ → V σ₂ → V τ) (d₁ d₂ : (ty : Montague.Ty) × V ty) : Option.map (fun (x : (ty : Montague.Ty) × V ty) => x.fst) (combine? (fun {σ₁ σ₂ τ : Montague.Ty} => op) d₁ d₂) = Option.map (fun (x : (τ : Montague.Ty) × Mode d₁.fst d₂.fst τ) => x.fst) (d₁.fst.mode? d₂.fst)

The type of a composed value is the type the mode selects, a function of the daughters' types alone.

theorem HeimKratzer.Mode.combine?_map {V : Montague.Ty → Type u_1} {V' : Montague.Ty → Type u_2} {op : {σ₁ σ₂ τ : Montague.Ty} → Mode σ₁ σ₂ τ → V σ₁ → V σ₂ → V τ} {op' : {σ₁ σ₂ τ : Montague.Ty} → Mode σ₁ σ₂ τ → V' σ₁ → V' σ₂ → V' τ} {h : {ty : Montague.Ty} → V ty → V' ty} (hh : ∀ {σ₁ σ₂ τ : Montague.Ty} (m : Mode σ₁ σ₂ τ) (a : V σ₁) (b : V σ₂), h (op m a b) = op' m (h a) (h b)) (d₁ d₂ : (ty : Montague.Ty) × V ty) : Option.map (fun (d : (ty : Montague.Ty) × V ty) => ⟨d.fst, h d.snd⟩) (combine? (fun {σ₁ σ₂ τ : Montague.Ty} => op) d₁ d₂) = combine? (fun {σ₁ σ₂ τ : Montague.Ty} => op') ⟨d₁.fst, h d₁.snd⟩ ⟨d₂.fst, h d₂.snd⟩

Composing commutes with every map of families that commutes with the modes.

@[simp]

theorem HeimKratzer.Mode.combine?_fn_left {V : Montague.Ty → Type u_1} (op : {σ₁ σ₂ τ : Montague.Ty} → Mode σ₁ σ₂ τ → V σ₁ → V σ₂ → V τ) {σ τ : Montague.Ty} (f : V (σ ⇒ τ)) (a : V σ) : combine? (fun {σ₁ σ₂ τ : Montague.Ty} => op) ⟨σ ⇒ τ, f⟩ ⟨σ, a⟩ = some ⟨τ, op functionalLeft f a⟩

@[simp]

theorem HeimKratzer.Mode.combine?_fn_right {V : Montague.Ty → Type u_1} (op : {σ₁ σ₂ τ : Montague.Ty} → Mode σ₁ σ₂ τ → V σ₁ → V σ₂ → V τ) {σ τ : Montague.Ty} (a : V σ) (f : V (σ ⇒ τ)) : combine? (fun {σ₁ σ₂ τ : Montague.Ty} => op) ⟨σ, a⟩ ⟨σ ⇒ τ, f⟩ = some ⟨τ, op functionalRight a f⟩

@[simp]

theorem HeimKratzer.Mode.combine?_predicateModification {V : Montague.Ty → Type u_1} (op : {σ₁ σ₂ τ : Montague.Ty} → Mode σ₁ σ₂ τ → V σ₁ → V σ₂ → V τ) (p q : V (Montague.Ty.e ⇒ Montague.Ty.t)) : combine? (fun {σ₁ σ₂ τ : Montague.Ty} => op) ⟨Montague.Ty.e ⇒ Montague.Ty.t, p⟩ ⟨Montague.Ty.e ⇒ Montague.Ty.t, q⟩ = some ⟨Montague.Ty.e ⇒ Montague.Ty.t, op predicateModification p q⟩