Documentation

Linglib.Studies.Belth2026

Belth (2026): A Learning-Based Account of Phonological Tiers [Bel26] #

D2L (Distant-to-Local) is an iterative learner that constructs phonological tiers as a byproduct of trying to express alternations as adjacent dependencies. Given underlying-form / surface-form pairs, D2L starts by projecting all segments and tries to predict the alternating segment from its linear neighbours. When the resulting rule fails Yang's Tolerance Principle [Yan16], D2L deletes the offending segments from the tier and tries again, until either a tolerated rule is found or no further deletion helps.

The output of D2L is a tier-based alternation rule, modelled here by the canonical Subregular.TierRule schema (in Phonology/Alternation.lean); the closely-related SPE non-tier Subregular.LocalRewrite.Rule schema in Phonology/Subregular/LocalRewrite.lean is the right substrate when the alternation does not factor through a tier projection. The function-level subregular classification of D2L outputs lives in the subregular function classes: tier-mediated dissimilation rules of the form Belth converges to are Tier-Subsequential ([ARGH20]). For Latin -alis / -aris allomorphy ([Bel26] §5.3, rule 54), the rule D2L converges to is

Disagree([?lat], {lat}) / [+cons] __ ∘ proj(·, [+cons]),

i.e. dissimilation of the underspecified affix-initial liquid /L/ from the immediately preceding [+cons] tier segment. [Bel26] reports 0.97 accuracy on a 121-word Perseus dataset; the residual ~3% errors are tolerated by Yang's Tolerance Principle (4 ≤ 121/ln 121), so D2L converges to this rule rather than memorizing the lexicon.

This study formalizes:

D2L's Turkish (Belth §5.1) and Finnish (§5.2) rules are sketched in §10 below. They require multi-feature dependencies and explicit Elsewhere defaults; both extensions are admittable on demand.

On verification scope. D2L itself — the learning algorithm — is not run inside Lean. Belth's empirical claim is that, given a corpus, D2L converges to specific rules. Verifying that claim end-to-end would require running D2L on naturalistic datasets (CHILDES, MorphoChallenge, Perseus), which is out of scope for a Lean formalization. We instead formalize the learned rules and verify their predictions on representative examples, plus the Tolerance Principle inequality that licenses convergence.

A minimal Latin segment alphabet sufficient for the -alis / -aris contrast. The unspecified affix-initial liquid is L; surface allomorphs are l and r.

