Partial interpretation

This file is Heim and Kratzer's composition engine on partial denotations. A function denotes a partial function, mathlib's PFun, whose domain is the definedness condition the book attaches to a lexical entry, and a node denotes a Part value of its type, defined when its daughters are and the function among them is defined at its argument. The engine evaluates the term a tree translates to (Tree.translate), so it composes by the same modes as the total engine (Mode.evalPartial); a trace denotes the value of its index and a binder abstracts over its index, the abstract being a partial function that is undefined wherever the body is. Predicate Abstraction therefore needs no distributor.

The book's distinction between uninterpretability and presupposition failure (§4.4.4) is the difference between the engine returning no denotation and returning an undefined one: Uninterpretable is decided by the types of the leaves alone (uninterpretable_congr), and PresupFailure asks after the denotations. The definite article is the book's Fregean entry (the), defined on the predicates true of exactly one individual.

Main declarations

• Ty.PDomain and PDenotation are the partial domains and denotations.
• Mode.evalPartial and Term.evalPartial are the partial denotations of a mode and of a term, and Partial.interp the engine, evaluating a tree's term.
• Partial.Uninterpretable and Partial.PresupFailure are the two ways of lacking a value, and Partial.interp_map_fst_congr shows the first depends on the leaves' types alone.
• Partial.the is the definite article, with Partial.the_dom its definedness condition.
• Ty.Lifts and Denotation.Lifts relate a total denotation to a partial one lifting it, and Partial.interp_lifts shows that on a lexicon lifting a total one the partial engine's values lift the pure engine's, every mode preserving the lift (Mode.lifts_evalPartial), so such a lexicon has no presupposition failure (Partial.not_presupFailure_of_lifts). Ty.Domain.toPartial is the lift at a first-order type.

References

• [HK98]

@[reducible, inline]

abbrev Montague.Ty.PDomain (E W : Type) (ty : Ty) (D : Type := ℝ) : Type

Partial denotation domains, as Ty.Domain but with functions the partial functions →., whose domain is a lexical entry's definedness condition.

Equations

• Montague.Ty.PDomain E W Montague.Ty.e D = E
• Montague.Ty.PDomain E W Montague.Ty.t D = Prop
• Montague.Ty.PDomain E W Montague.Ty.d D = D
• Montague.Ty.PDomain E W Montague.Ty.n D = ℕ
• Montague.Ty.PDomain E W Montague.Ty.v D = Empty
• Montague.Ty.PDomain E W Montague.Ty.s D = Empty
• Montague.Ty.PDomain E W (a ⇒ b) D = (Montague.Ty.PDomain E W a D →. Montague.Ty.PDomain E W b D)
• Montague.Ty.PDomain E W a.intens D = (W →. Montague.Ty.PDomain E W a D)

@[reducible, inline]

abbrev Montague.PDenotation (E W : Type) (D : Type := ℝ) : Type

A partial denotation is a semantic type with a possibly undefined value in its partial domain.

Equations

• Montague.PDenotation E W D = ((ty : Montague.Ty) × Part (Montague.Ty.PDomain E W ty D))

Partial denotations of the modes and terms

def HeimKratzer.Mode.evalPartial {E W D : Type} {σ₁ σ₂ τ : Montague.Ty} : Mode σ₁ σ₂ τ → Part (Montague.Ty.PDomain E W σ₁ D) → Part (Montague.Ty.PDomain E W σ₂ D) → Part (Montague.Ty.PDomain E W τ D)

The partial denotation of a mode, defined where both daughters are and the function or role head among them is defined at its argument.

Equations

• One or more equations did not get rendered due to their size.
• HeimKratzer.Mode.functionalLeft.evalPartial f x✝ = f.bind fun (fv : Montague.Ty.PDomain E W (σ₂ ⇒ τ) D) => x✝.bind fv
• HeimKratzer.Mode.functionalRight.evalPartial x✝ f = f.bind fun (fv : Montague.Ty.PDomain E W (σ₁ ⇒ τ) D) => x✝.bind fv

def HeimKratzer.Term.evalPartial {E W D : Type} {K : Montague.Ty → Type u_1} (I : {ty : Montague.Ty} → K ty → Part (Montague.Ty.PDomain E W ty D)) (g : Assignment E) {ty : Montague.Ty} : Term K ty → Part (Montague.Ty.PDomain E W ty D)

The partial denotation of a term under a partial interpretation of the constants and an assignment; an abstraction is the partial function undefined wherever its body is.

Equations

