Documentation

Linglib.Theories.Phonology.ItemSpecificity.Separation

Separation theorems for item-specificity theories #

The four sibling files in Theories/Phonology/ItemSpecificity/ — IndexedConstraints (@cite{pater-2010}), ScaledWeights (@cite{coetzee-pater-2008}), UseListed (@cite{zuraw-2000}), and RepresentationStrength (@cite{smolensky-goldrick-2016}, @cite{pierrehumbert-2001}, @cite{todd-pierrehumbert-hay-2019}) — agree that lexical-item identity conditions phonological alternation (typically through token frequency) but disagree on the channel through which it does so.

This file makes the disagreement Lean-provable. For each pair of theories, we construct a tiny concrete witness in which the two theories assign different numerical predictions to the same input. The theorems are not statistical fits or claims about which theory is empirically correct in any particular study — they are proofs that the theories are not extensionally equivalent. Empirical separation must then look for the witness pattern in real data.

Why separations and not implications #

The four theories are not nested: none extends another. They make qualitatively different commitments:

Each separation theorem below picks a contrast where these commitments have observable consequences.

What this file does not prove #

source
structure Phonology.ItemSpecificity.Separation.ToyItem :
Type

A minimal toy item type carrying just a log-frequency: enough to instantiate HasTokenFreq and exercise the four theories. The separation theorems do not depend on linguistic content — only on the frequency channel.

  • logFreq : ℝ
