Rolle 2018 — Grammatical tone: CoP-scope and Matrix-Basemap Correspondence

[Rol18]'s thesis frames dominant vs. non-dominant grammatical tone (GT) via three problems: the origin (where does the grammatical tune come from?), the erasure (why do the target's underlying tones go unrealized?), and the scope (what determines the domain of the GT operation?). This file formalises Rolle's two central mechanisms; the origin problem is solved by the floating-tone representation (the tune is part of the trigger's UR, in Tone/Grammatical.lean).

• CoP-scope (Ch 6) — the scope problem. Structural positions in a cophonological domain are ordered Spec > Head > Complement, and at spell-out syntactic structure is mapped to a morpho-phonological tree via hierarchy exchange. The dominant-GT asymmetry (triggers are dependents, targets are heads) is derived from this ordering rather than stipulated.
• Matrix-Basemap Correspondence (MxBM-C) (Ch 5) — the erasure problem. Dominant GT is faithfulness to a basemap output (a "deficient projection" of the input with all valued tones stripped), extending Output-Output Correspondence ([Ben97]) to the tonal tier.

Main definitions

CoP-scope

• CoPPosition, CoPPosition.rank, scopesOver, CoPPosition.isDependent
• CoPNode, hierarchyExchange
• dominant_gt_asymmetry_from_scope — derives the asymmetry from scope

Matrix-Basemap Correspondence

• deficientProjection, basemapOutput, tonalTier
• basemapViolations — IDENT-OO ([McCP95]) on the tonal tier, derived from Corr.identViol
• mkBasemapConstraint, tonalOverwrite_basemap_faithful

References

• [Rol18]
• [Ben97], [McCP95] — Output-Output Correspondence
• [Gol76]

CoP-scope: cophonological domain scope hierarchy

CoP-scope positions

inductive Rolle2018.CoPPosition : Type

Structural positions within a cophonological domain (CoP), ordered by scope. The ordering Spec > Head > Complement determines which VI's cophonology takes precedence within the domain.

[Rol18] Ch 6 §6.2: each VI has cophonology-scope over all inwardly located morphemes, and cophonologies apply cyclically up the tree, producing layered grammatical tone effects.

• spec : CoPPosition

  Specifier: outermost scope. Dependents (modifiers, possessors) typically occupy this position.

• head : CoPPosition

  Head: middle scope. Lexical heads (roots, stems) occupy this position.

• complement : CoPPosition

  Complement: innermost scope. Complements and some affixes occupy this position.

@[implicit_reducible]

instance Rolle2018.instDecidableEqCoPPosition : DecidableEq CoPPosition

Equations

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

@[implicit_reducible]

instance Rolle2018.instReprCoPPosition : Repr CoPPosition

Equations

• Rolle2018.instReprCoPPosition = { reprPrec := Rolle2018.instReprCoPPosition.repr }

def Rolle2018.instReprCoPPosition.repr : CoPPosition → ℕ → Std.Format

Equations

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

Scope ordering

def Rolle2018.CoPPosition.rank : CoPPosition → ℕ

Numeric rank for scope ordering: higher rank = wider scope. Spec (2) > Head (1) > Complement (0).

Equations

• Rolle2018.CoPPosition.spec.rank = 2
• Rolle2018.CoPPosition.head.rank = 1
• Rolle2018.CoPPosition.complement.rank = 0

def Rolle2018.scopesOver (a b : CoPPosition) : Bool

Does position a scope over position b?

Equations

• Rolle2018.scopesOver a b = decide (a.rank > b.rank)

theorem Rolle2018.spec_scopes_over_head : scopesOver CoPPosition.spec CoPPosition.head = true

Specifiers scope over heads.

theorem Rolle2018.head_scopes_over_complement : scopesOver CoPPosition.head CoPPosition.complement = true

Heads scope over complements.

theorem Rolle2018.spec_scopes_over_complement : scopesOver CoPPosition.spec CoPPosition.complement = true

Specifiers scope over complements (transitivity).

theorem Rolle2018.no_self_scope (p : CoPPosition) : scopesOver p p = false

