Harley (2014): On the identity of roots

This file formalizes [Har14b]'s argument that a root of List 1 is individuated neither by its form nor by its meaning but by an index, on which the Vocabulary Items of List 2 and the interpretations of List 3 are both keyed. Hiaki root suppletion (√322, vuite ~ tenne 'run') shows that roots must already be distinct when their items compete, since an item conditioned by number would otherwise block every less specified root, and that phonologically individuated roots would turn suppletion into rewriting; the caboodle item cahoot shows an interpretation bound to one frame with no Elsewhere, so a root is not a concept either. spellout realizes a root at its insertion site, the index with the number of the internal argument below, by the Subset Principle over the Hiaki vocabulary; run_isProperlySuppletive and cahoot_interp_gap are the two flanks. suppletion_not_agreement is §3.3's argument that conditioning by the internal argument, an ergative–absolutive pattern in a nominative–accusative language, is Vocabulary-Item competition rather than agreement, and unergative_elsewhere its prediction that the suppletive intransitives are unaccusative.

The syntactic evidence of §3.1 that roots take complements is formalized on the configurations of DistributedMorphology.RootCategorization. With the argument the sister of the root and adjuncts adjoined to nP, one, an nP anaphor, strands an adjunct and not the argument (oneStrands_iff), and if a selection restriction relates an argument to the head it is merged with, the noun and the verb of one root share their restriction on the object exactly when the root takes the object as its complement (selector_eq_iff).

Implementation notes

Footnote 16 settles the Elsewhere direction: the impersonal passive, whose argument is syntactically absent, surfaces as tenne, so tenne is the Elsewhere form and vuite is conditioned by a singular internal argument, as in the paper's (14); its (7) is a first pass with the roles reversed. The paper indexes only √322 and √548, the other indices here are arbitrary distinct ones, and the caboodle frame of (16) is recorded by its categorizing head. Example numbers follow the revised manuscript (LingBuzz 001527); the paper's Hiaki examples are the rows of Data/Examples/Harley2014.json.

References

• [Har14b]
• [Bob08]

List 1: roots as indices

def Harley2014.run : DistributedMorphology.Root

√322, realized vuite~tenne 'run' ((3a), (14)).

Equations

• Harley2014.run = { index := 322 }

def Harley2014.walk : DistributedMorphology.Root

The root realized weye~kaate 'walk' ((3f), (26)).

Equations

• Harley2014.walk = { index := 401 }

def Harley2014.kill : DistributedMorphology.Root

The root realized mea~sua 'kill' ((3g), (27)).

Equations

• Harley2014.kill = { index := 402 }

def Harley2014.sing : DistributedMorphology.Root

A non-suppletive intransitive root, bwiika 'sing', at whose index the suppletive items must not compete (§2.1).

Equations

• Harley2014.sing = { index := 500 }

The insertion site

inductive Harley2014.SiteFeature : Type

A root's Vocabulary Items may mention its index and the number of the internal argument on the terminal below.

• root (r : DistributedMorphology.Root) : SiteFeature
• internal (n : Number) : SiteFeature

@[instance_reducible]

instance Harley2014.instDecidableEqSiteFeature : DecidableEq SiteFeature

Equations

• Harley2014.instDecidableEqSiteFeature = Harley2014.instDecidableEqSiteFeature.decEq

def Harley2014.instDecidableEqSiteFeature.decEq (x✝ x✝¹ : SiteFeature) : Decidable (x✝ = x✝¹)

Equations

