Applicative heads

Applicative heads introduce applied arguments such as benefactives, goals, sources and affected datives. [Pyl08] distinguishes a high applicative, which Merges with the event and relates the applied argument to it, from a low applicative, which Merges with the theme and relates the applied argument to it by transfer to or from it; [Cue03] adds the static possession a low applicative can express and a third type, the affected applicative, which Merges between two events, taking the result state as its complement under the dynamic head that embeds it. The type is where the head Merges: ApplSite, a cut of the little-v chain of Minimalist.LittleV, is low when no head is below it, so that its complement is the theme DP, high when no head is above it, so that Voice selects it, and affected between. ApplSite.applType reads the type off the site, and the complement category of the type agrees with that of the site (ApplSite.applType_complement), so the typology follows from attachment height by construction.

Main definitions

• LowRelation, ApplType, ApplType.complement, ApplType.IsLow: the types and the category each Merges with.
• ApplSite, ApplSite.Low, ApplSite.Affected, ApplSite.High, ApplSite.complement, ApplSite.selector, ApplSite.applType, ApplSite.all: the merge site and its type.
• ApplHead, ApplHead.Licensed, ApplHead.SpecCanBearCase: the head, its licensing by Voice and the case-based blocking of its specifier.

Main results

• ApplSite.low_or_affected_or_high, ApplSite.applType_complement, ApplSite.mem_all_iff.
• ApplSite.Affected.biEventive, ApplSite.Affected.selector_dynamic, ApplSite.not_affected_of_state: an affected applicative needs two events and a dynamic head above it, so none is applied under a state.
• low_licensed_with_any, affected_licensed_with_any, high_licensed_of_assignsTheta.

Implementation notes

ApplHead.Licensed states the licensing of a high applicative by a Voice with event semantics ([Pyl08], [Sch08a]), which blocks the ethical dative in middles; [Cue03]'s high applicative over a state has no Voice above it at all, a disagreement a predicate over Voice heads cannot state, and Studies/Cuervo2003 states her licensing over sites instead.

References

• [Pyl08]
• [Cue03]
• [Sch08a]
• [Woo15]

Applicative types

inductive Minimalist.LowRelation : Type

A low applicative relates the applied argument and the theme by the dynamic transfer to a recipient or from a source of [Pyl08], or by the static possession of [Cue03]'s low applicative AT.

• recipient : LowRelation
• source : LowRelation
• possessor : LowRelation

@[instance_reducible]

instance Minimalist.instDecidableEqLowRelation : DecidableEq LowRelation

Equations

• Minimalist.instDecidableEqLowRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.instReprLowRelation.repr : LowRelation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprLowRelation : Repr LowRelation

Equations

• Minimalist.instReprLowRelation = { reprPrec := Minimalist.instReprLowRelation.repr }

inductive Minimalist.ApplType : Type

An applicative is high, relating the applied argument to the event; affected, relating it to a result state under the dynamic event that embeds it; or low, relating it to the theme.

• high : ApplType
• affected : ApplType
• low (relation : LowRelation) : ApplType

