CoP-Scope: Cophonological Domain Scope Hierarchy

@cite{rolle-2018}

The CoP-scope hierarchy is @cite{rolle-2018}'s solution to the scope problem for grammatical tone: what determines the domain over which a GT operation applies?

The hierarchy

Within a cophonological domain (CoP), structural positions are ordered by scope:

Spec ϕ > Head ϕ > Complement

A VI in specifier position scopes over the head, and a VI in head position scopes over its complement. At spell-out, syntactic structure is mapped to a morpho-phonological tree via hierarchy exchange, which preserves this asymmetric c-command ordering.

Deriving the dominant GT asymmetry

The dominant GT asymmetry (@cite{rolle-2018} §3.4.1) states that dominant GT triggers are always dependents (affixes, modifiers) and targets are always lexical heads. Here we derive it from the CoP-scope hierarchy rather than stipulating it:

1. Dominant GT requires the trigger to scope over the target
2. The target occupies Head position (it's the lexical head)
3. CoP-scope orders Spec > Head > Complement
4. Only Spec scopes over Head (Complement does not)
5. Spec is a dependent position
6. Therefore dominant triggers must be dependents

The key non-trivial prediction: complements are dependents but CANNOT be dominant triggers, because Complement does not scope over Head. This rules out outward dominance from complements.

inductive Phonology.Autosegmental.CoPScope.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.

@cite{rolle-2018} 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 Phonology.Autosegmental.CoPScope.instDecidableEqCoPPosition : DecidableEq CoPPosition

Equations

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

def Phonology.Autosegmental.CoPScope.instReprCoPPosition.repr : CoPPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.CoPScope.instReprCoPPosition : Repr CoPPosition

Equations

• Phonology.Autosegmental.CoPScope.instReprCoPPosition = { reprPrec := Phonology.Autosegmental.CoPScope.instReprCoPPosition.repr }

def Phonology.Autosegmental.CoPScope.CoPPosition.rank : CoPPosition → ℕ

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

Equations

• Phonology.Autosegmental.CoPScope.CoPPosition.spec.rank = 2
• Phonology.Autosegmental.CoPScope.CoPPosition.head.rank = 1
• Phonology.Autosegmental.CoPScope.CoPPosition.complement.rank = 0

def Phonology.Autosegmental.CoPScope.scopesOver (a b : CoPPosition) : Bool

Does position a scope over position b?

Equations

• Phonology.Autosegmental.CoPScope.scopesOver a b = decide (a.rank > b.rank)

theorem Phonology.Autosegmental.CoPScope.spec_scopes_over_head : scopesOver CoPPosition.spec CoPPosition.head = true

Specifiers scope over heads.

theorem Phonology.Autosegmental.CoPScope.head_scopes_over_complement : scopesOver CoPPosition.head CoPPosition.complement = true

Heads scope over complements.

theorem Phonology.Autosegmental.CoPScope.spec_scopes_over_complement : scopesOver CoPPosition.spec CoPPosition.complement = true

Specifiers scope over complements (transitivity).

theorem Phonology.Autosegmental.CoPScope.no_self_scope (p : CoPPosition) : scopesOver p p = false

No position scopes over itself.

theorem Phonology.Autosegmental.CoPScope.head_not_over_spec : scopesOver CoPPosition.head CoPPosition.spec = false

Heads do not scope over specifiers (asymmetry).

theorem Phonology.Autosegmental.CoPScope.complement_not_over_head : scopesOver CoPPosition.complement CoPPosition.head = false

Complements do not scope over heads (asymmetry).

def Phonology.Autosegmental.CoPScope.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

• Phonology.Autosegmental.CoPScope.CoPPosition.spec.isDependent = true
• Phonology.Autosegmental.CoPScope.CoPPosition.head.isDependent = false
• Phonology.Autosegmental.CoPScope.CoPPosition.complement.isDependent = true

theorem Phonology.Autosegmental.CoPScope.spec_is_dependent : CoPPosition.spec.isDependent = true

Specifiers are dependents.

theorem Phonology.Autosegmental.CoPScope.head_is_not_dependent : CoPPosition.head.isDependent = false

Heads are not dependents.

theorem Phonology.Autosegmental.CoPScope.complement_is_dependent : CoPPosition.complement.isDependent = true

Complements are dependents.

structure Phonology.Autosegmental.CoPScope.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 (@cite{rolle-2018} 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 GrammaticalTone.GTSpec

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

@[implicit_reducible]

instance Phonology.Autosegmental.CoPScope.instReprCoPNode : Repr CoPNode

Equations

• Phonology.Autosegmental.CoPScope.instReprCoPNode = { reprPrec := Phonology.Autosegmental.CoPScope.instReprCoPNode.repr }

def Phonology.Autosegmental.CoPScope.instReprCoPNode.repr : CoPNode → ℕ → Std.Format

Equations

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

def Phonology.Autosegmental.CoPScope.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

def Phonology.Autosegmental.CoPScope.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.

@cite{rolle-2018} 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

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

theorem Phonology.Autosegmental.CoPScope.hierarchyExchange_perm (nodes : List CoPNode) : (hierarchyExchange nodes).length = nodes.length

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

theorem Phonology.Autosegmental.CoPScope.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 Phonology.Autosegmental.CoPScope.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 Phonology.Autosegmental.CoPScope.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 Phonology.Autosegmental.CoPScope.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 Phonology.Autosegmental.CoPScope.head_cannot_dominate_spec : scopesOver CoPPosition.head CoPPosition.spec = false

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