Documentation

Studies.Rolle2018

Rolle (2018): Grammatical tone: typology and theory #

This file formalizes the dissertation's account of dominant grammatical tone, the replacement of a target's underlying tones by a trigger's grammatical tune, through its two mechanisms. Cophonology-scope answers the scope problem: hierarchy exchange lays the vocabulary items of a specifier–head–complement configuration out from outermost to innermost, Position, and an item's cophonology scopes over everything located inwardly, ScopesOver, so the dominant trigger is the outer item. The dominant-tone asymmetry, that triggers are dependents and lexical heads never impose dominance outward, is read off the order, and the typology table of trigger–target pairs is reproduced once objects sit in specifier position, Row.dominant_iff. Matrix–basemap correspondence answers the erasure problem: a dominant trigger's subranking promotes faithfulness to the output of a basemap derivation whose input is the induced projection of the target with its tones unvalued, basemapOutput, and cophonological evaluation under that subranking selects exactly the candidates whose tonal tier matches the basemap's, coph_selects_basemap_faithful; the same constraint referring to the stem itself yields the recessive pattern, in which the tune does not apply to a valued target.

Implementation notes #

Positions are the three of one specifier–head–complement configuration; a trigger–target pair on a larger spine is read at the configuration containing both, which is how the typology table's rows are placed. Basemap induction is represented by unvaluing the target's tones, the basemap derivation by the overwrite that docks the tune, and matrix–basemap correspondence by identity on the tonal tier, the substrate's Correspondence.identViol. The Izon and Hausa case studies and the treatment of apparent outward dominance are not formalized.

References #

Cophonology-scope #

inductive Rolle2018.Position :

The positions of a specifier–head–complement configuration, ordered from innermost to outermost as hierarchy exchange lays their vocabulary items out in the morpho-phonological tree: the head is outer to its complement and the specifier outer to the head.

complement : Position
head : Position
spec : Position

Instances For

@[instance_reducible]

instance Rolle2018.instDecidableEqPosition :

DecidableEq Position

Equations

Rolle2018.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Rolle2018.instFintypePosition :

Fintype Position

Equations

Rolle2018.instFintypePosition = { elems := { val := ↑Rolle2018.Position.enumList, nodup := Rolle2018.Position.enumList_nodup }, complete := Rolle2018.instFintypePosition._proof_1 }

def Rolle2018.Position.toFin :

Position → Fin 3

Equations

Instances For

theorem Rolle2018.Position.toFin_injective :

Function.Injective toFin

@[instance_reducible]

noncomputable instance Rolle2018.Position.instLinearOrder :

LinearOrder Position

Equations

Rolle2018.Position.instLinearOrder = LinearOrder.lift' Rolle2018.Position.toFin Rolle2018.Position.toFin_injective

def Rolle2018.Position.IsDependent (p : Position) :

A dependent position: any position but the head.

Equations

p.IsDependent = (p ≠ Rolle2018.Position.head)

Instances For

@[instance_reducible]

instance Rolle2018.Position.instDecidablePredIsDependent :

DecidablePred IsDependent

Equations

p.instDecidablePredIsDependent = { decide := !decide (p = Rolle2018.Position.head), reflects_decide := ⋯ }

def Rolle2018.ScopesOver (p q : Position) :

Cophonology-scope: the vocabulary item at p scopes over the item at q when q is located inwardly, so that p's subranking governs the constituent containing both.

Equations

Rolle2018.ScopesOver p q = (q < p)

Instances For

@[instance_reducible]

noncomputable instance Rolle2018.instDecidableRelPositionScopesOver :

DecidableRel ScopesOver

Equations

Rolle2018.instDecidableRelPositionScopesOver p q = { decide := (↑q.toFin).succ.ble ↑p.toFin, reflects_decide := ⋯ }

theorem Rolle2018.scopesOver_head_iff (p : Position) :

ScopesOver p Position.head ↔ p = Position.spec

Only the specifier's item scopes over the head: a dominant trigger targeting a lexical head is a dependent, and an object imposes dominant tone on its verb because it sits in specifier position.

theorem Rolle2018.not_scopesOver_spec (p : Position) :

¬ScopesOver p Position.spec

No item scopes over the specifier's: a lexical head never imposes dominance outward.

theorem Rolle2018.not_scopesOver_of_complement (q : Position) :

¬ScopesOver Position.complement q

The complement's item scopes over nothing.

theorem Rolle2018.isDependent_of_scopesOver_head {p : Position} (h : ScopesOver p Position.head) :

A trigger that scopes over another item is a dependent or the head over its complement.

inductive Rolle2018.Row :

The trigger–target pairs of the dominant-tone asymmetry table, with the positions the dissertation assigns them: an affix is a head taking the root, or the inner stem, as its complement; modifiers and objects are specifiers; an inner item stands to an outer one as the complement of the outer configuration.

affixRoot : Row
outerAffixStem : Row
modifierNoun : Row
outerModifierNoun : Row
objectVerb : Row
rootAffix : Row
innerAffixOuter : Row
nounModifier : Row
innerModifierOuter : Row
verbObject : Row

Instances For

@[instance_reducible]

instance Rolle2018.instDecidableEqRow :

DecidableEq Row

Equations

Rolle2018.instDecidableEqRow x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Rolle2018.instFintypeRow :

Fintype Row

Equations

Rolle2018.instFintypeRow = { elems := { val := ↑Rolle2018.Row.enumList, nodup := Rolle2018.Row.enumList_nodup }, complete := Rolle2018.instFintypeRow._proof_1 }

def Rolle2018.Row.DominantAttested :

The table's dominant column: dominant tone from a dependent onto a lexical head or an inner item is attested, dominant tone outward from a head or from an inner item is not.

Equations

Instances For