• Harley2014.instDecidableEqSiteFeature.decEq (Harley2014.SiteFeature.root a) (Harley2014.SiteFeature.root b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Harley2014.instDecidableEqSiteFeature.decEq (Harley2014.SiteFeature.root r) (Harley2014.SiteFeature.internal n) = isFalse ⋯
• Harley2014.instDecidableEqSiteFeature.decEq (Harley2014.SiteFeature.internal n) (Harley2014.SiteFeature.root r) = isFalse ⋯
• Harley2014.instDecidableEqSiteFeature.decEq (Harley2014.SiteFeature.internal a) (Harley2014.SiteFeature.internal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Harley2014.instReprSiteFeature : Repr SiteFeature

Equations

• Harley2014.instReprSiteFeature = { reprPrec := Harley2014.instReprSiteFeature.repr }

def Harley2014.instReprSiteFeature.repr : SiteFeature → ℕ → Std.Format

Equations

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

def Harley2014.site (c : Clause.Arguments Number) (r : DistributedMorphology.Root) : DistributedMorphology.Neighborhood (List SiteFeature)

The neighborhood of root r in a clause bearing the numbers c has the internal argument as the terminal below, and the external argument is not in the local environment (§3.3).

Equations

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

List 2: the suppletive Vocabulary Items

def Harley2014.suppletive (r : DistributedMorphology.Root) (sgForm elseForm : String) : Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem SiteFeature String)

A suppletive root has two items ((14), fn. 16), the form conditioned by a singular internal argument below and the Elsewhere form.

Equations

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

def Harley2014.vocabulary : Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem SiteFeature String)

The Hiaki suppletive vocabulary of (3a), (3f), (3g).

Equations

• Harley2014.vocabulary = Harley2014.suppletive Harley2014.run "vuite" "tenne" ++ Harley2014.suppletive Harley2014.walk "weye" "kaate" ++ Harley2014.suppletive Harley2014.kill "mea" "sua"

def Harley2014.spellout (c : Clause.Arguments Number) (r : DistributedMorphology.Root) : Option String

Spell out root r in clause c by the Subset Principle over vocabulary.

Equations

• Harley2014.spellout c r = DistributedMorphology.subsetPrinciple Harley2014.vocabulary (Harley2014.site c r)

theorem Harley2014.run_sg : spellout (Clause.Arguments.unaccusative Number.singular) run = some "vuite"

Singular subject → vuite ((6a)).

theorem Harley2014.run_pl : spellout (Clause.Arguments.unaccusative Number.plural) run = some "tenne"

Plural subject → tenne ((6b)).

theorem Harley2014.run_impersonal : spellout Clause.Arguments.empty run = some "tenne"

No number-bearing argument (the impersonal passive) → tenne, the Elsewhere form (fn. 16).

theorem Harley2014.walk_sg_pl : spellout (Clause.Arguments.unaccusative Number.singular) walk = some "weye" ∧ spellout (Clause.Arguments.unaccusative Number.plural) walk = some "kaate"

weye/kaate with a singular/plural subject ((26)).

theorem Harley2014.kill_sgObj_plObj : spellout (Clause.Arguments.transitive Number.singular Number.plural) kill = some "mea" ∧ spellout (Clause.Arguments.transitive Number.plural Number.singular) kill = some "sua"

mea/sua with a singular/plural object, whatever the subject ((27)).

§2.1–2.2 Individuation is not phonological

theorem Harley2014.run_two_forms : spellout (Clause.Arguments.unaccusative Number.singular) run ≠ spellout (Clause.Arguments.unaccusative Number.plural) run

One index has two phonologically unrelated forms, so a root identified by its form would split √322 in two (§2.2).

theorem Harley2014.index_local (c : Clause.Arguments Number) : spellout c sing = none

The suppletive items compete only at their own index, so a non-suppletive intransitive root receives no exponent from vocabulary, which is why List-1 roots must be distinct before spell-out (§2.1).

§3.3 Conditioning by the internal argument

theorem Harley2014.suppletion_ignores_external (obj subj subj' : Number) (r : DistributedMorphology.Root) : spellout (Clause.Arguments.transitive obj subj) r = spellout (Clause.Arguments.transitive obj subj') r

The external argument's number never conditions the form.

theorem Harley2014.unergative_elsewhere (n : Number) : spellout (Clause.Arguments.unergative n) run = some "tenne"

