Modifiers

[Par70] [Kam75]

A modifier of τ is a function on the modificand's denotation ([Par70]: "modifiers as functions on predicates"). Adjectives, adverbs, and relative clauses are all modifiers — of different τ (nominal e ⇒ t, event Event → Prop, …) — unified by being this type, not by implementing an interface.

The well-behaved special case is intersective modification: conjunction with a fixed property (λx. P x ∧ Q x), on which restrictive relative clauses, intersective adjectives, and manner adverbs all converge.

Main declarations

• Modifier — a modifier of τ is an endofunction τ → τ.
• Modifier.intersective — the intersective modifier built from a property P.
• Modifier.isIntersective / .isSubsective / .isPrivative — the [Kam75] modifier-meaning classification, as predicates on a modifier.

Implementation notes

Modifier.intersective is the canonical intersective-modification operation; the concrete reflexes reduce to it (ArgumentStructure/LF.EventModifier.modify over events calls it; the type-driven interpreter's Predicate Modification step is it at e ⇒ t). The adjective-specific classification in Gradability/Classification (over AdjMeaning) is the remaining copy to fold onto these forms (follow-up).

@[reducible, inline]

abbrev Modifier (τ : Type u_1) : Type u_1

A modifier of τ is a function on the modificand's denotation ([Par70]). Adjectives, adverbs, and relative clauses are modifiers of different τ; they compose as endofunctions (modifier stacking).

Equations

• Modifier τ = (τ → τ)

def Modifier.intersective {α : Type u_1} (P : α → Prop) : Modifier (α → Prop)

The intersective modifier built from a property P: combine P with the modificand by pointwise conjunction. The well-behaved special case (restrictive relative clauses, intersective adjectives, manner adverbs).

Equations

• Modifier.intersective P Q x = (P x ∧ Q x)

@[simp]

theorem Modifier.intersective_apply {α : Type u_1} (P Q : α → Prop) (x : α) : intersective P Q x = (P x ∧ Q x)

theorem Modifier.intersective_comm {α : Type u_1} (P Q : α → Prop) : intersective P Q = intersective Q P

Head and modifier intersect symmetrically (conjunction is commutative).

def Modifier.isIntersective {α : Type u_1} (m : Modifier (α → Prop)) : Prop

A modifier is intersective if it is conjunction with some fixed property.

Equations

• m.isIntersective = ∃ (P : α → Prop), ∀ (Q : α → Prop), m Q = Modifier.intersective P Q

def Modifier.isSubsective {α : Type u_1} (m : Modifier (α → Prop)) : Prop

A modifier is subsective if its output always entails the modificand (m Q ⊆ Q): a skillful surgeon is a surgeon.

Equations

• m.isSubsective = ∀ (Q : α → Prop) (x : α), m Q x → Q x

def Modifier.isPrivative {α : Type u_1} (m : Modifier (α → Prop)) : Prop

A modifier is privative if its output is disjoint from the modificand (m Q ∩ Q = ∅): a fake gun is not a gun.

Equations

• m.isPrivative = ∀ (Q : α → Prop) (x : α), m Q x → ¬Q x

theorem Modifier.intersective_isIntersective {α : Type u_1} (P : α → Prop) : (intersective P).isIntersective

theorem Modifier.isSubsective_of_isIntersective {α : Type u_1} {m : Modifier (α → Prop)} (h : m.isIntersective) : m.isSubsective

Intersective ⟹ subsective ([Kam75]'s implication structure).