@[instance_reducible]

instance Rolle2018.instDecidablePredRowDominantAttested :

DecidablePred Row.DominantAttested

Equations

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

theorem Rolle2018.Row.dominant_iff (r : Row) :

r.DominantAttested ↔ ScopesOver r.trigger r.target

The typology table falls out of cophonology-scope: dominant tone is attested for a trigger–target pair exactly when the trigger's item scopes over the target's.

Matrix–basemap correspondence #

def Rolle2018.tonalTier {S : Type} (tbus : List (Tone.TBU S)) :

The tonal tier, the tone of each tone-bearing unit, along which matrix and basemap outputs are compared.

Equations

Rolle2018.tonalTier tbus = List.map Tone.TBU.tone tbus

Instances For

@[simp]

theorem Rolle2018.tonalTier_eq_map {S : Type} (tbus : List (Tone.TBU S)) :

tonalTier tbus = List.map Tone.TBU.tone tbus

def Rolle2018.basemapViolations (tier₁ tier₂ : List Tone.TRN) :

ℕ

Matrix–basemap correspondence on the tonal tier: the identity violations between two tiers, the substrate's output–output identity restricted to tone.

Equations

Rolle2018.basemapViolations tier₁ tier₂ = (OptimalityTheory.Correspondence.parallel tier₁ tier₂).identViol OptimalityTheory.BinaryRole.lhs OptimalityTheory.BinaryRole.rhs

Instances For

theorem Rolle2018.basemapViolations_self (t : List Tone.TRN) :

basemapViolations t t = 0

theorem Rolle2018.eq_of_basemapViolations_eq_zero {t₁ t₂ : List Tone.TRN} (hLen : t₁.length = t₂.length) (h : basemapViolations t₁ t₂ = 0) :

t₁ = t₂

Tiers of equal length with no identity violation are equal.

def Rolle2018.mxbm {C : Type} (basemapTier : List Tone.TRN) (extractTier : C → List Tone.TRN) :

OptimalityTheory.Constraint C

The matrix–basemap constraint of a trigger's subranking: a candidate's tonal tier against the basemap output's.

Equations

Rolle2018.mxbm basemapTier extractTier c = Rolle2018.basemapViolations (extractTier c) basemapTier

Instances For

theorem Rolle2018.coph_selects_basemap_faithful {L C : Type} [DecidableEq L] [DecidableEq C] (extractTier : C → List Tone.TRN) (l : L) (defaultRanking : List (L × OptimalityTheory.Constraint C)) (candidates : List C) (h : candidates ≠ []) (basemapTier : List Tone.TRN) (hLen : ∀ c ∈ candidates, (extractTier c).length = basemapTier.length) (hFaithful : ∃ c ∈ candidates, extractTier c = basemapTier) (c : C) :

c ∈ OptimalityTheory.Cophonology.cophonologicalEval defaultRanking [(l, mxbm basemapTier extractTier)] candidates h → extractTier c = basemapTier

Promoting matrix–basemap faithfulness in a cophonology selects exactly the basemap-faithful candidates: with a faithful candidate available, every optimal candidate's tonal tier is the basemap's.

theorem Rolle2018.recessive {S L C : Type} [DecidableEq L] [DecidableEq C] (extractTier : C → List Tone.TRN) (l : L) (defaultRanking : List (L × OptimalityTheory.Constraint C)) (candidates : List C) (h : candidates ≠ []) (host : List (Tone.TBU S)) (hLen : ∀ c ∈ candidates, (extractTier c).length = host.length) (hFaithful : ∃ c ∈ candidates, extractTier c = tonalTier host) (c : C) :

c ∈ OptimalityTheory.Cophonology.cophonologicalEval defaultRanking [(l, mxbm (tonalTier host) extractTier)] candidates h → extractTier c = tonalTier host

Recessive grammatical tone: under a subranking promoting faithfulness to the stem itself, every optimal candidate keeps the target's own tones, so the tune does not apply to a valued target.

def Rolle2018.basemapOutput {S : Type} (host : List (Tone.TBU S)) (u : Tone.Tune) :

List (Tone.TBU S)

The basemap output: the trigger's tune docked onto the target's deficient projection, the target with its tones unvalued, which is the structure common to the vocabulary items that the constraint's similarity condition picks out.

Equations

Rolle2018.basemapOutput host u = Tone.overwrite (Tone.unvalue host) u

Instances For

theorem Rolle2018.tonalTier_basemapOutput_singleton {S : Type} (host : List (Tone.TBU S)) (t : Tone.TRN) :

tonalTier (basemapOutput host { melody := [t], anchor := Edge.left }) = List.map (fun (x : Tone.TBU S) => t) host

For a one-tone tune the basemap output carries the tune on every unit, whatever the target's own tones: the locus of erasure.

theorem Rolle2018.dominant {S L C : Type} [DecidableEq L] [DecidableEq C] (extractTier : C → List Tone.TRN) (l : L) (defaultRanking : List (L × OptimalityTheory.Constraint C)) (candidates : List C) (h : candidates ≠ []) (host : List (Tone.TBU S)) (t : Tone.TRN) (hLen : ∀ c ∈ candidates, (extractTier c).length = host.length) (hFaithful : ∃ c ∈ candidates, extractTier c = List.map (fun (x : Tone.TBU S) => t) host) (c : C) :

c ∈ OptimalityTheory.Cophonology.cophonologicalEval defaultRanking [(l, mxbm (tonalTier (basemapOutput host { melody := [t], anchor := Edge.left })) extractTier)] candidates h → extractTier c = List.map (fun (x : Tone.TBU S) => t) host

Dominant grammatical tone: under a subranking promoting faithfulness to the induced basemap, every optimal candidate carries the trigger's whole-word tune, whatever the target's underlying tones were.