def Minimalist.instDecidableEqApplType.decEq (x✝ x✝¹ : ApplType) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqApplType.decEq Minimalist.ApplType.high Minimalist.ApplType.high = isTrue ⋯
• Minimalist.instDecidableEqApplType.decEq Minimalist.ApplType.high Minimalist.ApplType.affected = isFalse Minimalist.instDecidableEqApplType.decEq._proof_3
• Minimalist.instDecidableEqApplType.decEq Minimalist.ApplType.high (Minimalist.ApplType.low relation) = isFalse ⋯
• Minimalist.instDecidableEqApplType.decEq Minimalist.ApplType.affected Minimalist.ApplType.high = isFalse Minimalist.instDecidableEqApplType.decEq._proof_5
• Minimalist.instDecidableEqApplType.decEq Minimalist.ApplType.affected Minimalist.ApplType.affected = isTrue ⋯
• Minimalist.instDecidableEqApplType.decEq Minimalist.ApplType.affected (Minimalist.ApplType.low relation) = isFalse ⋯
• Minimalist.instDecidableEqApplType.decEq (Minimalist.ApplType.low relation) Minimalist.ApplType.high = isFalse ⋯
• Minimalist.instDecidableEqApplType.decEq (Minimalist.ApplType.low relation) Minimalist.ApplType.affected = isFalse ⋯
• Minimalist.instDecidableEqApplType.decEq (Minimalist.ApplType.low a) (Minimalist.ApplType.low b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.instDecidableEqApplType : DecidableEq ApplType

Equations

• Minimalist.instDecidableEqApplType = Minimalist.instDecidableEqApplType.decEq

def Minimalist.instReprApplType.repr : ApplType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.instReprApplType.repr Minimalist.ApplType.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.ApplType.high")).group prec✝

@[instance_reducible]

instance Minimalist.instReprApplType : Repr ApplType

Equations

• Minimalist.instReprApplType = { reprPrec := Minimalist.instReprApplType.repr }

def Minimalist.ApplType.complement : ApplType → Cat

An applicative Merges with a vP when it is high or affected, and with the theme D when it is low.

Equations

• Minimalist.ApplType.high.complement = Minimalist.Cat.v
• Minimalist.ApplType.affected.complement = Minimalist.Cat.v
• (Minimalist.ApplType.low relation).complement = Minimalist.Cat.D

def Minimalist.ApplType.IsLow (t : ApplType) : Prop

An applicative is low when its complement is the theme.

Equations

• t.IsLow = (t.complement = Minimalist.Cat.D)

@[instance_reducible]

instance Minimalist.instDecidablePredApplTypeIsLow : DecidablePred ApplType.IsLow

Equations

• Minimalist.instDecidablePredApplTypeIsLow x✝ = Minimalist.instDecidablePredApplTypeIsLow._aux_1 x✝

theorem Minimalist.ApplType.isLow_iff (t : ApplType) : t.IsLow ↔ ∃ (r : LowRelation), t = low r

The merge site

structure Minimalist.ApplSite : Type

The site of an applicative head in an event structure records the verbal heads above ApplP and the heads of its complement, highest first.

• above : List LittleV
• below : List LittleV

@[instance_reducible]

instance Minimalist.instDecidableEqApplSite : DecidableEq ApplSite

Equations

• Minimalist.instDecidableEqApplSite = Minimalist.instDecidableEqApplSite.decEq

def Minimalist.instDecidableEqApplSite.decEq (x✝ x✝¹ : ApplSite) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqApplSite.decEq { above := a, below := a_1 } { above := b, below := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Minimalist.instReprApplSite.repr : ApplSite → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprApplSite : Repr ApplSite

Equations

• Minimalist.instReprApplSite = { reprPrec := Minimalist.instReprApplSite.repr }

def Minimalist.ApplSite.heads (s : ApplSite) : List LittleV

The event structure the applicative sits in.

Equations

• s.heads = s.above ++ s.below

def Minimalist.ApplSite.Low (s : ApplSite) : Prop

A site is low when Appl takes the theme DP as its complement, below every verbal head, and ApplP is the complement of the root.

Equations

• s.Low = (s.below = [])

def Minimalist.ApplSite.High (s : ApplSite) : Prop

A site is high when ApplP is the complement of no verbal head, Voice or Tense taking it.

Equations

• s.High = (s.above = [])

def Minimalist.ApplSite.Affected (s : ApplSite) : Prop

A site is affected when Appl takes a vP as its complement and ApplP is the complement of the verbal head above, so the applied argument participates in two events.

Equations

• s.Affected = (s.above ≠ [] ∧ s.below ≠ [])

@[instance_reducible]

instance Minimalist.ApplSite.instDecidablePredLow : DecidablePred Low

Equations

• x✝.instDecidablePredLow = Minimalist.ApplSite.instDecidablePredLow._aux_1 x✝

@[instance_reducible]

instance Minimalist.ApplSite.instDecidablePredHigh : DecidablePred High

Equations

• x✝.instDecidablePredHigh = Minimalist.ApplSite.instDecidablePredHigh._aux_1 x✝

@[instance_reducible]

instance Minimalist.ApplSite.instDecidablePredAffected : DecidablePred Affected

Equations

• x✝.instDecidablePredAffected = { decide := decide (x✝.above ≠ []) && decide (x✝.below ≠ []), reflects_decide := ⋯ }

def Minimalist.ApplSite.complement (s : ApplSite) : Cat

The category of Appl's complement, the theme DP of a low applicative and a vP otherwise.

Equations

• s.complement = if s.below = [] then Minimalist.Cat.D else Minimalist.Cat.v

def Minimalist.ApplSite.selector (s : ApplSite) : Option LittleV

ApplP is the complement of the lowest verbal head above it, whose root takes ApplP when the applicative is low, and of no verbal head when it is high.

Equations

• s.selector = s.above.getLast?

def Minimalist.ApplSite.applType (s : ApplSite) (r : LowRelation) : ApplType

The type of the applicative at the site, given the relation a low one reads.

Equations

• s.applType r = if s.below = [] then Minimalist.ApplType.low r else if s.above = [] then Minimalist.ApplType.high else Minimalist.ApplType.affected

theorem Minimalist.ApplSite.complement_eq_D_iff (s : ApplSite) : s.complement = Cat.D ↔ s.Low

theorem Minimalist.ApplSite.selector_eq_none_iff (s : ApplSite) : s.selector = none ↔ s.High

theorem Minimalist.ApplSite.applType_complement (s : ApplSite) (r : LowRelation) : (s.applType r).complement = s.complement

The type read off the site Merges with the category the site gives it.

theorem Minimalist.ApplSite.applType_eq_low_iff (s : ApplSite) (r : LowRelation) : s.applType r = ApplType.low r ↔ s.Low

theorem Minimalist.ApplSite.applType_eq_affected_iff (s : ApplSite) (r : LowRelation) : s.applType r = ApplType.affected ↔ s.Affected

theorem Minimalist.ApplSite.low_or_affected_or_high (s : ApplSite) (h : s.heads ≠ []) : s.Low ∨ s.Affected ∨ s.High

The three types partition the sites in a nonempty structure.

theorem Minimalist.ApplSite.Affected.not_low (s : ApplSite) (h : s.Affected) : ¬s.Low

theorem Minimalist.ApplSite.Affected.not_high (s : ApplSite) (h : s.Affected) : ¬s.High

theorem Minimalist.ApplSite.Affected.biEventive (s : ApplSite) (h : s.Affected) : LittleV.BiEventive s.heads

An affected applicative requires two events.

theorem Minimalist.ApplSite.Affected.selector_dynamic (s : ApplSite) (hw : LittleV.IsWellFormed s.heads) (h : s.Affected) (v : LittleV) : v ∈ s.selector → v.Dynamic

The head an affected applicative is the complement of is dynamic: it embeds the eventuality below the applicative.

theorem Minimalist.ApplSite.not_affected_of_state (s : ApplSite) (hw : LittleV.IsWellFormed s.heads) (h : s.selector = some LittleV.vBE) : ¬s.Affected

No affected applicative is applied under a state.

def Minimalist.ApplSite.all (l : List LittleV) : List ApplSite

The sites of an applicative in the structure l are the cuts of the list.

Equations

• Minimalist.ApplSite.all l = List.map (fun (i : ℕ) => { above := List.take i l, below := List.drop i l }) (List.range (l.length + 1))

theorem Minimalist.ApplSite.mem_all_iff {l : List LittleV} {s : ApplSite} : s ∈ all l ↔ s.heads = l

The applicative head

structure Minimalist.ApplHead : Type

An applicative head carries its type and whether it assigns dative case to its specifier.

• applType : ApplType

  High, affected or low.

• assignsDative : Bool

  Whether the applied argument receives dative case.

@[instance_reducible]

instance Minimalist.instDecidableEqApplHead : DecidableEq ApplHead

Equations

• Minimalist.instDecidableEqApplHead = Minimalist.instDecidableEqApplHead.decEq

def Minimalist.instDecidableEqApplHead.decEq (x✝ x✝¹ : ApplHead) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Minimalist.instReprApplHead : Repr ApplHead

Equations

• Minimalist.instReprApplHead = { reprPrec := Minimalist.instReprApplHead.repr }

def Minimalist.instReprApplHead.repr : ApplHead → ℕ → Std.Format

Equations

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

def Minimalist.applHigh : ApplHead

Canonical high applicative (ethical dative).

Equations

• Minimalist.applHigh = { applType := Minimalist.ApplType.high }

def Minimalist.applAffected : ApplHead

Canonical affected applicative (the dative of a causative or an inchoative).

Equations

• Minimalist.applAffected = { applType := Minimalist.ApplType.affected }

def Minimalist.applLowRecipient : ApplHead

Canonical low recipient applicative (DOC).

Equations

• Minimalist.applLowRecipient = { applType := Minimalist.ApplType.low Minimalist.LowRelation.recipient }

def Minimalist.applLowSource : ApplHead

Canonical low source applicative.

Equations

• Minimalist.applLowSource = { applType := Minimalist.ApplType.low Minimalist.LowRelation.source }

def Minimalist.applLowPossessor : ApplHead

Canonical low possessor applicative (possessive dative).

Equations

• Minimalist.applLowPossessor = { applType := Minimalist.ApplType.low Minimalist.LowRelation.possessor }

Voice–applicative licensing ([Pyl08], [Sch08a])

def Minimalist.ApplHead.Licensed (appl : ApplHead) (voice : Voice.Head) : Prop

appl.Licensed voice holds when voice is thematic and so supplies the event semantics a high applicative, the complement of Voice, requires; a low or an affected applicative requires nothing of Voice.

Equations

• appl.Licensed voice = (appl.applType = Minimalist.ApplType.high → voice.IsThematic)

@[instance_reducible]

instance Minimalist.instDecidableLicensed (appl : ApplHead) (voice : Voice.Head) : Decidable (appl.Licensed voice)

Equations

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

theorem Minimalist.low_licensed_with_any (v : Voice.Head) (r : LowRelation) : { applType := ApplType.low r }.Licensed v

Low applicatives are licensed under any Voice head ([Pyl08]).

theorem Minimalist.affected_licensed_with_any (v : Voice.Head) : applAffected.Licensed v

Affected applicatives are licensed under any Voice head: the head that selects them is the dynamic v below Voice ([Cue03]).

theorem Minimalist.high_licensed_of_assignsTheta (v : Voice.Head) (h : v.AssignsTheta) : applHigh.Licensed v

θ-assigning Voice licenses high applicatives (θ-assignment entails event semantics).

theorem Minimalist.ethical_possessive_middle_asymmetry : ¬applHigh.Licensed Voice.middle ∧ applLowPossessor.Licensed Voice.middle

High Appl is blocked with middle Voice, which has no event semantics, while a possessive dative survives there ([Pyl08]).

Case-based blocking of SpecApplP ([Woo15])

def Minimalist.ApplHead.SpecCanBearCase (appl : ApplHead) (c : Option Case) : Prop

If appl assigns dative, its specifier, bearing the case c, must bear one ([Woo15]).

Equations

• appl.SpecCanBearCase c = (appl.assignsDative = true → c.isSome = true)

@[instance_reducible]

instance Minimalist.instDecidableSpecCanBearCase (appl : ApplHead) (c : Option Case) : Decidable (appl.SpecCanBearCase c)

Equations

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