Instances For
    @[instance_reducible]
    Equations
    @[instance_reducible]
    Equations
    def Belth2026.instReprLatSeg.repr :
    LatSegStd.Format
    Equations
    Instances For

      [+cons] per [Cse10]'s feature inventory: every non-vowel is consonantal, except the orthographic ⟨v⟩, which [Bel26] treats as the glide [w] ([−cons]). This is the choice that lets pluv-aLis surface as [r] (the tier-preceding consonant of pluv- is /l/, not /v/). L is [+cons] — the underspecified /L/ projects onto the consonant tier even though its [lat] value is not yet fixed.

      Equations
      Instances For
        @[instance_reducible]
        Equations
        • One or more equations did not get rendered due to their size.
        def Belth2026.LatSeg.isLat :
        LatSegOption Bool

        [+lat] per [Cse10]: only l is lateral, and L is underspecified for [lat]. Returning Option Bool rather than Bool here avoids the older "junk default" pattern where L had to fake some concrete value — none is the honest answer.

        Equations
        Instances For

          The consonantal tier (Belth's learned tier for Latin, rule 54). Every [+cons] segment projects.

          Equations
          Instances For

            The rule D2L learns under the [+cons] tier ([Bel26] rule 54): Disagree([?lat], {lat}) / [+cons] __ ∘ proj(·, [+cons]).

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

              Underlying form of popularis 'popular': /popul-aLis/.

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

                Underlying form of pluvalis 'rainy': /pluv-aLis/. With /v/ off the consonant tier (treated as [w], [−cons]), the tier-preceding consonant in pluv-a is /l/.

                Equations
                Instances For

                  Underlying form of lunaris 'lunar': /lun-aLis/. The empirical counterexample: surface is [r], but the rule predicts [l] because the immediately preceding [+cons] segment in /lun-a/ is the nasal /n/ ([−lat]), and Disagree outputs [+lat].

                  Equations
                  Instances For

                    The position of L in each underlying form.

                    Equations
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations
                          Instances For
                            Equations
                            Instances For
                              def Belth2026.predicted (ur : List LatSeg) (lPos : ) :
                              Option Bool

                              Surface value predicted by the learned rule: some true = surfaces as l, some false = surfaces as r, none = the rule has no opinion.

                              Equations
                              Instances For

                                navalis: /v/ is [−cons] (a glide), so the tier-preceding consonant of /nav-a/ is /n/ ([−lat]). Disagree outputs [+lat] = l. ✓

                                popularis: tier-preceding consonant is /l/ ([+lat]). Disagree outputs [−lat] = r. ✓

                                pluvalis: with /v/ off the consonant tier, tier-preceding consonant of /pluv-a/ is /l/ ([+lat]). Disagree outputs [−lat] = r. ✓

                                floralis: tier-preceding consonant is /r/ ([−lat]). The intervening /r/ blocks the dissimilation that popularis's preceding /l/ would have triggered — exactly the long-distance pattern Belth's tier-projection is designed to capture. ✓

                                legalis: tier-preceding consonant is /g/ ([−lat]). The stem-initial /l/ is hidden from /L/ by the intervening /g/ on the consonant tier. ✓

                                navalis (l) vs popularis (r) is the minimal-pair contrast: both have a consonant immediately before the affix on the surface, but only /l/ triggers dissimilation.

                                lunaris: the rule predicts [l] (the last [+cons] segment in /lun-a/ is the nasal /n/, which is [−lat], so Disagree outputs [+lat]). This is the wrong prediction — the surface form is [r]. [Bel26] reports this as one of the ~3% of errors the Tolerance Principle tolerates; D2L does not refine the tier further on this dataset.

                                def Belth2026.latinData :
                                List (List LatSeg × Bool)

                                Witness pairs (underlying-form-prefix, expected-surface-lat-value) for each worked example.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem Belth2026.latinDissimRule_misses_lunaris :
                                  (List.filter (fun (x : List LatSeg × Bool) => match x with | (pre, expected) => !latinDissimRule.applyAt pre == some expected) latinData).length = 1

                                  The learned rule misses exactly one datum out of six (lunaris) — a 5/6 ≈ 83% match on this minimal corpus, the same single-error rate Belth reports at the corpus scale (~3%).

                                  Yang's Tolerance Principle is the productivity gate inside D2L: a rule with n items in scope and e exceptions is tolerated iff en / ln n. For our six worked examples with one exception (lunaris), 1 ≤ 6 / ln 6 ≈ 3.35 — the rule is comfortably under the threshold, matching [Bel26]'s 4-of-121 (~3%) result on the full Perseus corpus.

                                  The threshold inequality for the six-example demo: 1 exception ≤ 6/ln 6.

                                  theorem Belth2026.latinDissimRule_tolerated_on_examples :
                                  Yang2016.tolerates latinData.length (List.filter (fun (x : List LatSeg × Bool) => match x with | (pre, expected) => !latinDissimRule.applyAt pre == some expected) latinData).length

                                  The learned rule passes Yang's Tolerance Principle on the worked examples: its exception count (1, lunaris) fits under the threshold latinData.length / ln latinData.length. This is the productivity certificate that licenses D2L's convergence to latinDissimRule rather than memorizing each form.

                                  The consonant tier projection equals the canonical tierProject from the TSL formalism in the subregular layer. By construction both reduce to List.filter on the [+cons] predicate, so the autosegmental and language-theoretic tiers coincide. This grounds Belth's tier in the TSL_k subregular hierarchy.

                                  The TSL_2 grammar witnessing the Latin allomorphy pattern as a tier-based subregular language: project to the [+cons] tier, then forbid adjacent identical symbols. Lambert's [Lam22a] TSL_k schema, instantiated with IsCons as the tier predicate and the OCP forbidden 2-factor [some x, some x].

                                  Equations
                                  Instances For

                                    Belth's tier-based dissimilation has a natural OCP twin: surface forms produced by the rule should not contain adjacent [+lat] segments on the consonant tier. We expose this connection via Constraints.mkOCPOnTier, which already accepts a generic Tier. A tier-adjacent pair of identical liquids contributes one violation.

                                    Equations
                                    Instances For

                                      The OCP-on-tier evaluation of latinOCP on a candidate is zero iff that candidate is in latinTSLGrammar.lang. Specialization of Subregular.mkOCPOnTier_zero_iff_in_ocp_lang to the Latin grammar. The two perspectives — markedness constraint with zero violations and TSL_2 grammar membership — coincide.

                                      The OT analysis uses a minimal two-constraint inventory:

                                      1. latinOCP (markedness): no adjacent laterals on the [+cons] tier.
                                      2. latinStarR (markedness): the default-[l] preference, penalizing each surface [r].

                                      On this inventory, popularis and pluvalis each force OCP ≫ *r; navalis, floralis, legalis are vacuously satisfied. lunaris is unrankable — its ERC is contradictory (no W, one L), recapitulating the rule's empirical limit.

                                      def Belth2026.substL (val : LatSeg) :
                                      List LatSegList LatSeg

                                      Substitute val for every L in a candidate string. The two surface candidates for an underlying form are substL .l ur and substL .r ur.

                                      Equations
                                      Instances For

                                        Markedness constraint penalizing each surface [r]: the default-[l] preference.

                                        Equations
                                        Instances For

                                          The Latin ranking implied by allomorphy: OCP/[+cons] dominates *r.

                                          Equations
                                          Instances For
                                            def Belth2026.latCands (ur : List LatSeg) :
                                            List (List LatSeg)

                                            The two surface candidates for an underlying form.

                                            Equations
                                            Instances For
                                              @[instance_reducible]

                                              Membership in latinTSLGrammar.lang is decidable: the bridge to the integer-valued OCP score (latinOCP_zero_iff_in_TSL) transports the Decidable (latinOCP c = 0) instance to language membership.

                                              Equations
                                              def Belth2026.latinTSLExpected :
                                              List (List LatSeg × Bool)

                                              The empirically expected TSL_2 membership table for the Belth Latin inventory: each row pairs a candidate with whether the OCP-on-tier grammar should admit it. pluvalis and floralis are the discriminating cases (one candidate excluded for tier-adjacent identicals); navalis admits both (no adjacency); lunaris admits both (the OCP-on-tier grammar's empirical limit — the dissimilation rule fires even though only one tier-lateral is adjacent).

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem Belth2026.latinTSL_correct (p : List LatSeg × Bool) :
                                                p latinTSLExpected(p.1 latinTSLGrammar.lang) = (p.2 = true)

                                                The OCP-on-tier TSL_2 grammar agrees with the expected membership table on every row of latinTSLExpected: the empirical payoff of the latinOCP_zero_iff_in_TSL bridge in one shot.

                                                popularis: OCP fires once on [p,o,p,u,l,a,l,i,s] (the tier-adjacent (l, l)). Only *r-once on the [r]-candidate — but OCP outranks, so [r] wins.

                                                pluvalis: same OCP-ranking-decides pattern as popularis (the consonant tier of /pluv-a/ is [p, l], so substituting Ll creates a tier-adjacent (l, l)).

                                                navalis, floralis, legalis: the [l]-candidate has OCP=0 (no tier-adjacent laterals) and *r=0; the [r]-candidate has *r=1. *r breaks the tie in favour of [l].

                                                lunaris: the OT analysis selects [l], not the empirical [r] — the same error the rule makes (§5). Both candidates have OCP=0 on the consonant tier (the intervening /n/ separates the laterals in /lun-a-l-is/ so they are not tier-adjacent), so *r picks the [l]-candidate.

                                                The ERC induced by popularis (winner [r], loser [l]): OCP prefers the winner (W on constraint 0); *r prefers the loser (L on constraint 1). The full vector is ⟨W, L⟩ = simpleERC 0 1.

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

                                                  The ERC induced by pluvalis: same shape as popularis.

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

                                                    The ERC induced by navalis (winner [l], loser [r]): OCP indifferent, *r prefers the winner. ⟨e, W⟩ — trivial (no L).

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

                                                      The ERC induced by floralis.

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

                                                        The ERC induced by legalis.

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

                                                          The ERC induced by lunaris (taking the empirical [r] as the winner): OCP indifferent (no laterals are tier-adjacent on either candidate), *r prefers the loser [l]. ⟨e, L⟩ — contradictory (no W, one L). No ranking on the inventory ⟨OCP, *r⟩ can satisfy this; the OT formulation thus reproduces exactly the rule's empirical limit.

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

                                                            The five non-lunaris contrasts form a consistent ERC set: the identity ranking (OCP at position 0, *r at position 1) satisfies every word's ranking requirements. Two informative ERCs (popularis, pluvalis) both reduce to simpleERC 0 1; the other three are trivial.

                                                            Bridge to the dominance characterisation: under any ranking satisfying the empirical ERC set (sans lunaris), OCP dominates *r.

                                                            TSL_2 witness: Latin liquid dissimilation is tier-strictly-local at window-size 2.

                                                            BTSL_2 corollary (via IsTierStrictlyLocal.toIsBTSL in Subregular.Multitier): Latin liquid dissimilation is in the multitier closure of strictly local languages, hence consumed by the [Lam26] BTC framework.