Borer (2013): Structuring Sense: Volume III: Taking Form

A category-less root takes its category from the extended projection above it, so dance is a noun under a determiner and a verb under infinitival to, with nothing added to it. Such roots never occur as adjectives (too dance), and the words that occur as adjectives occur neither as nouns nor as verbs (a green, to green). Distributed Morphology categorizes a root by a head n, v or a that may be null, so it has to rule each pairing of a root with a head in or out. Borer's resolution is that adjectives are not roots. Like derivatives they are born categorized, and a categorized core fits only the extended projection of its own category, while the adjectival extended projection cannot categorize a root.

A root also selects the realization of what attaches to it, as run selects its past ran and goose its plural geese. Selection is local, so only what attaches to a bare root can be selected: derivatives inflect regularly, and on the resolution so do adjectives. Distributed Morphology puts a head between every stem and its inflection, and recovers local selection only by letting null heads be transparent. The chapter ends on a problem it leaves open: -ify and en- are selected by the roots of clarify and enlarge, so a functor taking adjectives attaches to a bare root after all.

Main statements

• licenses_nominal_and_verbal_iff: roots, and roots alone, occur both as nouns and as verbs, which with the lexicon derives every judgment of the paradigm (acceptable_iff_licensed).
• complement_ne_none_of_wellFormed: nothing that takes an adjective attaches to a bare root, so no root selects its realization.
• not_exists_licensing: no condition on the category of a complement both derives the paradigm and lets the verbalizers of clarify and enlarge take their roots.
• dm_seesRoot: in Distributed Morphology's representations no inflection sees its root unless null heads are transparent.

Implementation notes

• The category of a core is an Option CatFamily, none for a root, and an example's frame is the family of the extended projection it builds: nominal under a and the, verbal under to, adjectival under too. The adpositional extended projection is taken not to categorize roots, which the paradigm does not test.
• The verbal thin and yellow are listed as categorized verbs, since as roots they would be nouns as well.
• A word's terminals are the book's categorial functors, with the category each projects and the categories it takes, the segments of extended projections, among them the comparative and the superlative, and the head an adjective is born with. Which realizations a root selects is taken from the book's table of functors and its discussion of -en and en-.
• Distributed Morphology's words are read with the heads, cycles and ∅-Transparency of Embick2010.

TODO

The table of functors is not recorded as data, only the choices of the words built with them, and the functors with a meaning of their own (-ing, -er, -ship), which the book sets apart from the default-and-selection pattern, are treated as functors like the rest. The book's arguments from stacked null heads, which nothing rules out once null heads are transparent, and from the direction of derivation in Kiparsky's examples, are not formalized; they are where Embick's cycles and contextual categorization would come apart.

References

• [Bor13]
• [Emb10]

Categorization by the extended projection

def Borer2013.Licenses (e : Minimalist.CatFamily) : Option Minimalist.CatFamily → Prop

Licenses e κ says that the extended projection of family e takes a core of category κ, where none is a category-less root. A categorized core fits only the extended projection of its own category, and a root becomes a noun or a verb in its extended projection, but the adjectival one cannot make it an adjective.

Equations

• Borer2013.Licenses e (some c) = (c = e)
• Borer2013.Licenses e none = (e = Minimalist.CatFamily.nominal ∨ e = Minimalist.CatFamily.verbal)

@[instance_reducible]

instance Borer2013.instDecidablePredOptionCatFamilyLicenses (e : Minimalist.CatFamily) : DecidablePred (Licenses e)

Equations

• Borer2013.instDecidablePredOptionCatFamilyLicenses e (some c) = Borer2013.instDecidablePredOptionCatFamilyLicenses._aux_1 e c
• Borer2013.instDecidablePredOptionCatFamilyLicenses e none = { decide := decide (e = Minimalist.CatFamily.nominal) || decide (e = Minimalist.CatFamily.verbal), reflects_decide := ⋯ }

@[simp]

theorem Borer2013.licenses_some {e c : Minimalist.CatFamily} : Licenses e (some c) ↔ c = e

@[simp]

theorem Borer2013.licenses_none {e : Minimalist.CatFamily} : Licenses e none ↔ e = Minimalist.CatFamily.nominal ∨ e = Minimalist.CatFamily.verbal

theorem Borer2013.licenses_nominal_and_verbal_iff {κ : Option Minimalist.CatFamily} : Licenses Minimalist.CatFamily.nominal κ ∧ Licenses Minimalist.CatFamily.verbal κ ↔ κ = none

