Harley (2014): On the identity of roots

This file formalizes [harley-2014]'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.

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

• [harley-2014]
• [bobaljik-2008]

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

What 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: the internal argument is the terminal below; 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) : List (DistributedMorphology.VocabularyItem SiteFeature String)

A suppletive root's 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 : List (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, two phonologically unrelated forms: 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: a non-suppletive intransitive root receives no exponent from vocabulary — 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.conditioningPattern : Minimalist.AgreementPattern

Which arguments condition Hiaki suppletion, read off spellout: the sole argument of an intransitive and the object of a transitive, not the transitive subject.

Equations

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

theorem Harley2014.conditioningPattern_isErgAbs : conditioningPattern.isErgAbs = true

Suppletion follows an ergative–absolutive distribution.

theorem Harley2014.suppletion_not_agreement (t : Minimalist.CaseAccessibility) : Minimalist.agreementFromThreshold Minimalist.nomAcc t ≠ conditioningPattern

Suppletion is not agreement: Hiaki case is nominative–accusative ((29)), and no agreement threshold over nominative–accusative case yields an ergative–absolutive pattern (Minimalist.nomAcc_no_ergAbs_agreement, [bobaljik-2008]'s generalization) — 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 : List (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 as a Realization: a root's Elsewhere-selected exponent as a singleton fiber, ∅ 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).