Borer 2013: categorizing roots and the adjective asymmetry

This file formalizes the categorial paradigm of [borer-2013]'s chapter on categorizing roots. A root is a phonological index that a categorial frame realizes; the frame does the categorizing, so nothing is added to the form when a root occurs as a noun rather than a verb. On Morphology.Realization that fixes Ctx as the frame itself, with no head in it, where a Distributed Morphology instance would put a categorizer there.

The paradigm is Borer's (120)–(121): √DANCE and √CHAIR are licensed in the verbal and nominal frames but not the adjectival one, √GREEN and √BIG only in the adjectival frame. Her point is that the asymmetry survives the question of zero categorizers — a theory that mediates categorization through possibly-null category heads still has to rule these cells in and out one by one. Footnote 39 adds the residue: thin and yellow, but not red and fat, occur as verbs too, and since nothing about their adjectival behaviour predicts which, the verbal uses must be listed.

Main definitions

• Root, Frame, licensed — the roots and frames of (120)–(121) and footnote 39
• english — the frames as a Realization, each licensed root realized by its own index

Main results

• english_invariant — no root has more than one exponent: the frame categorizes and adds nothing
• adjectival_roots_are_rigid — no root of the adjectival frame is licensed in the nominal one
• nv_flexibility_systematic — outside the adjectival roots, the nominal and verbal frames license exactly the same roots
• verbal_use_unpredictable — two adjectival roots agree everywhere but the verbal frame, so that cell is not a function of the rest of the paradigm and must be listed

References

• [borer-2013]

inductive Borer2013.Frame : Type

The categorial frames a root may be realized in.

• nFrame : Frame
• vFrame : Frame
• aFrame : Frame

@[instance_reducible]

instance Borer2013.instDecidableEqFrame : DecidableEq Frame

Equations

• Borer2013.instDecidableEqFrame x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Borer2013.instFintypeFrame : Fintype Frame

Equations

• Borer2013.instFintypeFrame = { elems := { val := ↑Borer2013.Frame.enumList, nodup := Borer2013.Frame.enumList_nodup }, complete := Borer2013.instFintypeFrame._proof_1 }

@[instance_reducible]

instance Borer2013.instReprFrame : Repr Frame

Equations

• Borer2013.instReprFrame = { reprPrec := Borer2013.instReprFrame.repr }

def Borer2013.instReprFrame.repr : Frame → ℕ → Std.Format

Equations

• Borer2013.instReprFrame.repr Borer2013.Frame.nFrame prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Frame.nFrame")).group prec✝
• Borer2013.instReprFrame.repr Borer2013.Frame.vFrame prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Frame.vFrame")).group prec✝
• Borer2013.instReprFrame.repr Borer2013.Frame.aFrame prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Frame.aFrame")).group prec✝

inductive Borer2013.Root : Type

The roots of (120)–(121) and footnote 39.

• dance : Root
• chair : Root
• green : Root
• big : Root
• thin : Root
• yellow : Root
• red : Root
• fat : Root

@[instance_reducible]

instance Borer2013.instDecidableEqRoot : DecidableEq Root

Equations

• Borer2013.instDecidableEqRoot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Borer2013.instFintypeRoot : Fintype Root

Equations

• Borer2013.instFintypeRoot = { elems := { val := ↑Borer2013.Root.enumList, nodup := Borer2013.Root.enumList_nodup }, complete := Borer2013.instFintypeRoot._proof_1 }

@[instance_reducible]

instance Borer2013.instReprRoot : Repr Root

Equations

• Borer2013.instReprRoot = { reprPrec := Borer2013.instReprRoot.repr }

def Borer2013.instReprRoot.repr : Root → ℕ → Std.Format

Equations

• Borer2013.instReprRoot.repr Borer2013.Root.dance prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Root.dance")).group prec✝
• Borer2013.instReprRoot.repr Borer2013.Root.chair prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Root.chair")).group prec✝
• Borer2013.instReprRoot.repr Borer2013.Root.green prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Root.green")).group prec✝
• Borer2013.instReprRoot.repr Borer2013.Root.big prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Root.big")).group prec✝
• Borer2013.instReprRoot.repr Borer2013.Root.thin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Root.thin")).group prec✝
• Borer2013.instReprRoot.repr Borer2013.Root.yellow prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Root.yellow")).group prec✝
• Borer2013.instReprRoot.repr Borer2013.Root.red prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Root.red")).group prec✝
• Borer2013.instReprRoot.repr Borer2013.Root.fat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2013.Root.fat")).group prec✝