Only an internal argument conditions the form. An intransitive whose sole argument is external gets the Elsewhere form whatever its number, so the suppletive intransitives must be unaccusative, the paper's prediction from locality.

def Harley2014.conditions : ArgumentRole → Bool

Whether the number of an argument conditions Hiaki suppletion, read off spellout. That of the sole argument of an intransitive and of the object of a transitive does, and that of the transitive subject does not.

Equations

• One or more equations did not get rendered due to their size.
• Harley2014.conditions ArgumentRole.R = false
• Harley2014.conditions ArgumentRole.T = false

theorem Harley2014.isErgative_conditions : Alignment.IsErgative conditions

Suppletion follows an ergative–absolutive distribution.

theorem Harley2014.suppletion_not_agreement (t : Bobaljik2008.CaseCategory) : Bobaljik2008.controls Alignment.AlignmentType.accusative t ≠ conditions

Suppletion is not agreement. Hiaki case is nominative–accusative ((29)), and no setting of accessibility derives ergative agreement from accusative case (Bobaljik2008.not_isErgative_controls_accusative), so the pattern is local Vocabulary-Item competition, conditioned by the internal argument.

§2.3 Individuation is not semantic: the caboodle item

def Harley2014.cahoot : DistributedMorphology.Root

√548 cahoot ((16)).

Equations

• Harley2014.cahoot = { index := 548 }

def Harley2014.cahootLF : Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem DistributedMorphology.Allosemy.Feature String)

The List-3 entry of √548: "a conspiracy" in the frame of (16), recorded by its categorizing head, and no Elsewhere.

Equations

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

theorem Harley2014.cahoot_no_elsewhere : DistributedMorphology.winner? cahootLF ∅ = none

Outside its frame the caboodle item has no interpretation. The paper adds that no List-3 entry could be a true Elsewhere, since an interpretation must compose with its sister's type; caboodle items make the absence visible.

Both flanks on the Realization carrier

Form varies across contexts (IsProperlySuppletive), meaning does not vary but gaps (an empty interp fiber outside the frame, via Allosemy.toInterpreted): vocabulary is the List-2 map, cahootLF the List-3 map.

def Harley2014.realization : Morphology.Realization DistributedMorphology.Root (Clause.Arguments Number) String

List 2 is a Realization whose fiber at a root is its Elsewhere-selected exponent, and ∅ at an index with no item.

Equations

• Harley2014.realization = { realize := fun (r : DistributedMorphology.Root) (c : Clause.Arguments Number) => (Harley2014.spellout c r).elim ∅ fun (x : String) => {x} }

theorem Harley2014.run_isProperlySuppletive : realization.IsProperlySuppletive run

√322 realizes two nonempty, distinct fibers across two licensed clauses — the go/went case the predicate names (§2.2).

theorem Harley2014.run_hasSuppletiveCore : Morphology.Root.HasSuppletiveCore realization (fun (s : String) => {s}) run

Under the identity core-extraction, vuite/tenne alternate at the core itself — Morphology.Root.HasSuppletiveCore, suppletion proper rather than affixal inflection.

def Harley2014.cahootHead : Morphology.Realization.Interpreted Unit (DistributedMorphology.Neighborhood (List DistributedMorphology.Allosemy.Feature)) Unit String

√548 as a List-3 Realization.Interpreted view.

Equations

• Harley2014.cahootHead = DistributedMorphology.Allosemy.toInterpreted Harley2014.cahootLF

theorem Harley2014.cahoot_interp_gap : cahootHead.interp () (DistributedMorphology.Allosemy.embedding [DistributedMorphology.Allosemy.Feature.cat DistributedMorphology.Categorizer.n]) = {"a conspiracy"} ∧ cahootHead.interp () ∅ = ∅

The caboodle item is interpreted inside its frame and has an empty interp fiber elsewhere — a gap, the meaning-side analogue of an empty realization fiber, so a licensing failure rather than allosemy (§2.3).