• One or more equations did not get rendered due to their size.
• HeimKratzer.Term.evalPartial I g (HeimKratzer.Term.const c) = I c
• HeimKratzer.Term.evalPartial I g (HeimKratzer.Term.var n) = Part.some (g n)

Composition of defined daughters

These are rewriting lemmas rather than simp lemmas, since the reducible Ty.PDomain keys a concrete domain and a variable one differently for simp's index.

theorem HeimKratzer.Partial.combine?_forward {E W D : Type} {σ τ : Montague.Ty} (f : Montague.Ty.PDomain E W (σ ⇒ τ) D) (a : Montague.Ty.PDomain E W σ D) : Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} => Mode.evalPartial) ⟨σ ⇒ τ, Part.some f⟩ ⟨σ, Part.some a⟩ = some ⟨τ, f a⟩

A binary node whose left daughter is a defined function over the right daughter's type applies it forward.

theorem HeimKratzer.Partial.combine?_backward {E W D : Type} {σ τ : Montague.Ty} (a : Montague.Ty.PDomain E W σ D) (f : Montague.Ty.PDomain E W (σ ⇒ τ) D) : Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} => Mode.evalPartial) ⟨σ, Part.some a⟩ ⟨σ ⇒ τ, Part.some f⟩ = some ⟨τ, f a⟩

A binary node whose right daughter is a defined function over the left daughter's type applies it backward.

theorem HeimKratzer.Partial.combine?_predicateModification {E W D : Type} (P Q : Montague.Ty.PDomain E W (Montague.Ty.e ⇒ Montague.Ty.t) D) : Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} => Mode.evalPartial) ⟨Montague.Ty.e ⇒ Montague.Ty.t, Part.some P⟩ ⟨Montague.Ty.e ⇒ Montague.Ty.t, Part.some Q⟩ = some ⟨Montague.Ty.e ⇒ Montague.Ty.t, Part.some fun (x : Montague.Ty.PDomain E W Montague.Ty.e D) => (P x).bind fun (a : Montague.Ty.PDomain E W Montague.Ty.t D) => Part.map (fun (b : Prop) => a ∧ b) (Q x)⟩

Two defined predicates compose by predicate modification, conjoined pointwise.

Tree interpretation

def HeimKratzer.Partial.valueAt {E W D : Type} (τ : Montague.Ty) : Option (Montague.PDenotation E W D) → Part (Montague.Ty.PDomain E W τ D)

The value of an interpreted daughter at the type τ, which is undefined where the daughter is uninterpretable or of another type.

Equations

• HeimKratzer.Partial.valueAt τ (some ⟨ty, v⟩) = if h : ty = τ then h ▸ v else Part.none
• HeimKratzer.Partial.valueAt τ none = Part.none

