Harley (2014): roots as abstract indices

[Har14b] [Mar97] [HM93] [Bob08]

[Har14b] "On the identity of roots" argues that a root terminal (DM's List 1) is neither phonologically nor semantically individuated: it is an abstract index, a syntactic atom identified only by its position in the vocabulary, with its form supplied by List 2 (Vocabulary Insertion) and its meaning by List 3 (the Encyclopedia). The argument is negative on both flanks:

• Phonological identification fails (§2.1–2.2). Hiaki has suppletive roots — one root, two phonologically unrelated forms competing under the Elsewhere Condition. If a root were identified by its phonology (√kæt), root suppletion would be incoherent.
• Semantic identification fails (§2.3–2.4). Cran-morphs (cahoot) have a meaning only inside one licensing frame and none elsewhere, so a root cannot be a Fodorian atomic concept either.

What survives is the index: RootIndex := ℕ here, a √322-style meaningless tag. Distinctness of roots is then true by typing — distinct indices are distinct roots — which is exactly what lets √tenne block √vuite at its index without blocking a different intransitive root (§2.1, Marantz's thought experiment).

This file

• vocabulary — the Hiaki suppletive List-2 entries ([Har14b] (3), (26), (27)), keyed by RootIndex, resolved by the shared DM engine Morphology.DM.VI.vocabularyInsert.
• Selection theorems — the engine picks the attested form per context.
• suppletion_ignores_ergative — the §3.3 ergative-absolutive generalization: suppletion tracks the internal (absolutive) argument's number and is blind to the external (ergative) argument.
• run_index_two_forms — one index, two exponents: phonological individuation would split the root (§2.1–2.2).
• cahoot_no_elsewhere — the cran-morph has an interpretation only in its licensing context and none elsewhere (§2.3), stated on the LF side with the allosemy exponence engine (selectBy, no Elsewhere = none).

The vuite/tenne Elsewhere direction (fn. 16)

The paper's first pass (7) writes the plural tenne as the conditioned form (/ [DP-pl]) and vuite as Elsewhere. Footnote 16 corrects this: in the Hiaki impersonal passive the sole argument is syntactically absent and so number-unspecified, and the root then surfaces as tenne, not as singular vuite. So tenne is the true Elsewhere form and vuite is conditioned by a singular internal argument. We encode the considered (fn. 16) analysis: vuite / [absolutive-sg], tenne elsewhere (plural and number-unspecified).

List 1: roots as abstract indices

@[reducible, inline]

abbrev Harley2014.RootIndex : Type

A List-1 root index: a meaningless √-style tag ([Har14b] §2.4). Individuation is by index alone — distinct indices, distinct roots — so the phonological form (List 2) and the interpretation (List 3) are free to vary without identifying the root.

Equations

• Harley2014.RootIndex = ℕ

def Harley2014.runRoot : RootIndex

√322: the Hiaki root realized vuite/tenne 'run' ([Har14b] (14)).

Equations

• Harley2014.runRoot = 322

def Harley2014.walkRoot : RootIndex

√401: the root realized weye/kaate 'walk' ([Har14b] (26)).

Equations

• Harley2014.walkRoot = 401

def Harley2014.killRoot : RootIndex

√402: the root realized mea/sua 'kill' ([Har14b] (27)).

Equations

• Harley2014.killRoot = 402

def Harley2014.singRoot : RootIndex

√500: a non-suppletive intransitive root ('sing', bwiika), used to show the suppletive rules do not block insertion at other indices.

Equations

• Harley2014.singRoot = 500

The conditioning context

Suppletion is conditioned by number, but — crucially for §3.3 — by the number of the absolutive (internal) argument: the sole argument of an intransitive, the object of a transitive. The ergative (external) argument never conditions it.

inductive Harley2014.Number : Type

Grammatical number of an argument. unspecified is the number-neutral case of [Har14b] fn. 16 (the impersonal passive), which surfaces as the Elsewhere form.

• sg : Number
• pl : Number
• unspecified : Number

@[implicit_reducible]

instance Harley2014.instDecidableEqNumber : DecidableEq Number

Equations

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

def Harley2014.instReprNumber.repr : Number → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Harley2014.instReprNumber.repr Harley2014.Number.sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Harley2014.Number.sg")).group prec✝
• Harley2014.instReprNumber.repr Harley2014.Number.pl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Harley2014.Number.pl")).group prec✝

@[implicit_reducible]

instance Harley2014.instReprNumber : Repr Number

Equations

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

structure Harley2014.Ctx : Type

The morphosyntactic context a suppletive root is spelled out in: the number of its absolutive (internal) argument, plus — for a transitive — the number of its ergative (external) argument, which is never consulted.

• absNumber : Number

  Number of the absolutive (internal) argument — the conditioning one.

• ergNumber : Option Number

  Number of the ergative (external) argument, none if intransitive. Never conditions suppletion (§3.3).

@[implicit_reducible]

instance Harley2014.instDecidableEqCtx : DecidableEq Ctx

Equations

• Harley2014.instDecidableEqCtx = Harley2014.instDecidableEqCtx.decEq

def Harley2014.instDecidableEqCtx.decEq (x✝ x✝¹ : Ctx) : Decidable (x✝ = x✝¹)

Equations

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

def Harley2014.instReprCtx.repr : Ctx → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Harley2014.instReprCtx : Repr Ctx

Equations

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

List 2: the suppletive Vocabulary Items

Each root index has a singular-conditioned entry (specificity 1) and an Elsewhere entry (specificity 0); the DM engine's Elsewhere resolution (vocabularyInsert) selects the more specific matching rule.

def Harley2014.vocabulary : List (Morphology.DM.VI.VocabItem Ctx RootIndex)

The Hiaki suppletive vocabulary ([Har14b] (3), (26), (27)): three suppletive roots, each an sg-conditioned form competing with an Elsewhere form, all keyed by RootIndex.

Equations

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

@[implicit_reducible]

instance Harley2014.instDecidableRelVocabItemCtxRootIndexProdAppliesString : DecidableRel Morphology.Exponence.Applies

Equations

• Harley2014.instDecidableRelVocabItemCtxRootIndexProdAppliesString vi c = instDecidableEqBool (vi.matches c.1 c.2) true

def Harley2014.insert (ctx : Ctx) (idx : RootIndex) : Option String

Spell out root idx in context ctx by Elsewhere competition over vocabulary, resolved by the shared exponence engine (Exponence.realize on the VocabItem specificity score) — the same selection engine as the allosemy LF side below.

Equations

• Harley2014.insert ctx idx = Morphology.Exponence.realize Morphology.DM.VI.VocabItem.specificity Harley2014.vocabulary (ctx, idx)

Selection: the engine picks the attested form

theorem Harley2014.run_sg : insert { absNumber := Number.sg } runRoot = some "vuite"

Singular subject → vuite ([Har14b] (1a)).

theorem Harley2014.run_pl : insert { absNumber := Number.pl } runRoot = some "tenne"

Plural subject → tenne ([Har14b] (1b)).

theorem Harley2014.run_impersonal : insert { absNumber := Number.unspecified } runRoot = some "tenne"

Number-unspecified (impersonal passive) → tenne, the true Elsewhere form ([Har14b] fn. 16): the diagnostic that tenne, not vuite, is Elsewhere.

theorem Harley2014.walk_sg : insert { absNumber := Number.sg } walkRoot = some "weye"

Singular subject → weye ([Har14b] (26a)).

theorem Harley2014.walk_pl : insert { absNumber := Number.pl } walkRoot = some "kaate"

Plural subject → kaate ([Har14b] (26b)).

theorem Harley2014.kill_sgObj : insert { absNumber := Number.sg, ergNumber := some Number.pl } killRoot = some "mea"

Singular object → mea, regardless of the (plural) subject ([Har14b] (27a)).

theorem Harley2014.kill_plObj : insert { absNumber := Number.pl, ergNumber := some Number.sg } killRoot = some "sua"

Plural object → sua, regardless of the (singular) subject ([Har14b] (27b)).

§3.3 The ergative-absolutive conditioning generalization

theorem Harley2014.suppletion_ignores_ergative (n : Number) (e e' : Option Number) (i : RootIndex) : insert { absNumber := n, ergNumber := e } i = insert { absNumber := n, ergNumber := e' } i

Suppletion tracks the absolutive argument ([Har14b] §3.3): the selected form depends only on the internal (absolutive) argument's number; the external (ergative) argument's number is never consulted. This is the ergative-absolutive distribution of suppletive agreement — the challenge to [Bob08]'s marked-case generalization the paper raises.

§2.1 Individuation is not phonological

theorem Harley2014.run_index_two_forms : insert { absNumber := Number.sg } runRoot ≠ insert { absNumber := Number.pl } runRoot

One index, two forms. The single root √322 is realized by two phonologically unrelated exponents (vuite vs tenne). Any identification of the root by its phonological form would split it in two, making suppletion incoherent ([Har14b] §2.2, contra Borer 2009).

theorem Harley2014.suppletive_rule_index_local (n : Number) : insert { absNumber := n } singRoot = none

The suppletive rule is index-local ([Har14b] §2.1, Marantz's thought experiment): tenne competes only at √322, so it does not block insertion at a different intransitive root — a non-suppletive √500 (bwiika 'sing') gets no exponent from this vocabulary. This is why List-1 roots must be individuated (as indices) before spell-out.

§2.3 Individuation is not semantic: the cran-morph on the LF side

The mirror argument on List 3. A cran-morph (cahoot) has an interpretation only inside its licensing frame (in [ [ √ n ] -PL ]) and — unlike an ordinary root — no Elsewhere interpretation ([Har14b] (16)). We state this with the allosemy exponence engine (AllosemicEntry as an Morphology.Exponence.Rule instance): selectBy returns a meaning in the licensed context and none outside it.

def Harley2014.cahootLF : List (Morphology.DM.Allosemy.AllosemicEntry String)

√548 cahoot: a single LF entry, licensed only under n (the idiom frame), with no Elsewhere alloseme ([Har14b] (16)).

Equations

• Harley2014.cahootLF = [{ label := "cahoot", denotation := "a conspiracy", context := { belowCat := some Morphology.DM.Categorizer.n } }]

theorem Harley2014.cahoot_licensed : (Morphology.Exponence.selectBy Morphology.DM.Allosemy.AllosemicEntry.score cahootLF { belowCat := some Morphology.DM.Categorizer.n }).isSome = true

In its licensing context the cran-morph is interpreted.

theorem Harley2014.cahoot_no_elsewhere : (Morphology.Exponence.selectBy Morphology.DM.Allosemy.AllosemicEntry.score cahootLF { }).isNone = true

No Elsewhere interpretation ([Har14b] (16)): outside the licensing frame the cran-morph receives no meaning at all — the LF engine returns none, the semantic analogue of a phonological gap. A Fodorian atomic concept could not behave this way, so the root is not semantically individuated.

The surviving individuation: the index

Both individuation-failure arguments on the shared Realization carrier

The two negative flanks (§2.1–2.2 phonological, §2.3 semantic) are the constancy pair of Morphology.Realization at one index: form varies across contexts (IsProperlySuppletive), meaning does not vary but gaps (an empty interp fiber outside the cran-morph's frame, via AllosemicHead.toInterpreted). The vocabulary of §2.1 is the List-2 map, cahootLF the List-3 map.

The form side wraps this file's insert — the shared Exponence engine (Exponence.realize, argmax) — as a Realization. VI.toRealization wraps the equivalent DM vocabularyInsert, whose List.mergeSort is well-founded-recursive and so kernel-opaque; insert computes, so the fibers reduce and the same theorem lands on the same data.

def Harley2014.realization : Morphology.Realization RootIndex Ctx String

The Hiaki suppletive vocabulary as a Realization: index → its Elsewhere-selected exponent (insert) as a singleton fiber, ∅ at an unlicensed index — the univalent stratum ([Mar97]'s List 2).

Equations

• Harley2014.realization = { realize := fun (r : Harley2014.RootIndex) (c : Harley2014.Ctx) => match Harley2014.insert c r with | some f => {f} | none => ∅ }

theorem Harley2014.run_isProperlySuppletive : realization.IsProperlySuppletive runRoot

Phonological individuation fails, on the carrier ([Har14b] §2.1–2.2): the Hiaki √322 realizes two nonempty, distinct fibers (vuite / tenne) across two licensed contexts — IsProperlySuppletive, the exact √GO case the predicate names. A root identified by its form would split here.

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

√322 is a suppletive-core root, not merely affixally inflected ([Har14b] §2.1): under the monomorphemic-form core extraction (a whole exponent is its own core), vuite/tenne alternate at the core itself — the go/went case of Morphology.Root.HasSuppletiveCore, the certificate axis that distinguishes true suppletion from cat/cats inflection.

def Harley2014.cahootHead : Morphology.DM.Allosemy.AllosemicHead String

√548 cahoot as a List-3 Realization.Interpreted view: one head, the cran-morph's single alloseme.

Equations

• Harley2014.cahootHead = { morpheme := Morphology.DM.Categorizer.n, entries := Harley2014.cahootLF }

theorem Harley2014.cahoot_interp_gap : cahootHead.toInterpreted.interp () { belowCat := some Morphology.DM.Categorizer.n } = {"a conspiracy"} ∧ cahootHead.toInterpreted.interp () { } = ∅

Semantic individuation fails, on the carrier ([Har14b] §2.3): the cran-morph is interpreted (a conspiracy) inside its licensing frame but has an empty interp fiber elsewhere — the meaning-side analogue of an empty realization fiber, a gap rather than contextual variation. So this is a licensing failure, not an IsAllosemous witness: unlike an ordinary root (whose meaning would merely vary), a Fodorian atom could not gap.