One-replacement and the selection of objects

def Harley2014.student : DistributedMorphology.RootCategorization.Lexicon String

The root √STUD of student, nominalized by -ent, with the argument chemistry.

Equations

• Harley2014.student = { x := DistributedMorphology.Categorizer.n, root := "stud", head := "ent", arg := "chemistry" }

def Harley2014.studentWithHair (a : DistributedMorphology.RootCategorization.Attachment) : PhraseStructure.Tree DistributedMorphology.RootCategorization.Cat String

student of chemistry with long hair, the nP of (22) with the adjunct of (23) adjoined to it.

Equations

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

inductive Harley2014.Dependent : Type

The dependents of a noun that one replaces.

• argument : Dependent
• adjunct : Dependent

@[instance_reducible]

instance Harley2014.instDecidableEqDependent : DecidableEq Dependent

Equations

• Harley2014.instDecidableEqDependent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Harley2014.instReprDependent : Repr Dependent

Equations

• Harley2014.instReprDependent = { reprPrec := Harley2014.instReprDependent.repr }

def Harley2014.instReprDependent.repr : Dependent → ℕ → Std.Format

Equations

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

def Harley2014.Dependent.pos (a : DistributedMorphology.RootCategorization.Attachment) : Dependent → Core.Order.TreePath

The position of a dependent in studentWithHair.

Equations

• Harley2014.Dependent.pos a Harley2014.Dependent.argument = { toList := 0 :: a.argPos.toList }
• Harley2014.Dependent.pos a Harley2014.Dependent.adjunct = { toList := [1] }

def Harley2014.OneStrands (a : DistributedMorphology.RootCategorization.Attachment) (d : Dependent) : Prop

one, an nP anaphor, strands the dependent from the root.

Equations

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

@[instance_reducible]

instance Harley2014.instDecidableOneStrands (a : DistributedMorphology.RootCategorization.Attachment) (d : Dependent) : Decidable (OneStrands a d)

Equations

• Harley2014.instDecidableOneStrands a d = Harley2014.instDecidableOneStrands._aux_1 a d

def Harley2014.dependentTable : List (String × Dependent)

The dependents as named in the rows.

Equations

• Harley2014.dependentTable = [("argument", Harley2014.Dependent.argument), ("adjunct", Harley2014.Dependent.adjunct)]

def Harley2014.oneData : List (Dependent × Judgment)

The examples of (18), the dependent each strands with its judgment.

Equations

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

theorem Harley2014.oneData_length : oneData.length = 2

theorem Harley2014.oneStrands_iff (p : Dependent × Judgment) : p ∈ oneData → (p.2 = Judgment.acceptable ↔ OneStrands DistributedMorphology.RootCategorization.Attachment.complement p.1)

One-replacement. one strands exactly the dependents that (18) accepts stranded.

def Harley2014.study : DistributedMorphology.RootCategorization.Lexicon String

The verb study of (21a), with the object physics.

Equations

• Harley2014.study = { x := DistributedMorphology.Categorizer.v, root := "stud", head := "y", arg := "physics" }

def Harley2014.studentOfPhysics : DistributedMorphology.RootCategorization.Lexicon String

The noun student of (21b), with the object physics.

Equations

• Harley2014.studentOfPhysics = { x := DistributedMorphology.Categorizer.n, root := "stud", head := "ent", arg := "physics" }

theorem Harley2014.selector_eq_iff (a : DistributedMorphology.RootCategorization.Attachment) : DistributedMorphology.RootCategorization.selector (DistributedMorphology.RootCategorization.Attachment.tree study a) a.argPos = DistributedMorphology.RootCategorization.selector (DistributedMorphology.RootCategorization.Attachment.tree studentOfPhysics a) a.argPos ↔ a = DistributedMorphology.RootCategorization.Attachment.complement

Selection across categories. The verb and the noun of (21) have their object merged with one head exactly when the root takes the object as its complement.