No position scopes over itself.

theorem Rolle2018.head_not_over_spec : scopesOver CoPPosition.head CoPPosition.spec = false

Heads do not scope over specifiers (asymmetry).

theorem Rolle2018.complement_not_over_head : scopesOver CoPPosition.complement CoPPosition.head = false

Complements do not scope over heads (asymmetry).

Dependency status (derived from position)

def Rolle2018.CoPPosition.isDependent : CoPPosition → Bool

Whether a position is a dependent position. Derived from the CoP structure: specifiers and complements are dependents; heads are not.

This is not an independent stipulation — it follows from the structural definition of the CoP, where the head is the structural center and specifiers/complements are its dependents.

Equations

• Rolle2018.CoPPosition.spec.isDependent = true
• Rolle2018.CoPPosition.head.isDependent = false
• Rolle2018.CoPPosition.complement.isDependent = true

theorem Rolle2018.spec_is_dependent : CoPPosition.spec.isDependent = true

Specifiers are dependents.

theorem Rolle2018.head_is_not_dependent : CoPPosition.head.isDependent = false

Heads are not dependents.

theorem Rolle2018.complement_is_dependent : CoPPosition.complement.isDependent = true

Complements are dependents.

CoP node — morpho-phonological tree node

structure Rolle2018.CoPNode : Type

A node in a morpho-phonological tree within a cophonological domain. Each node represents a morpheme at a structural position, with an optional grammatical tone specification.

Dependency status is derived from position via CoPPosition.isDependent, not independently stipulated. After hierarchy exchange ([Rol18] Ch 4), syntactic structure maps to a CoP tree where scope ordering determines evaluation order: outer-scoping VIs' cophonologies apply after (and thus override) inner-scoping ones.

• position : CoPPosition

  Structural position within the CoP.

• gtSpec : Option Tone.GTSpec

  Optional GT specification. none if this morpheme has no grammatical tone.

def Rolle2018.instReprCoPNode.repr : CoPNode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rolle2018.instReprCoPNode : Repr CoPNode

Equations

• Rolle2018.instReprCoPNode = { reprPrec := Rolle2018.instReprCoPNode.repr }

def Rolle2018.CoPNode.isDependent (n : CoPNode) : Bool

Derived dependency status: a node is a dependent iff its position is Spec or Complement.

Equations

• n.isDependent = n.position.isDependent

Hierarchy exchange

def Rolle2018.hierarchyExchange (nodes : List CoPNode) : List CoPNode

Hierarchy exchange: map a set of morphemes (from syntactic structure) to a cophonological evaluation order. The result is sorted by scope rank (highest first), so outer-scoping cophonologies are evaluated last — their effects take precedence.

[Rol18] Ch 4: hierarchy exchange preserves the inside-out derivational history of the syntactic module by referencing asymmetrical c-command, mediated through the CoP-scope ordering.

Equations

• Rolle2018.hierarchyExchange nodes = nodes.mergeSort fun (a b : Rolle2018.CoPNode) => decide (a.position.rank ≥ b.position.rank)

theorem Rolle2018.hierarchyExchange_perm (nodes : List CoPNode) : (hierarchyExchange nodes).length = nodes.length

Hierarchy exchange preserves the node set (it only reorders).

Deriving the dominant GT asymmetry

theorem Rolle2018.scopes_over_head_implies_spec (p : CoPPosition) (h : scopesOver p CoPPosition.head = true) : p = CoPPosition.spec

The key lemma: if a position scopes over Head, it must be Spec.

Complement has lower rank than Head, so it cannot scope over Head. Head cannot scope over itself. Only Spec (rank 2 > 1) qualifies.

This is the structural backbone of the dominant GT asymmetry: if dominant GT requires scoping over the head, and only Spec scopes over Head, then dominant triggers must be at Spec.

theorem Rolle2018.scopes_over_head_is_dependent (p : CoPPosition) (h : scopesOver p CoPPosition.head = true) : p.isDependent = true

A position that scopes over Head is a dependent position.

