Applicative heads

Applicative heads introduce applied arguments (benefactives, goals, sources). Following [Pyl08], a high applicative Merges with the event and relates the applied argument to it; a low applicative Merges with the theme (recipient = transfer to, source = transfer from). High applicatives need Voice to supply event semantics, so they are blocked under semantically null Voice (middles, anticausatives); low applicatives are Voice-independent.

The high/low distinction is read off the Merge complement's category via the head function SO.outerCatC, so the typology follows from attachment height by construction.

Main definitions

• ApplType, ApplType.complement: the high/low typology and the complement it Merges with.
• ApplType.RequiresEventSemantics, IsLow: structural predicates read off the complement.
• ApplHead.Licensed: licensing of an applicative by a Voice head.
• ApplHead.SpecCanBearCase: case-based blocking of SpecApplP ([Woo15]).

References

[Cue03], [Pyl08], [Woo15]

Applicative type and its Merge complement

inductive Minimalist.ApplType : Type

High vs low applicatives ([Pyl08]): high relates to the event, low to the theme.

• high : ApplType

  Above VP: relates the applied argument to the event.

• lowRecipient : ApplType

  Below VP: transfer-of-possession to the applied argument.

• lowSource : ApplType

  Below VP: transfer-of-possession from the applied argument.

@[implicit_reducible]

instance Minimalist.instDecidableEqApplType : DecidableEq ApplType

Equations

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

@[implicit_reducible]

instance Minimalist.instReprApplType : Repr ApplType

Equations

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

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✝

def Minimalist.ApplType.complement : ApplType → Cat

The category an applicative Merges with: the event v (high) or the theme D (low).

Equations

• Minimalist.ApplType.high.complement = Minimalist.Cat.v
• Minimalist.ApplType.lowRecipient.complement = Minimalist.Cat.D
• Minimalist.ApplType.lowSource.complement = Minimalist.Cat.D

def Minimalist.ApplType.complementSO (a : ApplType) : SO

The complement constituent an applicative Merges with — a leaf headed by a.complement.

Equations

• a.complementSO = Minimalist.SO.mkLeaf a.complement [] 0

def Minimalist.ApplType.complementFeatures (a : ApplType) : CatFeatures

The Merge complement's categorial features, read via the §1.13 head function SO.outerCatC.

Equations

• a.complementFeatures = a.complementSO.outerCatC.elim { plusV := false, plusN := false } Minimalist.catFeatures

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

a.IsLow: the applicative Merges with a nominal (theme) complement.

Equations

• a.IsLow = (a.complementFeatures.plusN = true)

@[implicit_reducible]

instance Minimalist.instDecidablePredApplTypeIsLow : DecidablePred ApplType.IsLow

Equations

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

def Minimalist.ApplType.RequiresEventSemantics (a : ApplType) : Prop

a.RequiresEventSemantics: a Merges with the verbal (event) complement.

Equations

• a.RequiresEventSemantics = (a.complementFeatures.plusV = true)

@[implicit_reducible]

instance Minimalist.instDecidablePredApplTypeRequiresEventSemantics : DecidablePred ApplType.RequiresEventSemantics

Equations

• Minimalist.instDecidablePredApplTypeRequiresEventSemantics x✝ = Minimalist.instDecidablePredApplTypeRequiresEventSemantics._aux_1 x✝

def Minimalist.ApplType.RequiresThemeInComplement (a : ApplType) : Prop

a.RequiresThemeInComplement: low applicatives need an unsaturated theme in the complement.

Equations

• a.RequiresThemeInComplement = a.IsLow

@[implicit_reducible]

instance Minimalist.instDecidablePredApplTypeRequiresThemeInComplement : DecidablePred ApplType.RequiresThemeInComplement

Equations

• Minimalist.instDecidablePredApplTypeRequiresThemeInComplement a = Minimalist.instDecidablePredApplTypeRequiresThemeInComplement._aux_1 a

The applicative head

structure Minimalist.ApplHead : Type

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

• applType : ApplType

  High or low (recipient/source).

• assignsDative : Bool

  Whether the applied argument receives dative case.

@[implicit_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.

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

Equations

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

@[implicit_reducible]

instance Minimalist.instReprApplHead : Repr ApplHead

Equations

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

def Minimalist.applHigh : ApplHead

Canonical high applicative (ethical dative).

Equations

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

def Minimalist.applLowRecipient : ApplHead

Canonical low recipient applicative (DOC, possessive dative).

Equations

• Minimalist.applLowRecipient = { applType := Minimalist.ApplType.lowRecipient }

def Minimalist.applLowSource : ApplHead

Canonical low source applicative.

Equations

• Minimalist.applLowSource = { applType := Minimalist.ApplType.lowSource }

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

def Minimalist.ApplHead.Licensed (appl : ApplHead) (voice : VoiceHead) : Prop

appl.Licensed voice: if appl requires event semantics, voice supplies them.

Equations

• appl.Licensed voice = (appl.applType.RequiresEventSemantics → voice.HasSemantics)

@[implicit_reducible]

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

Equations

• Minimalist.instDecidableLicensed appl voice = Minimalist.instDecidableLicensed._aux_1 appl voice

Licensing predictions

theorem Minimalist.high_requires_event : ApplType.high.RequiresEventSemantics

High applicatives require event semantics.

theorem Minimalist.low_no_event_requirement : ¬ApplType.lowRecipient.RequiresEventSemantics ∧ ¬ApplType.lowSource.RequiresEventSemantics

Low applicatives do not require event semantics.

theorem Minimalist.low_licensed_with_any (v : VoiceHead) : applLowRecipient.Licensed v ∧ applLowSource.Licensed v

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

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

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

theorem Minimalist.ethical_dative_with_agent : applHigh.Licensed voiceAgent

Ethical datives (high Appl) are licensed with agentive Voice.

theorem Minimalist.ethical_dative_blocked_in_middle : ¬applHigh.Licensed voiceMiddle

High Appl is blocked with middle Voice (no event semantics) ([Pyl08]).

theorem Minimalist.possessive_dative_survives_middle : applLowRecipient.Licensed voiceMiddle

Possessive datives (low Appl) survive in middles.

theorem Minimalist.possessive_dative_survives_anticausative : applLowRecipient.Licensed voiceAnticausative

Possessive datives survive in anticausatives.

theorem Minimalist.ethical_possessive_middle_asymmetry : ¬applHigh.Licensed voiceMiddle ∧ applLowRecipient.Licensed voiceMiddle

The asymmetry: ethical blocked but possessive survives in middles.

Case-based blocking of SpecApplP ([Woo15])

def Minimalist.ApplHead.SpecCanBearCase {α : Type u_1} [HasCase α] (appl : ApplHead) (x : α) : Prop

appl.SpecCanBearCase x: if appl assigns dative, x must bear case ([Woo15]).

Equations

• appl.SpecCanBearCase x = (appl.assignsDative = true → (caseOf x).isSome = true)

@[implicit_reducible]

instance Minimalist.instDecidableSpecCanBearCase {α : Type u_1} [HasCase α] (appl : ApplHead) (x : α) : Decidable (appl.SpecCanBearCase x)

Equations

• Minimalist.instDecidableSpecCanBearCase appl x = Minimalist.instDecidableSpecCanBearCase._aux_1 appl x