Locality domains for contextual allomorphy across the interfaces

[marantz-2013]: contextual allosemy — the choice of a polysemous root's meaning in context — is bounded exactly as contextual allomorphy is, by the spell-out domain of the first category head and by adjacency at the interface, phonological for allomorphy and semantic for allosemy. Past tense conditions the root of taught across a null v but not the root of quantized across -ize ((1)); productive -er, outer -er and -ness, and the verb made from the noun house show a second category head closing the domain ((2), (3), §6.2); global fixes the reading globalize cannot revert, and novelize the one novelization cannot (§6.3). The Japanese continuative nominalizations, Greek -tos statives, and English quantized energy ((5)–(7), Table 6.1) assign a special root meaning over an overt verbalizer because that verbalizer is semantically null and the trigger is noncyclic; their counterparts over an overt adjectivizer cannot. Idioms such as nationalize live in a different domain, below the external argument, which neither contains nor is contained in the root's spell-out domain.

Main definitions

• Head, Morpheme, cyclic, phonNull, semNull, agentive: the heads of the examples, the categorizers as the cyclic heads, and nullness at each interface.
• Row, rows: the paper's words, each with the head whose conditioning of the root is at issue.

Main results

• allomorphy_rows, allosemy_rows: attested conditioning is visible at its interface and blocked conditioning is not.
• idiom_rows: the idiomatic word lies below Voice.
• domains_cross_cut: a head local to the root outside the idiom domain, and one inside the idiom domain outside the root's.
• strong_prediction: a head that conditions the root is the first category head or noncyclic, with only null heads below it (§6.5).

Heads and interfaces

inductive Marantz2013.Head : Type

The heads of the examples: the categorizers, Voice, and the noncyclic tense, participle, and continuative heads.

• n : Head
• v : Head
• a : Head
• voice : Head
• tense : Head
• participle : Head
• continuative : Head

@[instance_reducible]

instance Marantz2013.instDecidableEqHead : DecidableEq Head

Equations

• Marantz2013.instDecidableEqHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Marantz2013.instReprHead.repr : Head → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Marantz2013.instReprHead.repr Marantz2013.Head.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Head.n")).group prec✝
• Marantz2013.instReprHead.repr Marantz2013.Head.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Head.v")).group prec✝
• Marantz2013.instReprHead.repr Marantz2013.Head.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Head.a")).group prec✝
• Marantz2013.instReprHead.repr Marantz2013.Head.voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Head.voice")).group prec✝
• Marantz2013.instReprHead.repr Marantz2013.Head.tense prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Head.tense")).group prec✝
• Marantz2013.instReprHead.repr Marantz2013.Head.participle prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Head.participle")).group prec✝

@[instance_reducible]

instance Marantz2013.instReprHead : Repr Head

Equations

• Marantz2013.instReprHead = { reprPrec := Marantz2013.instReprHead.repr }

inductive Marantz2013.Sem : Type

Whether a head occurrence contributes at LF.

• contentful : Sem
• null : Sem

@[instance_reducible]

instance Marantz2013.instDecidableEqSem : DecidableEq Sem

Equations

• Marantz2013.instDecidableEqSem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Marantz2013.instReprSem : Repr Sem

Equations

• Marantz2013.instReprSem = { reprPrec := Marantz2013.instReprSem.repr }

def Marantz2013.instReprSem.repr : Sem → ℕ → Std.Format

Equations

• Marantz2013.instReprSem.repr Marantz2013.Sem.contentful prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Sem.contentful")).group prec✝
• Marantz2013.instReprSem.repr Marantz2013.Sem.null prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Sem.null")).group prec✝

structure Marantz2013.Morpheme : Type

A head occurrence: its exponent, empty when phonologically null, and its semantic contribution.

• head : Head
• exponent : String
• sem : Sem

def Marantz2013.instDecidableEqMorpheme.decEq (x✝ x✝¹ : Morpheme) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Marantz2013.instDecidableEqMorpheme : DecidableEq Morpheme

Equations

• Marantz2013.instDecidableEqMorpheme = Marantz2013.instDecidableEqMorpheme.decEq

@[instance_reducible]

instance Marantz2013.instReprMorpheme : Repr Morpheme

Equations

• Marantz2013.instReprMorpheme = { reprPrec := Marantz2013.instReprMorpheme.repr }

def Marantz2013.instReprMorpheme.repr : Morpheme → ℕ → Std.Format

Equations

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