Follows from scopes_over_head_implies_spec (it must be Spec) and spec_is_dependent (Spec is a dependent).

theorem Rolle2018.dominant_gt_asymmetry_from_scope (triggerPos targetPos : CoPPosition) (hTarget : targetPos = CoPPosition.head) (hScope : scopesOver triggerPos targetPos = true) : { triggerIsDependent := triggerPos.isDependent, targetIsHead := !targetPos.isDependent }.holds = true

The dominant GT asymmetry derived from CoP-scope.

Hypotheses:

1. The target is at Head position (it's the lexical head)
2. The trigger scopes over the target (required for dominance)

From these two facts alone, the CoP-scope hierarchy determines:

• The trigger is at Spec (only Spec scopes over Head)
• Spec is a dependent position
• Head is not a dependent position

Therefore DominantGTAsymmetry.holds is satisfied: the trigger is a dependent and the target is a head. The Bool values are computed from positions, not independently stipulated.

Non-trivial prediction: complements are dependents but cannot be dominant triggers, because Complement does not scope over Head.

theorem Rolle2018.complement_cannot_dominate_head : scopesOver CoPPosition.complement CoPPosition.head = false

Complements cannot be dominant triggers despite being dependents: Complement does not scope over Head. This is a non-trivial prediction of the CoP-scope account — the asymmetry is not simply "dependents dominate heads" but specifically "dependents that scope over heads dominate heads."

theorem Rolle2018.head_cannot_dominate_spec : scopesOver CoPPosition.head CoPPosition.spec = false

Heads cannot impose dominant GT on specifiers (outward dominance).

Matrix-Basemap Correspondence (MxBM-C)

A basemap is an abstract I/O mapping derived from a "deficient projection" of the input: all valued (lexical) tones on the target are stripped, leaving only floating (grammatical) tones. Dominant GT = faithfulness to the basemap output; since the basemap has no valued tones to preserve, the matrix output is forced to match the grammatical tune, so the target's underlying tones go unrealized.

Basemap — deficient projection

def Rolle2018.deficientProjection {S : Type} (host : List (Tone.TBU S)) (defaultTone : Tone.TRN) : List (Tone.TBU S)

Strip all tones from a host word, replacing them with a default tone. The deficient projection of [Rol18] Ch 5: the input with all valued (lexical) tones removed, leaving only the segmental skeleton ready to receive floating (grammatical) tones.

The defaultTone is the tone assigned to "unvalued" TBUs — language-specific (often L in African tone languages).

Equations

• Rolle2018.deficientProjection host defaultTone = List.map (fun (tbu : Tone.TBU S) => { seg := tbu.seg, tone := defaultTone }) host

theorem Rolle2018.deficientProjection_uniform {S : Type} (host : List (Tone.TBU S)) (defaultTone : Tone.TRN) : List.map Tone.TBU.tone (deficientProjection host defaultTone) = List.map (fun (x : Tone.TBU S) => defaultTone) host

Deficient projection produces uniform tone: every TBU gets the default tone.

Basemap output

def Rolle2018.basemapOutput {S : Type} [DecidableEq S] [BEq S] [Repr S] (host : List (Tone.TBU S)) (spec : Tone.Spec) (defaultTone : Tone.TRN) : List (Tone.TBU S)

Compute the basemap output: apply the grammatical tune to the deficient projection. This represents what the output would look like if the target had no underlying tones — only the floating tones from the trigger determine the surface pattern.

For replacive-dominant GT with a whole-word melody, the basemap output has the grammatical tune on every TBU.

Equations

• Rolle2018.basemapOutput host spec defaultTone = Tone.tonalOverwrite (Rolle2018.deficientProjection host defaultTone) spec

Tonal tier extraction

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

Extract the tonal tier from a list of TBUs.

Grounded in the Tier abstraction (TierProjection.apply (TierProjection.total TBU.tone)): an erasing string homomorphism (TBU S)* → TRN* in the Kleisli category of Option. The tonal tier is the total (no-erasure) case [Gol76].

Equations

• Rolle2018.tonalTier tbus = (TierProjection.total Tone.TBU.tone).apply tbus

@[simp]

theorem Rolle2018.tonalTier_eq_map {S : Type} (tbus : List (Tone.TBU S)) : tonalTier tbus = List.map Tone.TBU.tone tbus

The tonal tier reduces to List.map TBU.tone (the historical formulation), via TierProjection.total's length-preservation property.

Matrix-Basemap Correspondence — derived from Corr

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

Matrix-Basemap Correspondence violation count: Hamming distance between the matrix tonal tier and the basemap tonal tier.

Derived from Corr.identViol on the (false, true) edge of the binary parallel-pair correspondence between the two tiers. This structurally identifies MxBM-C as IDENT-OO of [McCP95] / [Ben97] specialized to the tonal tier — no separate Hamming implementation, no bridge theorem required.

On unequal-length tiers, the underlying Corr.parallel truncates to the shorter prefix (matching List.zip semantics).

Equations

• Rolle2018.basemapViolations tier₁ tier₂ = (OptimalityTheory.Correspondence.Corr.parallel tier₁ tier₂).identViol OptimalityTheory.Correspondence.Side.lhs OptimalityTheory.Correspondence.Side.rhs

theorem Rolle2018.basemapViolations_self_eq_zero (t : List Tone.TRN) : basemapViolations t t = 0

Self-comparison has zero basemap violations: a tonal tier is perfectly faithful to itself. Derived from Corr.identity_ident_zero.

theorem Rolle2018.basemapViolations_eq_zero_imp (t₁ t₂ : List Tone.TRN) (hLen : t₁.length = t₂.length) (hZero : basemapViolations t₁ t₂ = 0) : t₁ = t₂

Zero basemap violations with equal-length tiers implies the tiers are identical. The equal-length hypothesis is necessary because the underlying Corr.parallel truncates to min.

Constraint bridge

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

Wrap basemapViolations as a Constraint for use in OT tableaux and cophonological evaluation.

Given a fixed basemap output (the tonal tier of the basemap-faithful form), this constraint evaluates each candidate by comparing its tonal tier against the basemap. In [Rol18]'s analysis, dominant triggers promote this constraint above default markedness in their cophonology's subranking.

extractTier converts a candidate to its tonal tier for comparison. This allows the constraint to work with any candidate type, not just raw List TRN.

Equations

• Rolle2018.mkBasemapConstraint basemapTier extractTier c = Rolle2018.basemapViolations (extractTier c) basemapTier

Dominance as basemap faithfulness

theorem Rolle2018.tonalOverwrite_basemap_faithful {S : Type} [DecidableEq S] [BEq S] [Repr S] (host : List (Tone.TBU S)) (t defaultTone : Tone.TRN) : have spec := { name := "", melody := [t], window := Tone.ValuationWindow.whole }; tonalTier (Tone.tonalOverwrite host spec) = tonalTier (basemapOutput host spec defaultTone)

The central theorem of MxBM-C: for replacive-dominant GT with a whole-word single-tone melody, the matrix output's tonal tier equals the basemap output's tonal tier.

This captures [Rol18]'s key insight: dominant GT is not a special deletion rule or markedness constraint, but faithfulness to an abstract basemap. The target's underlying tones go unrealized because the output must match what would happen if those tones were never there.

theorem Rolle2018.basemapOutput_tone_independent_whole {S : Type} [DecidableEq S] [BEq S] [Repr S] (host₁ host₂ : List (Tone.TBU S)) (t defaultTone : Tone.TRN) (hLen : host₁.length = host₂.length) : have spec := { name := "", melody := [t], window := Tone.ValuationWindow.whole }; tonalTier (basemapOutput host₁ spec defaultTone) = tonalTier (basemapOutput host₂ spec defaultTone)

The basemap output's tonal tier is independent of the host's underlying tones: for whole-word replacement, two hosts with different lexical tones but identical segmental content produce the same basemap tonal tier.

The formal content of "transparadigmatic uniformity" ([Rol18] Ch 5): the basemap abstracts away from the paradigmatic tonal variation of the target.