def HeimKratzer.Partial.interp {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (t : PhraseStructure.Tree C L) : Option (Montague.PDenotation E W D)

The partial denotation of a tree under an assignment is its term's partial denotation, with each word's partial denotation its constant. A terminal denotes what its leaf interpretation gives it, a binary node what the mode its daughters' types select composes, a trace the value of its index, and a binder the partial function abstracting over its index in the body.

Equations

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

@[simp]

theorem HeimKratzer.Partial.interp_terminal {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (c : C) (w : L) : interp lex g (PhraseStructure.Tree.terminal c w) = lex w

@[simp]

theorem HeimKratzer.Partial.interp_node_unary {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (c : C) (t : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.node c [t]) = interp lex g t

@[simp]

theorem HeimKratzer.Partial.interp_adjoin_unary {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (c : C) (t : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.adjoin c [t]) = interp lex g t

@[simp]

theorem HeimKratzer.Partial.interp_node_binary {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (c : C) (t₁ t₂ : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.node c [t₁, t₂]) = (interp lex g t₁).bind fun (d₁ : Montague.PDenotation E W D) => (interp lex g t₂).bind fun (d₂ : Montague.PDenotation E W D) => Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} => Mode.evalPartial) d₁ d₂

@[simp]

theorem HeimKratzer.Partial.interp_adjoin_binary {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (c : C) (t₁ t₂ : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.adjoin c [t₁, t₂]) = (interp lex g t₁).bind fun (d₁ : Montague.PDenotation E W D) => (interp lex g t₂).bind fun (d₂ : Montague.PDenotation E W D) => Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} => Mode.evalPartial) d₁ d₂

@[simp]

theorem HeimKratzer.Partial.interp_trace {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (n : ℕ) (c : C) : interp lex g (PhraseStructure.Tree.trace n c) = some ⟨Montague.Ty.e, Part.some (g n)⟩

@[simp]

theorem HeimKratzer.Partial.interp_bind {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (n : ℕ) (c : C) (body : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.bind n c body) = Option.map (fun (d : Montague.PDenotation E W D) => ⟨Montague.Ty.e ⇒ d.fst, Part.some fun (x : Montague.Ty.PDomain E W Montague.Ty.e D) => valueAt d.fst (interp lex (Function.update g n x) body)⟩) (interp lex g body)

theorem HeimKratzer.Partial.interp_junk {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) {l : PhraseStructure.Tree.Label C L} {cs : List (PhraseStructure.Tree C L)} (h : ¬l.Licenses (List.map RoseTree.value cs)) : interp lex g (RoseTree.node l cs) = none

A node whose daughters its label does not license denotes nothing.

Uninterpretability and presupposition failure

def HeimKratzer.Partial.Uninterpretable {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (t : PhraseStructure.Tree C L) : Prop

A tree is uninterpretable when the engine assigns it no denotation.

Equations

• HeimKratzer.Partial.Uninterpretable lex g t = (HeimKratzer.Partial.interp lex g t = none)

def HeimKratzer.Partial.PresupFailure {E W D C : Type} {L : Type u_1} (lex : L → Option (Montague.PDenotation E W D)) (g : Assignment E) (t : PhraseStructure.Tree C L) : Prop

A tree is a presupposition failure when its denotation is undefined.

Equations

• HeimKratzer.Partial.PresupFailure lex g t = ∃ (d : Montague.PDenotation E W D), HeimKratzer.Partial.interp lex g t = some d ∧ ¬d.snd.Dom

theorem HeimKratzer.Partial.interp_map_fst_congr {E W D C : Type} {L : Type u_1} (lex lex' : L → Option (Montague.PDenotation E W D)) (g g' : Assignment E) (h : ∀ (w : L), Option.map (fun (x : Montague.PDenotation E W D) => x.fst) (lex w) = Option.map (fun (x : Montague.PDenotation E W D) => x.fst) (lex' w)) (t : PhraseStructure.Tree C L) : Option.map (fun (x : Montague.PDenotation E W D) => x.fst) (interp lex g t) = Option.map (fun (x : Montague.PDenotation E W D) => x.fst) (interp lex' g' t)

Whether a tree is interpretable, and at which type, depends only on the types of its leaves, [HK98]'s characterization of uninterpretability.

theorem HeimKratzer.Partial.uninterpretable_congr {E W D C : Type} {L : Type u_1} (lex lex' : L → Option (Montague.PDenotation E W D)) (g g' : Assignment E) (h : ∀ (w : L), Option.map (fun (x : Montague.PDenotation E W D) => x.fst) (lex w) = Option.map (fun (x : Montague.PDenotation E W D) => x.fst) (lex' w)) (t : PhraseStructure.Tree C L) : Uninterpretable lex g t ↔ Uninterpretable lex' g' t

Uninterpretability is decided by the leaves' types alone.

The definite article

def HeimKratzer.Partial.Holds {E : Type} (P : E →. Prop) (x : E) : Prop

A partial predicate holds of an individual when it is defined there and true.

Equations

• HeimKratzer.Partial.Holds P x = ∃ (h : (P x).Dom), (P x).get h

noncomputable def HeimKratzer.Partial.the {E W D : Type} : Montague.Ty.PDomain E W ((Montague.Ty.e ⇒ Montague.Ty.t) ⇒ Montague.Ty.e) D

[HK98]'s Fregean entry for the definite article, which maps a predicate true of exactly one individual to that individual and is undefined elsewhere.

Equations

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

theorem HeimKratzer.Partial.the_dom {E W D : Type} (P : E →. Prop) : (the P).Dom ↔ ∃! x : E, Holds P x

The definite article is defined exactly on the predicates true of one individual.

@[simp]

theorem HeimKratzer.Partial.holds_lift {E : Type} (P : E → Prop) (x : E) : Holds (↑P) x ↔ P x

A total predicate holds where it is true.

theorem HeimKratzer.Partial.the_lift_eq_some {E W D : Type} {P : E → Prop} {a : E} (h : ∀ (x : E), P x ↔ x = a) : the ↑P = Part.some a

On a total predicate true of exactly one individual, the definite article picks it.

Total lexica

A partial denotation lifts a total one when it agrees with it at a base type and, at a function type, is defined on every lift of an argument with a value lifting the total function's value. On a lexicon whose entries lift a total lexicon, every value of the partial engine is defined and lifts the pure engine's value at the same node, since both evaluate the same term and every mode preserves the lift; so a total lexicon has no presupposition failures.

def Montague.Ty.Lifts {E W D : Type} (ty : Ty) : Domain E W ty D → PDomain E W ty D → Prop

The lifting relation between a total denotation and a partial one of the same type.

Equations

• Montague.Ty.e.Lifts x_3 y = (x_3 = y)
• Montague.Ty.t.Lifts x_3 y = (x_3 = y)
• Montague.Ty.d.Lifts x_3 y = (x_3 = y)
• Montague.Ty.n.Lifts x_3 y = (x_3 = y)
• Montague.Ty.v.Lifts x_3 y = (x_3 = y)
• Montague.Ty.s.Lifts x_3 y = (x_3 = y)
• (a ⇒ b).Lifts f f' = ∀ (x : Montague.Ty.Domain E W a D) (y : Montague.Ty.PDomain E W a D), a.Lifts x y → ∃ (z : Montague.Ty.PDomain E W b D), f' y = Part.some z ∧ b.Lifts (f x) z
• a.intens.Lifts f f' = ∀ (w : W), ∃ (z : Montague.Ty.PDomain E W a D), f' w = Part.some z ∧ a.Lifts (f w) z

@[simp]

theorem Montague.Ty.lifts_e {E W D : Type} {x y : E} : e.Lifts x y ↔ x = y

@[simp]

theorem Montague.Ty.lifts_t {E W D : Type} {x y : Prop} : t.Lifts x y ↔ x = y

theorem Montague.Ty.lifts_fn {E W D : Type} {a b : Ty} {f : Domain E W (a ⇒ b) D} {f' : PDomain E W (a ⇒ b) D} : (a ⇒ b).Lifts f f' ↔ ∀ (x : Domain E W a D) (y : PDomain E W a D), a.Lifts x y → ∃ (z : PDomain E W b D), f' y = Part.some z ∧ b.Lifts (f x) z

theorem Montague.Ty.lifts_lift {E W D : Type} {b : Ty} {f : E → Domain E W b D} {f' : E → PDomain E W b D} (h : ∀ (x : E), b.Lifts (f x) (f' x)) : (e ⇒ b).Lifts f ↑f'

A total function of individuals lifts to the everywhere-defined partial function whose values lift its values.

inductive Montague.Denotation.Lifts {E W D : Type} : Denotation E W Id D → PDenotation E W D → Prop

A partial denotation lifts a total one when it has the same type and a defined value that lifts the total value.

• mk {E W D : Type} {ty : Ty} {x : Ty.Domain E W ty D} {y : Ty.PDomain E W ty D} (h : ty.Lifts x y) : Lifts ⟨ty, x⟩ ⟨ty, Part.some y⟩

theorem Montague.Denotation.Lifts.fst {E W D : Type} {d : Denotation E W Id D} {d' : PDenotation E W D} (h : d.Lifts d') : d.fst = d'.fst

inductive Montague.Ty.FirstOrder : Ty → Prop

The types whose functions take only individuals as arguments are those the extensional lexicon of [HK98] has, namely individuals, truth values, degrees, cardinalities, eventualities, functions from individuals, and intensions.

• e : Ty.e.FirstOrder
• t : Ty.t.FirstOrder
• d : Ty.d.FirstOrder
• n : Ty.n.FirstOrder
• v : Ty.v.FirstOrder
• s : Ty.s.FirstOrder
• fn {b : Ty} : b.FirstOrder → (Ty.e ⇒ b).FirstOrder
• intens {a : Ty} : a.FirstOrder → a.intens.FirstOrder

def Montague.Ty.Domain.toPartial {E W D : Type} (ty : Ty) : Domain E W ty D → PDomain E W ty D

The partial denotation a total one lifts to, defined everywhere on individual arguments and nowhere on a function argument.

theorem Montague.Ty.lifts_toPartial {E W D : Type} {ty : Ty} (h : ty.FirstOrder) (x : Domain E W ty D) : ty.Lifts x (Domain.toPartial ty x)

At a first-order type, the lift of a total denotation lifts it.

def Montague.Denotation.toPartial {E W D : Type} (d : Denotation E W Id D) : PDenotation E W D

The partial denotation a total one lifts to.

Equations

• d.toPartial = ⟨d.fst, Part.some (Montague.Ty.Domain.toPartial d.fst d.snd)⟩

theorem Montague.Denotation.lifts_toPartial {E W D : Type} {d : Denotation E W Id D} (h : d.fst.FirstOrder) : d.Lifts d.toPartial

A first-order total denotation is lifted by its partial counterpart.

theorem HeimKratzer.Mode.lifts_evalPartial {E W D : Type} {σ₁ σ₂ τ : Montague.Ty} (m : Mode σ₁ σ₂ τ) {a : Montague.Ty.Domain E W σ₁ D} {b : Montague.Ty.Domain E W σ₂ D} {a' : Montague.Ty.PDomain E W σ₁ D} {b' : Montague.Ty.PDomain E W σ₂ D} (ha : σ₁.Lifts a a') (hb : σ₂.Lifts b b') : ∃ (z : Montague.Ty.PDomain E W τ D), m.evalPartial (Part.some a') (Part.some b') = Part.some z ∧ τ.Lifts (m.eval a b) z

Every mode preserves the lift, since on defined daughters that lift total ones a mode's partial value is defined and lifts its total value.

def HeimKratzer.LiftsConst {E W D : Type} (ty : Montague.Ty) (c : Id (Montague.Ty.Domain E W ty D)) (c' : Part (Montague.Ty.PDomain E W ty D)) : Prop

A partial constant lifts a total one when it is defined with a value lifting it.

Equations

• HeimKratzer.LiftsConst ty c c' = ∃ (y : Montague.Ty.PDomain E W ty D), c' = Part.some y ∧ ty.Lifts c y

theorem HeimKratzer.Term.Rel.lifts {E W D : Type} {ty : Montague.Ty} {u : Term (fun (ty : Montague.Ty) => Id (Montague.Ty.Domain E W ty D)) ty} {u' : Term (fun (ty : Montague.Ty) => Part (Montague.Ty.PDomain E W ty D)) ty} (h : Rel LiftsConst u u') (g : Assignment E) : ∃ (z : Montague.Ty.PDomain E W ty D), evalPartial (fun {ty : Montague.Ty} (c : Part (Montague.Ty.PDomain E W ty D)) => c) g u' = Part.some z ∧ ty.Lifts (eval (fun {ty : Montague.Ty} (c : Montague.Ty.Domain E W ty D) => c) g u) z

Terms of the same shape whose partial constants lift the total ones have a defined partial denotation lifting the total one, under every assignment.

theorem HeimKratzer.Partial.interp_lifts {E W D C : Type} {L : Type u_1} {lex : L → Option (Montague.Denotation E W Id D)} {lex' : L → Option (Montague.PDenotation E W D)} (hlex : ∀ (w : L) (d' : Montague.PDenotation E W D), lex' w = some d' → ∃ (d : Montague.Denotation E W Id D), lex w = some d ∧ d.Lifts d') (g : Assignment E) (t : PhraseStructure.Tree C L) {d' : Montague.PDenotation E W D} (h : interp lex' g t = some d') : ∃ (d : Montague.Denotation E W Id D), Tree.interp lex g t = some d ∧ d.Lifts d'

On a lexicon lifting a total one, every value of the partial engine is defined and lifts the pure engine's value at that node.

theorem HeimKratzer.Partial.not_presupFailure_of_lifts {E W D C : Type} {L : Type u_1} {lex : L → Option (Montague.Denotation E W Id D)} {lex' : L → Option (Montague.PDenotation E W D)} (hlex : ∀ (w : L) (d' : Montague.PDenotation E W D), lex' w = some d' → ∃ (d : Montague.Denotation E W Id D), lex w = some d ∧ d.Lifts d') (g : Assignment E) (t : PhraseStructure.Tree C L) : ¬PresupFailure lex' g t

A lexicon lifting a total one has no presupposition failures.

theorem HeimKratzer.Partial.lifts_map_toPartial {E W D : Type} {L : Type u_1} {lex : L → Option (Montague.Denotation E W Id D)} (h : ∀ (w : L) (d : Montague.Denotation E W Id D), lex w = some d → d.fst.FirstOrder) (w : L) (d' : Montague.PDenotation E W D) (h' : Option.map Montague.Denotation.toPartial (lex w) = some d') : ∃ (d : Montague.Denotation E W Id D), lex w = some d ∧ d.Lifts d'

The entrywise lift of a first-order lexicon lifts it.

theorem HeimKratzer.Partial.not_presupFailure_map_toPartial {E W D C : Type} {L : Type u_1} {lex : L → Option (Montague.Denotation E W Id D)} (h : ∀ (w : L) (d : Montague.Denotation E W Id D), lex w = some d → d.fst.FirstOrder) (g : Assignment E) (t : PhraseStructure.Tree C L) : ¬PresupFailure (fun (w : L) => Option.map Montague.Denotation.toPartial (lex w)) g t

The entrywise lift of a first-order lexicon has no presupposition failures.