def Marantz2013.cyclic (m : Morpheme) : Prop

The category heads are the cyclic heads.

Equations

• Marantz2013.cyclic m = (m.head = Marantz2013.Head.n ∨ m.head = Marantz2013.Head.v ∨ m.head = Marantz2013.Head.a)

def Marantz2013.phonNull (m : Morpheme) : Prop

Phonologically null: no overt exponent.

Equations

• Marantz2013.phonNull m = (m.exponent = "")

def Marantz2013.semNull (m : Morpheme) : Prop

Semantically null: contributes nothing at LF.

Equations

• Marantz2013.semNull m = (m.sem = Marantz2013.Sem.null)

def Marantz2013.agentive (m : Morpheme) : Prop

Introduces the external argument.

Equations

• Marantz2013.agentive m = (m.head = Marantz2013.Head.voice)

@[instance_reducible]

instance Marantz2013.instDecidablePredMorphemeCyclic : DecidablePred cyclic

Equations

• Marantz2013.instDecidablePredMorphemeCyclic x✝ = Marantz2013.instDecidablePredMorphemeCyclic._aux_1 x✝

@[instance_reducible]

instance Marantz2013.instDecidablePredMorphemePhonNull : DecidablePred phonNull

Equations

• Marantz2013.instDecidablePredMorphemePhonNull x✝ = Marantz2013.instDecidablePredMorphemePhonNull._aux_1 x✝

@[instance_reducible]

instance Marantz2013.instDecidablePredMorphemeSemNull : DecidablePred semNull

Equations

• Marantz2013.instDecidablePredMorphemeSemNull x✝ = Marantz2013.instDecidablePredMorphemeSemNull._aux_1 x✝

@[instance_reducible]

instance Marantz2013.instDecidablePredMorphemeAgentive : DecidablePred agentive

Equations

• Marantz2013.instDecidablePredMorphemeAgentive x✝ = Marantz2013.instDecidablePredMorphemeAgentive._aux_1 x✝

The words

inductive Marantz2013.Claim : Type

The paper's claim about a head's conditioning of its root.

• attested : Claim
• blocked : Claim

@[instance_reducible]

instance Marantz2013.instDecidableEqClaim : DecidableEq Claim

Equations

• Marantz2013.instDecidableEqClaim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Marantz2013.instReprClaim : Repr Claim

Equations

• Marantz2013.instReprClaim = { reprPrec := Marantz2013.instReprClaim.repr }

def Marantz2013.instReprClaim.repr : Claim → ℕ → Std.Format

Equations

• Marantz2013.instReprClaim.repr Marantz2013.Claim.attested prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Claim.attested")).group prec✝
• Marantz2013.instReprClaim.repr Marantz2013.Claim.blocked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Marantz2013.Claim.blocked")).group prec✝

@[instance_reducible]

instance Marantz2013.instFintypeClaim : Fintype Claim

Equations

• Marantz2013.instFintypeClaim = { elems := { val := ↑Marantz2013.Claim.enumList, nodup := Marantz2013.Claim.enumList_nodup }, complete := Marantz2013.instFintypeClaim._proof_1 }

structure Marantz2013.Row : Type

A word, the head whose conditioning of the root is at issue, and the paper's claims about allomorphy, allosemy, and idiomatic meaning.

• form : String
• spine : DistributedMorphology.Spine Morpheme
• trigger : Fin self.spine.heads.length
• allomorphy : Option Claim
• allosemy : Option Claim
• idiom : Option Claim

def Marantz2013.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Marantz2013.instReprRow : Repr Row

Equations

• Marantz2013.instReprRow = { reprPrec := Marantz2013.instReprRow.repr }

def Marantz2013.Morpheme.ofLabel (exp : String) : String → Option Morpheme

A head occurrence from the pool's labels; v0 is a semantically null v.

Equations