Instances For
    source
    @[implicit_reducible]
    instance Phonology.ItemSpecificity.Separation.instInhabitedToyItem :
    Inhabited ToyItem
    Equations
    source
    def Phonology.ItemSpecificity.Separation.instInhabitedToyItem.default :
    ToyItem
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Phonology.ItemSpecificity.Separation.instHasTokenFreqToyItem :
      HasTokenFreq ToyItem
      Equations
      source
      def Phonology.ItemSpecificity.Separation.baseOne :
      Core.Constraint.OT.NamedConstraint ToyItem

      A toy base constraint that always fires once. The four theories differ only in how they modulate this base violation count, so using a constant base isolates the modulation channel.

      Equations
      Instances For
        source
        theorem Phonology.ItemSpecificity.Separation.sep_indexed_vs_scaled :
        have lo := { logFreq := 5 }; have hi := { logFreq := 10 }; (Indexed.mkCoreOnly 3 baseOne).eval lo = (Indexed.mkCoreOnly 3 baseOne).eval hi ∧ Scaled.scaledWeight 0 1 lo < Scaled.scaledWeight 0 1 hi

        Separation (Indexed vs. Scaled). Two items in the same (high-frequency, "core") stratum with different log-frequencies:

        • Indexed: assigns them equal effective violation counts (the stratum determines everything).
        • Scaled (with nonzero positive slope): assigns the higher-frequency item a strictly greater effective weight.

        The witness uses items at log-frequency 5 and 10 with a stratum cutoff at 3 (so both are "core") and a scaled-weight slope of 1 with base weight 0.

        source
        theorem Phonology.ItemSpecificity.Separation.sep_uselisted_novel_invariant :
        UseListed.dispatch 3 (fun (x : ToyItem) => 99) (fun (x : ToyItem) => 7) { logFreq := 0.5 } = 7

        Separation (UseListed vs. anything else). For an item below the listing threshold ("novel"), UseListed dispatches to the grammar regardless of what the listed-form lookup would have produced.

        Concretely: pick a novel item at log-frequency 0.5 with threshold 3, a "listed form" function that returns the constant 99, and a "grammar" function that returns the constant 7. UseListed dispatches to the grammar (= 7), distinct from the listed surface (= 99).

        source
        theorem Phonology.ItemSpecificity.Separation.sep_uselisted_vs_scaled_on_novel_pair :
        have novelLo := { logFreq := 0.5 }; have novelHi := { logFreq := 2.5 }; UseListed.dispatch 3 (fun (x : ToyItem) => 99) (fun (x : ToyItem) => 7) novelLo = UseListed.dispatch 3 (fun (x : ToyItem) => 99) (fun (x : ToyItem) => 7) novelHi ∧ Scaled.scaledWeight 0 1 novelLo ≠ Scaled.scaledWeight 0 1 novelHi

        Separation (UseListed vs. ScaledWeights). For a novel item, UseListed delivers the grammar's output — unchanged by frequency. ScaledWeights with positive slope, by contrast, scales the weight by frequency even for novel items. The witness compares two novel items with different (sub-threshold) log-frequencies:

        • UseListed: same dispatch (grammar's output) for both.
        • ScaledWeights: distinct effective weights.

        The implication for empirical work is direct: present subjects with novel stimuli at varying log-frequencies (e.g., wug stimuli matched to corpus frequency proxies). UseListed predicts no frequency gradient on novel items; ScaledWeights predicts one.

        source
        theorem Phonology.ItemSpecificity.Separation.sep_repstrength_vs_scaled_compositional :
        have n1 := { logFreq := 5 }; have n2_lo := { logFreq := 1 }; have n2_hi := { logFreq := 7 }; RepStrength.compoundActivation id RepStrength.minCombine n1 n2_lo ≠ RepStrength.compoundActivation id RepStrength.minCombine n1 n2_hi ∧ Scaled.scaledWeight 0 1 { logFreq := 4 } = Scaled.scaledWeight 0 1 { logFreq := 4 }

        Separation (RepStrength vs. Scaled). RepStrength's compound activation depends on constituent frequencies via the combine rule; ScaledWeights' effective weight on a compound depends only on the compound's own frequency. So two compounds with the same compound frequency but different constituent frequencies receive:

        • RepStrength: distinct activations (under min combine, the compound with the lower-activation constituent loses).
        • ScaledWeights: identical effective weights (compound frequency is the only input).

        The concrete witness uses the identity sigmoid (so activation = log frequency) and min combine. Two compounds with different N2 activations get different compoundActivation values.

        source
        theorem Phonology.ItemSpecificity.Separation.sep_indexed_vs_uselisted_routing :
        have hi := { logFreq := 10 }; (Indexed.mkCoreOnly 3 baseOne).eval hi = 1 ∧ UseListed.dispatch 3 (fun (x : ToyItem) => 99) (fun (x : ToyItem) => 7) hi = 99

        Separation (Indexed vs. UseListed). Both theories partition the lexicon at a frequency threshold, but with opposite computational consequences: Indexed routes high-frequency items through the grammar (with stratum-specific constraints firing); UseListed routes them around the grammar (returning a stored surface).

        Concrete witness: above-threshold item, base constraint that always fires.

        • Indexed-CoreOnly: violation count 1 (stratum-specific constraint fires).
        • UseListed: returns the listed surface (99), grammar untouched.

        These two outcomes — 1 and 99 — live in different types (Nat violation count vs. listed surface representation), but structurally the divergence is: Indexed says "compute through grammar", UseListed says "skip grammar".

        source
        theorem Phonology.ItemSpecificity.Separation.sep_repstrength_vs_uselisted_subthreshold :
        have lo := { logFreq := 0.5 }; have hi := { logFreq := 2.5 }; RepStrength.activation id lo ≠ RepStrength.activation id hi ∧ UseListed.dispatch 3 (fun (x : ToyItem) => 99) (fun (x : ToyItem) => 7) lo = UseListed.dispatch 3 (fun (x : ToyItem) => 99) (fun (x : ToyItem) => 7) hi

        Separation (RepStrength vs. UseListed). Two items both below the listing threshold ("novel" from UseListed's perspective):

        • RepStrength: assigns them distinct activations as a continuous function of log-frequency.
        • UseListed: dispatches both to the grammar, which (under any frequency-blind grammar function) returns the same value.

        This is the mirror of sep_uselisted_vs_scaled_on_novel_pair (§3) for the lexicon-side gradient theory: UseListed's storage gate is binary, while RepStrength's activation channel is continuous in log-frequency even within a single stratum.

        Empirical content: with novel stimuli at varying log-frequencies, RepStrength predicts gradient lexical-strength effects; UseListed predicts no frequency gradient on novel items.

        source
        theorem Phonology.ItemSpecificity.Separation.sep_repstrength_vs_indexed_within_stratum :
        have lo := { logFreq := 5 }; have hi := { logFreq := 10 }; RepStrength.activation id lo ≠ RepStrength.activation id hi ∧ (Indexed.mkCoreOnly 3 baseOne).eval lo = (Indexed.mkCoreOnly 3 baseOne).eval hi

        Separation (RepStrength vs. Indexed). Two items in the same Indexed stratum ("core") with different log-frequencies:

        • RepStrength: assigns them distinct activations.
        • Indexed: assigns them the same effective violation count (the stratum determines everything within).

        This is the lexicon-side mirror of sep_indexed_vs_scaled (§2): both Indexed and (Indexed-vs-Scaled) RepStrength take the same contrast, but route it through different cells of the directory's discrete/continuous × grammar/lexicon grid. RepStrength's continuity within a stratum is the discriminating feature.