Roots, and roots alone, occur both as nouns and as verbs.

theorem Borer2013.Licenses.eq_adjectival {e : Minimalist.CatFamily} {κ : Option Minimalist.CatFamily} (hA : Licenses Minimalist.CatFamily.adjectival κ) (h : Licenses e κ) : e = Minimalist.CatFamily.adjectival

A core that occurs as an adjective occurs in no other extended projection, since the adjectival extended projection takes no root and an adjective is categorized.

theorem Borer2013.exists_ne_of_verbal_of_adjectival {l : List (Option Minimalist.CatFamily)} (hV : ∃ κ ∈ l, Licenses Minimalist.CatFamily.verbal κ) (hA : ∃ κ ∈ l, Licenses Minimalist.CatFamily.adjectival κ) : ∃ κ ∈ l, ∃ κ' ∈ l, κ ≠ κ'

A word that is both a verb and an adjective is listed under two categories, since no core is licensed in both extended projections. The verbal uses of thin and yellow cannot be predicted from their adjectival ones and must be listed (fn. 39).

The paradigm

def Borer2013.lexicon : List (String × Option Minimalist.CatFamily)

The words of the paradigm, each with the category of a core it is listed as. The roots are category-less, the adjectives are born categorized, and thin and yellow are listed again as verbs.

Equations

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

def Borer2013.categories (w : String) : List (Option Minimalist.CatFamily)

The categories a word is listed under.

Equations

• Borer2013.categories w = List.filterMap (fun (p : String × Option Minimalist.CatFamily) => if p.1 = w then some p.2 else none) Borer2013.lexicon

structure Borer2013.Row : Type

A row records the extended projection an example puts its word in, the categories of the cores the word is listed as, and the judgment.

• frame : Minimalist.CatFamily
• cores : List (Option Minimalist.CatFamily)
• judgment : Judgment

def Borer2013.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Borer2013.instDecidableEqRow : DecidableEq Row

Equations

• Borer2013.instDecidableEqRow = Borer2013.instDecidableEqRow.decEq

def Borer2013.Row.ofDatum (d : Datum) : Option Row

The row of an example whose word is listed.

Equations

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

def Borer2013.data : List Row

The examples.

Equations

• Borer2013.data = List.filterMap Borer2013.Row.ofDatum Borer2013.Examples.all

theorem Borer2013.acceptable_iff_licensed (d : Row) : d ∈ data → (d.judgment = Judgment.acceptable ↔ ∃ κ ∈ d.cores, Licenses d.frame κ)

An example is acceptable exactly when its word is listed as a core that fits the extended projection the example puts it in: a dance, to dance and too green are acceptable, and too dance, a green and to green are not.

Local selection

inductive Borer2013.Terminal : Type

A terminal of a word above its root is a categorial functor, projecting a category over a complement of one of the categories it takes, a segment of an extended projection, or the head that an item is born with.

• functor (proj : Minimalist.CatFamily) (takes : List Minimalist.CatFamily) : Terminal
• segment (e : Minimalist.CatFamily) : Terminal
• born (c : Minimalist.CatFamily) : Terminal