def Borer2013.licensed : Root → Frame → Bool

Which frames license which root: (120) for √DANCE and √CHAIR, (121) for √GREEN and √BIG, and footnote 39 for the four property roots, of which only thin and yellow also occur as verbs.

Equations

• Borer2013.licensed Borer2013.Root.dance Borer2013.Frame.nFrame = true
• Borer2013.licensed Borer2013.Root.dance Borer2013.Frame.vFrame = true
• Borer2013.licensed Borer2013.Root.chair Borer2013.Frame.nFrame = true
• Borer2013.licensed Borer2013.Root.chair Borer2013.Frame.vFrame = true
• Borer2013.licensed Borer2013.Root.green Borer2013.Frame.aFrame = true
• Borer2013.licensed Borer2013.Root.big Borer2013.Frame.aFrame = true
• Borer2013.licensed Borer2013.Root.red Borer2013.Frame.aFrame = true
• Borer2013.licensed Borer2013.Root.fat Borer2013.Frame.aFrame = true
• Borer2013.licensed Borer2013.Root.thin Borer2013.Frame.aFrame = true
• Borer2013.licensed Borer2013.Root.thin Borer2013.Frame.vFrame = true
• Borer2013.licensed Borer2013.Root.yellow Borer2013.Frame.aFrame = true
• Borer2013.licensed Borer2013.Root.yellow Borer2013.Frame.vFrame = true
• Borer2013.licensed x✝¹ x✝ = false

def Borer2013.english : Morphology.Realization Root Frame Root

The exoskeletal system: where a frame licenses a root, the root is realized by its own phonological index. Categorization is the frame's doing, so the form is the same in every frame that licenses it.

Equations

• Borer2013.english = { realize := fun (r : Borer2013.Root) (c : Borer2013.Frame) => if Borer2013.licensed r c = true then {r} else ∅ }

@[simp]

theorem Borer2013.isLicensed_iff (r : Root) (c : Frame) : english.IsLicensed r c ↔ licensed r c = true

@[instance_reducible]

instance Borer2013.instDecidableIsLicensedRootFrameEnglish (r : Root) (c : Frame) : Decidable (english.IsLicensed r c)

Equations

• Borer2013.instDecidableIsLicensedRootFrameEnglish r c = decidable_of_iff (Borer2013.licensed r c = true) ⋯

theorem Borer2013.english_invariant (r : Root) : english.IsInvariant r

No root has more than one exponent: a root occurring in two frames is spelled the same in both, since the frame categorizes and no morphology is added. This is what distinguishes the exoskeletal instance from one whose Ctx carries a categorizer.

theorem Borer2013.adjectival_roots_are_rigid (r : Root) (h : english.IsLicensed r Frame.aFrame) : ¬english.IsLicensed r Frame.nFrame

(121b–c): a root licensed in the adjectival frame is licensed in neither of the others, save for the listed verbal uses of footnote 39 — no adjectival root at all is licensed in the nominal frame.

theorem Borer2013.nv_flexibility_systematic (r : Root) (h : ¬english.IsLicensed r Frame.aFrame) : english.IsLicensed r Frame.nFrame ↔ english.IsLicensed r Frame.vFrame

(120b–c): outside the adjectival roots, noun-verb flexibility is systematic — the nominal and verbal frames license exactly the same roots.

theorem Borer2013.no_root_in_all_frames (r : Root) : ¬(english.IsLicensed r Frame.nFrame ∧ english.IsLicensed r Frame.vFrame ∧ english.IsLicensed r Frame.aFrame)

(120a) and (121b): no root is licensed in all three frames — the categorial systems do not fully overlap.

theorem Borer2013.verbal_use_unpredictable : english.IsLicensed Root.thin Frame.aFrame ∧ english.IsLicensed Root.red Frame.aFrame ∧ (english.IsLicensed Root.thin Frame.nFrame ↔ english.IsLicensed Root.red Frame.nFrame) ∧ english.IsLicensed Root.thin Frame.vFrame ∧ ¬english.IsLicensed Root.red Frame.vFrame

Footnote 39: thin and red are alike in every frame but the verbal one, so a root's verbal cell is not a function of the rest of its paradigm. The verbal uses of to thin and to yellow cannot be predicted and must be listed.

theorem Borer2013.yellow_fat_unpredictable : english.IsLicensed Root.yellow Frame.vFrame ∧ ¬english.IsLicensed Root.fat Frame.vFrame

The same holds of yellow against fat: the pair of listed verbs is not a class the paradigm picks out.