• Marantz2013.Morpheme.ofLabel exp "n" = some { head := Marantz2013.Head.n, exponent := exp, sem := Marantz2013.Sem.contentful }
• Marantz2013.Morpheme.ofLabel exp "v" = some { head := Marantz2013.Head.v, exponent := exp, sem := Marantz2013.Sem.contentful }
• Marantz2013.Morpheme.ofLabel exp "v0" = some { head := Marantz2013.Head.v, exponent := exp, sem := Marantz2013.Sem.null }
• Marantz2013.Morpheme.ofLabel exp "a" = some { head := Marantz2013.Head.a, exponent := exp, sem := Marantz2013.Sem.contentful }
• Marantz2013.Morpheme.ofLabel exp "voice" = some { head := Marantz2013.Head.voice, exponent := exp, sem := Marantz2013.Sem.contentful }
• Marantz2013.Morpheme.ofLabel exp "T" = some { head := Marantz2013.Head.tense, exponent := exp, sem := Marantz2013.Sem.contentful }
• Marantz2013.Morpheme.ofLabel exp "ptcp" = some { head := Marantz2013.Head.participle, exponent := exp, sem := Marantz2013.Sem.contentful }
• Marantz2013.Morpheme.ofLabel exp "cont" = some { head := Marantz2013.Head.continuative, exponent := exp, sem := Marantz2013.Sem.contentful }
• Marantz2013.Morpheme.ofLabel exp x✝ = none

def Marantz2013.triggerOfLabel : String → Option ℕ

The position of the trigger among the heads, innermost first.

Equations

• Marantz2013.triggerOfLabel "1" = some 0
• Marantz2013.triggerOfLabel "2" = some 1
• Marantz2013.triggerOfLabel "3" = some 2
• Marantz2013.triggerOfLabel "4" = some 3
• Marantz2013.triggerOfLabel x✝ = none

def Marantz2013.Claim.ofLabel : String → Option Claim

Equations

• Marantz2013.Claim.ofLabel "attested" = some Marantz2013.Claim.attested
• Marantz2013.Claim.ofLabel "blocked" = some Marantz2013.Claim.blocked
• Marantz2013.Claim.ofLabel x✝ = none

def Marantz2013.rootNames : List String

The roots of the pool, indexed by first occurrence.

Equations

• Marantz2013.rootNames = (List.filterMap (fun (x : Data.Examples.LinguisticExample) => x.feature? "root") Marantz2013.Examples.all).eraseDups

def Marantz2013.Row.ofExample (ex : Data.Examples.LinguisticExample) : Option Row

Equations

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

theorem Marantz2013.row_ofExample_isSome (ex : Data.Examples.LinguisticExample) : ex ∈ Examples.all → (Row.ofExample ex).isSome = true

def Marantz2013.rows : List Row

The words of (1)–(3), (5)–(7), Table 6.1, and §6.2–6.3.

Equations

• Marantz2013.rows = List.filterMap Marantz2013.Row.ofExample Marantz2013.Examples.all

Predictions

theorem Marantz2013.allomorphy_rows (r : Row) : r ∈ rows → ∀ (c : Claim), r.allomorphy = some c → (r.spine.SeesRoot cyclic phonNull r.trigger ↔ c = Claim.attested)

Allomorphy ((1)–(3), §6.2): the trigger conditions root allomorphy iff it is local and every head between them is phonologically null.

theorem Marantz2013.allosemy_rows (r : Row) : r ∈ rows → ∀ (c : Claim), r.allosemy = some c → (r.spine.SeesRoot cyclic semNull r.trigger ↔ c = Claim.attested)

Allosemy (§6.2–6.4): the trigger fixes a special root meaning iff it is local and every head between them is semantically null — so an overt but semantically null verbalizer lets a noncyclic participle or continuative reach the root, and an overt adjectivizer blocks it.

theorem Marantz2013.idiom_rows (r : Row) : r ∈ rows → r.idiom = some Claim.attested → r.spine.IdiomLocal agentive r.trigger ∧ ¬r.spine.RootLocal cyclic r.trigger

Idiom (§6.3): the idiomatic nationalize lies below any external argument, though its v is not local to the root.

theorem Marantz2013.domains_cross_cut : (∃ r ∈ rows, r.spine.RootLocal cyclic r.trigger ∧ ¬r.spine.IdiomLocal agentive r.trigger) ∧ ∃ r ∈ rows, r.spine.IdiomLocal agentive r.trigger ∧ ¬r.spine.RootLocal cyclic r.trigger

The two domains cross-cut: past tense is local to the root of taught but above Voice, and the v of nationalize is below Voice but outside the root's domain.

theorem Marantz2013.strong_prediction {s : DistributedMorphology.Spine Morpheme} {null : Morpheme → Prop} {i : Fin s.heads.length} (h : s.SeesRoot cyclic null i) : (∀ j < i, null s.heads[j]) ∧ (cyclic s.heads[i] → ∀ j < i, ¬cyclic s.heads[j])

The strong prediction (§6.5): whatever conditions the root across an intervening head sees only null heads below it, and if it is itself a category head it is the first.