def Borer2013.instDecidableEqTerminal.decEq (x✝ x✝¹ : Terminal) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Borer2013.instDecidableEqTerminal.decEq (Borer2013.Terminal.functor proj takes) (Borer2013.Terminal.segment e) = isFalse ⋯
• Borer2013.instDecidableEqTerminal.decEq (Borer2013.Terminal.functor proj takes) (Borer2013.Terminal.born c) = isFalse ⋯
• Borer2013.instDecidableEqTerminal.decEq (Borer2013.Terminal.segment e) (Borer2013.Terminal.functor proj takes) = isFalse ⋯
• Borer2013.instDecidableEqTerminal.decEq (Borer2013.Terminal.segment a) (Borer2013.Terminal.segment b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Borer2013.instDecidableEqTerminal.decEq (Borer2013.Terminal.segment e) (Borer2013.Terminal.born c) = isFalse ⋯
• Borer2013.instDecidableEqTerminal.decEq (Borer2013.Terminal.born c) (Borer2013.Terminal.functor proj takes) = isFalse ⋯
• Borer2013.instDecidableEqTerminal.decEq (Borer2013.Terminal.born c) (Borer2013.Terminal.segment e) = isFalse ⋯
• Borer2013.instDecidableEqTerminal.decEq (Borer2013.Terminal.born a) (Borer2013.Terminal.born b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Borer2013.instDecidableEqTerminal : DecidableEq Terminal

Equations

• Borer2013.instDecidableEqTerminal = Borer2013.instDecidableEqTerminal.decEq

@[instance_reducible]

instance Borer2013.instReprTerminal : Repr Terminal

Equations

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

def Borer2013.instReprTerminal.repr : Terminal → ℕ → Std.Format

Equations

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

def Borer2013.Terminal.proj : Terminal → Minimalist.CatFamily

The category a terminal projects.

Equations

• (Borer2013.Terminal.functor p takes).proj = p
• (Borer2013.Terminal.segment p).proj = p
• (Borer2013.Terminal.born p).proj = p

def Borer2013.complement (ts : List Terminal) : ℕ → Option Minimalist.CatFamily

The category of what the terminal at position i attaches to, the bare root for the first terminal and otherwise the category of the terminal below.

Equations

• Borer2013.complement ts 0 = none
• Borer2013.complement ts i.succ = Option.map Borer2013.Terminal.proj ts[i]?

def Borer2013.Terminal.Takes (L : Minimalist.CatFamily → Option Minimalist.CatFamily → Prop) : Terminal → Option Minimalist.CatFamily → Prop

A terminal takes a complement of category κ under the licensing L when it is a functor and L licenses κ in one of the categories it takes, a segment whose extended projection L licenses κ in, or a born head on its root.

Equations

• Borer2013.Terminal.Takes L (Borer2013.Terminal.functor proj cs) x✝ = ∃ c ∈ cs, L c x✝
• Borer2013.Terminal.Takes L (Borer2013.Terminal.segment e) x✝ = L e x✝
• Borer2013.Terminal.Takes L (Borer2013.Terminal.born c) x✝ = (x✝ = none)

@[instance_reducible]

instance Borer2013.instDecidableTakesLicenses (t : Terminal) (κ : Option Minimalist.CatFamily) : Decidable (Terminal.Takes Licenses t κ)

Equations

• Borer2013.instDecidableTakesLicenses (Borer2013.Terminal.functor p takes) κ = Borer2013.instDecidableTakesLicenses._aux_1 κ p takes
• Borer2013.instDecidableTakesLicenses (Borer2013.Terminal.segment p) κ = Borer2013.instDecidableTakesLicenses._aux_3 κ p
• Borer2013.instDecidableTakesLicenses (Borer2013.Terminal.born p) κ = Borer2013.instDecidableTakesLicenses._aux_5 κ p

def Borer2013.WellFormed (L : Minimalist.CatFamily → Option Minimalist.CatFamily → Prop) (ts : List Terminal) : Prop

A word is well formed under L when each of its terminals takes what it attaches to.

Equations

• Borer2013.WellFormed L ts = ∀ (i : ℕ) (h : i < ts.length), Borer2013.Terminal.Takes L ts[i] (Borer2013.complement ts i)

@[instance_reducible]

instance Borer2013.instDecidableWellFormedLicenses (ts : List Terminal) : Decidable (WellFormed Licenses ts)

Equations

• Borer2013.instDecidableWellFormedLicenses ts = ts.length.decidableBallLT fun (i : ℕ) (h : i < ts.length) => Borer2013.Terminal.Takes Borer2013.Licenses ts[i] (Borer2013.complement ts i)

inductive Borer2013.Choice : Type

Whether a terminal has its default realization or one that its root selects.

• default : Choice
• rootSelected : Choice

@[instance_reducible]

instance Borer2013.instDecidableEqChoice : DecidableEq Choice

Equations

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

@[instance_reducible]

instance Borer2013.instReprChoice : Repr Choice

Equations

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

def Borer2013.instReprChoice.repr : Choice → ℕ → Std.Format

Equations

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

structure Borer2013.Word : Type

A word records its terminals, innermost first, the terminal whose realization is at issue, and the choice of that realization.

• terminals : List Terminal
• target : ℕ
• choice : Choice

def Borer2013.instDecidableEqWord.decEq (x✝ x✝¹ : Word) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Borer2013.instDecidableEqWord : DecidableEq Word

Equations

• Borer2013.instDecidableEqWord = Borer2013.instDecidableEqWord.decEq

def Borer2013.instReprWord.repr : Word → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Borer2013.instReprWord : Repr Word

Equations

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

def Borer2013.terminalTable : List (String × Terminal)

The terminals as named in the rows.

Equations

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

def Borer2013.choiceTable : List (String × Choice)

The choices as named in the rows.

Equations

• Borer2013.choiceTable = [("default", Borer2013.Choice.default), ("rootSelected", Borer2013.Choice.rootSelected)]

def Borer2013.Word.ofDatum (d : Datum) : Option Word

The word of an example in the book's own representation, its target counted from one.

Equations

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

def Borer2013.words : List Word

The words of the chapter's structures.

Equations

• Borer2013.words = List.filterMap Borer2013.Word.ofDatum Borer2013.Examples.all

structure Borer2013.DMWord : Type

A word as Distributed Morphology represents it, with the inflection whose realization is at issue.

• spine : DistributedMorphology.ComplexHead DistributedMorphology.Root Embick2010.Morpheme
• target : Fin self.spine.heads.length
• choice : Choice

def Borer2013.DMWord.ofDatum (d : Datum) : Option DMWord

The word of an example in Distributed Morphology's representation.

Equations

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

def Borer2013.dmWords : List DMWord

The words of the renderings of Distributed Morphology.

Equations

• Borer2013.dmWords = List.filterMap Borer2013.DMWord.ofDatum Borer2013.Examples.all

theorem Borer2013.isSome_ofDatum (d : Datum) : d ∈ Examples.all → ((Row.ofDatum d).isSome || (Word.ofDatum d).isSome || (DMWord.ofDatum d).isSome) = true

Every example is a judgment of the paradigm or a word in one of the two representations.

theorem Borer2013.complement_eq_none_of_rootSelected (w : Word) : w ∈ words → w.choice = Choice.rootSelected → complement w.terminals w.target = none

A root selects only the realization of what attaches to it directly, since selection is local and every exceptional realization is listed with a root: -ate, -ify and -ment attach to their roots, while the past tense of instantiated and the plural of formations attach to a derivative and take their defaults.

theorem Borer2013.complement_ne_none_of_wellFormed {ts : List Terminal} (hw : WellFormed Licenses ts) {i : ℕ} (hi : i < ts.length) (ht : ts[i] = Terminal.segment Minimalist.CatFamily.adjectival ∨ ∃ (p : Minimalist.CatFamily), ts[i] = Terminal.functor p [Minimalist.CatFamily.adjectival]) : complement ts i ≠ none

In a word well formed under the resolution, a segment of the adjectival extended projection or a functor taking adjectives attaches to a categorized core, never to a bare root, so its realization is never selected by a root: adjectives take only the regular -er and -est, and only the default nominalizers.

theorem Borer2013.not_wellFormed_iff (w : Word) : w ∈ words → (¬WellFormed Licenses w.terminals ↔ ∃ p ∈ [Minimalist.CatFamily.verbal, Minimalist.CatFamily.nominal], w.terminals.head? = some (Terminal.functor p [Minimalist.CatFamily.adjectival]))

The words that the resolution rules out are those that put a functor taking adjectives directly on a root: the verbs of fattened and of the problem cases clarify and enlarge, which do select their realizations, and abilities and weaknesses, which the section on zero categorizers brackets so before the section on adjectives treats their bases as born adjectives.

theorem Borer2013.not_exists_licensing : ¬∃ (L : Minimalist.CatFamily → Option Minimalist.CatFamily → Prop), (∀ d ∈ data, d.judgment = Judgment.acceptable ↔ ∃ κ ∈ d.cores, L d.frame κ) ∧ ∀ w ∈ words, w.choice = Choice.rootSelected → ∀ t ∈ w.terminals[w.target]?, Terminal.Takes L t (complement w.terminals w.target)

The puzzle of the adjective. No licensing condition on the category of a complement both derives the judgments of the paradigm and lets the verbalizers of the problem cases take what their selection requires. Too dance shows that a bare root is not adjectival, while the root-selected -ify of clarify takes an adjectival complement that, selection being local, must be its root.

theorem Borer2013.dm_seesRoot (w : DMWord) : w ∈ dmWords → ¬w.spine.SeesRoot Embick2010.cyclic (fun (x : Embick2010.Morpheme) => False) w.target ∧ (w.choice = Choice.rootSelected → w.spine.SeesRoot Embick2010.cyclic Embick2010.phonNull w.target)

In Distributed Morphology every stem is categorized by a head, so without ∅-Transparency no inflection sees the root, and the past of run is no closer to its root than the past of instantiate. With Embick's ∅-Transparency every root-selected inflection does see it.