Marantz (2013): Locality Domains for Contextual Allomorphy Across the Interfaces

This file formalizes the locality claim of [Mar13]: 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; a second category head closes the domain, as -er, -ness, and the verb made from the noun house show; global fixes the reading globalize cannot revert. The heads of the examples with their nullness at each interface (Head, Morpheme, cyclic, phonNull, semNull) and the words with the head whose conditioning is at issue (Row, rows) give the results: attested conditioning is visible at its interface and blocked conditioning is not (allomorphy_rows, allosemy_rows), idioms live below Voice in a domain that neither contains nor is contained in the root's (idiom_rows, domains_cross_cut), and a head that conditions the root is the first category head or noncyclic with only null heads below it (strong_prediction).

Implementation notes

The words are the rows of Data/Examples/Marantz2013, the examples of (1) to (3) and (5) to (7) and Table 6.1 of the chapter; the locality predicates are those of Morphology/DistributedMorphology/Locality.

References

• [Mar13]

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

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

@[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.ComplexHead DistributedMorphology.Root 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 : Datum) => x.feature? "root") Marantz2013.Examples.all).eraseDups

def Marantz2013.Row.ofDatum (ex : Datum) : Option Row

Equations

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

theorem Marantz2013.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum 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.ofDatum 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.ComplexHead DistributedMorphology.Root 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.