Belth (2026): A Learning-Based Account of Phonological Tiers

This file formalizes D2L, Belth's learner, and the paper's own runs of it. D2L receives pairs of underlying and surface forms, an alternating class, and a feature, and constructs the search-and-copy rule Rel(A, F) / C __ ∘ proj(·, T) (Phonology.SearchCopy) from adjacent dependencies alone: starting from the whole alphabet as the tier, it builds the left- and right-context rules whose contexts are the segments tier-adjacent to the targets, counts the applications and correct applications of the more accurate one, accepts it under Yang's Tolerance Principle (Yang2016.tolerates) with the Elsewhere default the untouched targets show, and otherwise deletes from the tier the smallest natural class containing the contexts that produced errors (D2L.iterate, D2L.learn). On the paper's toy vocabulary (20) the learner runs exactly as its trace (21), (30), (32) and (33) says: three iterations with the tiers Σ, [+cons] and [+sib], accuracies 1/8, 4/8 and 7/7, and the rule Agree({S}, {ant}) / [+sib] __ ∘ proj(·, [+sib]) with default [s] (Toy.iterations, Toy.learn). The rules D2L converges to on natural language data are run on the paper's examples: Latin liquid dissimilation (54) on (53), with the lunaris row it mispredicts (latin_rows, lunaris_mispredicted); Finnish backness harmony (52), which is the search-and-copy reading of the fragment's Finnish.palatalHarmony, on (51) (finnish_rows); and Turkish vowel harmony (49a) on (46) and (47) through the fragment's two harmonies (turkish_rows).

Implementation notes

A target with no tier-adjacent segment on the rule's side is an underextension on either side; the paper writes the right word boundary into the right-context set, which changes only that rule's application count, never the choice between the two rules on the paper's data. A context that is itself alternating is never added to the deletion set, since the alternating segments must stay on the tier ((19), step 8); on this reading of (28) the second iteration deletes exactly {n, k, g}. A trigger unspecified for the feature counts as an incorrect application, as the paper counts it. Ties in accuracy go to the left-context rule. Belth's Turkish rule (49a) transmits backness and rounding as one feature set; the fragment factors it into the two harmonies of Göksel and Kerslake, applied in turn. The predictions of section 4 need Finley's and McMullin and Hansson's full stimulus lists, which the paper does not print, so the learned rules (40) and (44) are not run here.

References

• [Bel26]
• [Yan16]
• [GK05]

D2L

structure Belth2026.D2L.Problem (α : Type u_2) [DecidableEq α] : Type u_2

A learning problem consists of the alphabet, the alternating segments A, the feature F read and written on them, the natural classes a tier may lose, and the vocabulary of underlying and surface forms.

• alphabet : List α
• targets : List α
• value : α → Option Bool
• write : Bool → α → α
• value_write (v : Bool) (s : α) : s ∈ self.targets → self.value (self.write v s) = some v
• write_value (v : Bool) (s : α) : s ∈ self.targets → self.value s = some v → self.write v s = s
• classes : List (List α)
• vocabulary : List (List α × List α)

structure Belth2026.D2L.Summary (α : Type u_2) : Type u_2

The applications n and correct applications c of a rule over the vocabulary, the contexts of its incorrect applications, and the surface segments of the targets it leaves untouched.

• n : ℕ
• c : ℕ
• errors : List α
• untouched : List α

@[instance_reducible]

instance Belth2026.D2L.instDecidableEqSummary {α✝ : Type u_2} [DecidableEq α✝] : DecidableEq (Summary α✝)

Equations

• Belth2026.D2L.instDecidableEqSummary = Belth2026.D2L.instDecidableEqSummary.decEq

def Belth2026.D2L.instDecidableEqSummary.decEq {α✝ : Type u_2} [DecidableEq α✝] (x✝ x✝¹ : Summary α✝) : Decidable (x✝ = x✝¹)

Equations

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

def Belth2026.D2L.instReprSummary.repr {α✝ : Type u_2} [Repr α✝] : Summary α✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Belth2026.D2L.instReprSummary {α✝ : Type u_2} [Repr α✝] : Repr (Summary α✝)

Equations

• Belth2026.D2L.instReprSummary = { reprPrec := Belth2026.D2L.instReprSummary.repr }

structure Belth2026.D2L.Iteration (α : Type u_2) : Type u_2

One iteration of D2L records the tier, the two context classes and summaries, the side chosen, the default the chosen rule infers, and the deletion set.

• tier : List α
• contextsL : List α
• contextsR : List α
• left : Summary α
• right : Summary α
• chosen : Edge
• default : Option (Option Bool)
• deletion : List α

@[instance_reducible]

instance Belth2026.D2L.instDecidableEqIteration {α✝ : Type u_2} [DecidableEq α✝] : DecidableEq (Iteration α✝)

Equations

• Belth2026.D2L.instDecidableEqIteration = Belth2026.D2L.instDecidableEqIteration.decEq

def Belth2026.D2L.instDecidableEqIteration.decEq {α✝ : Type u_2} [DecidableEq α✝] (x✝ x✝¹ : Iteration α✝) : Decidable (x✝ = x✝¹)

Equations

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

def Belth2026.D2L.instReprIteration.repr {α✝ : Type u_2} [Repr α✝] : Iteration α✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Belth2026.D2L.instReprIteration {α✝ : Type u_2} [Repr α✝] : Repr (Iteration α✝)

Equations

• Belth2026.D2L.instReprIteration = { reprPrec := Belth2026.D2L.instReprIteration.repr }

def Belth2026.D2L.Iteration.summary {α : Type u_1} (it : Iteration α) : Summary α

The summary of the side an iteration chose.

Equations

• it.summary = match it.chosen with | Edge.left => it.left | Edge.right => it.right

def Belth2026.D2L.Iteration.contexts {α : Type u_1} (it : Iteration α) : List α

The contexts of the side an iteration chose.

Equations

• it.contexts = match it.chosen with | Edge.left => it.contextsL | Edge.right => it.contextsR

def Belth2026.D2L.better {α : Type u_1} (l r : Summary α) : Bool

Whether the left summary is at least as accurate as the right one.

Equations

• Belth2026.D2L.better l r = if l.n = 0 then decide (r.c = 0) else if r.n = 0 then true else decide (r.c * l.n ≤ l.c * r.n)

def Belth2026.D2L.trace {α : Type u_1} (g : Phonology.SearchCopy α) : List α → List α → Option α → Option α → List (Option α × α × α)

For each target on the tier of a form, read in the direction of g, the underlying segment tier-adjacent to it if g applied, the segment g output, and the surface segment. The rule applies when the output segment preceding the target on the tier is a trigger.

Equations

• One or more equations did not get rendered due to their size.
• Belth2026.D2L.trace g x✝³ x✝² x✝¹ x✝ = []

def Belth2026.D2L.applications {α : Type u_1} (g : Phonology.SearchCopy α) (p : List α × List α) : List (Option α × α × α)

The trace of g over a pair of forms, in the direction of g.

Equations

• Belth2026.D2L.applications g p = match g.direction with | Edge.left => Belth2026.D2L.trace g p.1 p.2 none none | Edge.right => Belth2026.D2L.trace g p.1.reverse p.2.reverse none none

def Belth2026.D2L.Problem.precedingContexts {α : Type u_1} [DecidableEq α] (P : Problem α) (T : List α) : List α → Option α → List α

The segments tier-adjacent before the targets of a form on the tier T.

Equations

• P.precedingContexts T [] x✝ = []
• P.precedingContexts T (x_2 :: xs) x✝ = if x_2 ∈ T then (if x_2 ∈ P.targets then x✝.toList else []) ++ P.precedingContexts T xs (some x_2) else P.precedingContexts T xs x✝

def Belth2026.D2L.Problem.contexts {α : Type u_1} [DecidableEq α] (P : Problem α) (T : List α) (d : Edge) : List α

The context class C of the rule on side d over the tier T, every segment tier-adjacent to a target on that side in some underlying form.

Equations

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

def Belth2026.D2L.Problem.candidate {α : Type u_1} [DecidableEq α] (P : Problem α) (T C : List α) (rel : Phonology.SearchCopy.Relation) (d : Edge) (default : Option Bool := none) : Phonology.SearchCopy α

The candidate rule over the tier T with the contexts C.

Equations

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

def Belth2026.D2L.Problem.summary {α : Type u_1} [DecidableEq α] (P : Problem α) (g : Phonology.SearchCopy α) : Summary α

The summary of g over the vocabulary.

Equations

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

def Belth2026.D2L.Problem.inferDefault {α : Type u_1} [DecidableEq α] (P : Problem α) (untouched : List α) : Option (Option Bool)

The Elsewhere default the untouched targets determine; none when their surface forms disagree, which rejects the rule.

Equations

• P.inferDefault untouched = match (List.map P.value untouched).dedup with | [] => some none | [v] => some v | x => none

def Belth2026.D2L.Problem.step {α : Type u_1} [DecidableEq α] (P : Problem α) (rel : Phonology.SearchCopy.Relation) (T D : List α) : Iteration α

The iteration over the tier T with the deletion set D.

Equations

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

def Belth2026.D2L.Problem.deletionClass {α : Type u_1} [DecidableEq α] (P : Problem α) (D : List α) : Option (List α)

The smallest natural class containing D and no target.

Equations

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

def Belth2026.D2L.Problem.nextTier {α : Type u_1} [DecidableEq α] (P : Problem α) (T D : List α) : List α

The tier after deleting the class of D, or D itself when no class contains it.

Equations

• P.nextTier T D = match P.deletionClass D with | some N => List.filter (fun (x : α) => decide (x ∉ N)) T | none => List.filter (fun (x : α) => decide (x ∉ D)) T

def Belth2026.D2L.Problem.iterate {α : Type u_1} [DecidableEq α] (P : Problem α) (rel : Phonology.SearchCopy.Relation) : ℕ → List α → List α → List (Iteration α)

The iterations of D2L from the tier T with the deletion set D, until the tier is empty or stops shrinking.

Equations

• One or more equations did not get rendered due to their size.
• P.iterate rel 0 x✝¹ x✝ = []

def Belth2026.D2L.Problem.rule {α : Type u_1} [DecidableEq α] (P : Problem α) (rel : Phonology.SearchCopy.Relation) (it : Iteration α) : Option (Phonology.SearchCopy α)

The rule an iteration proposes, the chosen side's candidate with its inferred default.

Equations

• P.rule rel it = Option.map (fun (d : Option Bool) => P.candidate it.tier it.contexts rel it.chosen d) it.default

def Belth2026.D2L.Problem.learn {α : Type u_1} [DecidableEq α] (P : Problem α) (rel : Phonology.SearchCopy.Relation) (sat : ℕ → ℕ → Prop) [DecidableRel sat] : Option (Phonology.SearchCopy α)

D2L returns the rule of the first iteration the criterion sat accepts on its applications and exceptions.

Equations

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

The toy vocabulary (20)

inductive Belth2026.Toy.Seg : Type

The segments of the toy vocabulary, with sh for ʃ and S the sibilant unspecified for anteriority.

• sh : Seg
• o : Seg
• k : Seg
• u : Seg
• S : Seg
• i : Seg
• a : Seg
• p : Seg
• n : Seg
• s : Seg
• g : Seg
• t : Seg

@[instance_reducible]

instance Belth2026.Toy.instDecidableEqSeg : DecidableEq Seg

Equations

• Belth2026.Toy.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Belth2026.Toy.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.sh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.sh")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.o")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.k prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.k")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.u")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.S")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.i")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.a")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.p")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.n")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.s")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.g prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.g")).group prec✝
• Belth2026.Toy.instReprSeg.repr Belth2026.Toy.Seg.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.Toy.Seg.t")).group prec✝

@[instance_reducible]

instance Belth2026.Toy.instReprSeg : Repr Seg

Equations

• Belth2026.Toy.instReprSeg = { reprPrec := Belth2026.Toy.instReprSeg.repr }

def Belth2026.Toy.Seg.cons : Seg → Bool

Consonantality.

Equations

• Belth2026.Toy.Seg.o.cons = false
• Belth2026.Toy.Seg.u.cons = false
• Belth2026.Toy.Seg.i.cons = false
• Belth2026.Toy.Seg.a.cons = false
• x✝.cons = true

def Belth2026.Toy.Seg.sib : Seg → Bool

Sibilance.

Equations

• Belth2026.Toy.Seg.sh.sib = true
• Belth2026.Toy.Seg.S.sib = true
• Belth2026.Toy.Seg.s.sib = true
• x✝.sib = false

def Belth2026.Toy.Seg.ant : Seg → Option Bool

Anteriority, unspecified on S and on the vowels.

Equations

• Belth2026.Toy.Seg.s.ant = some true
• Belth2026.Toy.Seg.n.ant = some true
• Belth2026.Toy.Seg.p.ant = some true
• Belth2026.Toy.Seg.t.ant = some true
• Belth2026.Toy.Seg.sh.ant = some false
• Belth2026.Toy.Seg.k.ant = some false
• Belth2026.Toy.Seg.g.ant = some false
• x✝.ant = none

def Belth2026.Toy.alphabet : List Seg

Equations

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

def Belth2026.Toy.classes : List (List Seg)

The natural classes describable by one feature.

Equations

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

def Belth2026.Toy.vocabulary : List (List Seg × List Seg)

The pairs of (20a).

Equations

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

def Belth2026.Toy.problem : D2L.Problem Seg

The problem of (20), with A = {S} and F = {ant}.

Equations

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

def Belth2026.Toy.consTier : List Seg

The consonant tier of the second iteration.

Equations

• Belth2026.Toy.consTier = List.filter Belth2026.Toy.Seg.cons Belth2026.Toy.alphabet

def Belth2026.Toy.sibTier : List Seg

The sibilant tier of the third iteration.

Equations

• Belth2026.Toy.sibTier = List.filter Belth2026.Toy.Seg.sib Belth2026.Toy.alphabet

def Belth2026.Toy.rightUntouched : List Seg

The surface sibilants the right-context rules leave untouched.

Equations

• Belth2026.Toy.rightUntouched = [Belth2026.Toy.Seg.sh, Belth2026.Toy.Seg.sh, Belth2026.Toy.Seg.sh, Belth2026.Toy.Seg.s, Belth2026.Toy.Seg.s, Belth2026.Toy.Seg.s]

theorem Belth2026.Toy.iterations : problem.iterate Phonology.SearchCopy.Relation.agree problem.alphabet.length problem.alphabet [] = [{ tier := alphabet, contextsL := [Seg.u, Seg.a, Seg.o, Seg.i, Seg.t], contextsR := [Seg.i], left := { n := 8, c := 1, errors := [Seg.u, Seg.a, Seg.o, Seg.i], untouched := [] }, right := { n := 2, c := 0, errors := [Seg.i], untouched := rightUntouched }, chosen := Edge.left, default := some none, deletion := [Seg.u, Seg.a, Seg.o, Seg.i] }, { tier := consTier, contextsL := [Seg.sh, Seg.n, Seg.k, Seg.g, Seg.S, Seg.t], contextsR := [Seg.S], left := { n := 8, c := 4, errors := [Seg.n, Seg.k, Seg.g], untouched := [] }, right := { n := 2, c := 0, errors := [], untouched := rightUntouched }, chosen := Edge.left, default := some none, deletion := [Seg.u, Seg.a, Seg.o, Seg.i, Seg.n, Seg.k, Seg.g] }, { tier := sibTier, contextsL := [Seg.sh, Seg.s, Seg.S], contextsR := [Seg.S], left := { n := 7, c := 7, errors := [], untouched := [Seg.s] }, right := { n := 2, c := 0, errors := [], untouched := rightUntouched }, chosen := Edge.left, default := some (some true), deletion := [Seg.u, Seg.a, Seg.o, Seg.i, Seg.n, Seg.k, Seg.g] }]

The paper's trace (21), (30), (32) and (33) is three iterations over the tiers Σ, [+cons] and [+sib], the left rule chosen each time with 1, 4 and 7 correct applications out of 8, 8 and 7, the second iteration deleting n, k and g, and the third leaving only ut-S untouched, whose [s] is the default.

def Belth2026.Toy.rule33 : Phonology.SearchCopy Seg

Rule (33a) with its default, Agree({S}, {ant}) / [+sib] __ ∘ proj(·, [+sib]) and [s] elsewhere.

Equations

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

theorem Belth2026.Toy.learn (sat : ℕ → ℕ → Prop) [DecidableRel sat] (h1 : ¬sat 8 7) (h2 : ¬sat 8 4) (h3 : sat 7 0) : problem.learn Phonology.SearchCopy.Relation.agree sat = some rule33

D2L accepts the third iteration and no earlier one under any criterion that rejects seven exceptions in eight and four in eight and accepts none in seven.

theorem Belth2026.Toy.iterations_disagree : problem.iterate Phonology.SearchCopy.Relation.disagree problem.alphabet.length problem.alphabet [] = [{ tier := alphabet, contextsL := [Seg.u, Seg.a, Seg.o, Seg.i, Seg.t], contextsR := [Seg.i], left := { n := 8, c := 0, errors := [Seg.u, Seg.a, Seg.o, Seg.i, Seg.t], untouched := [] }, right := { n := 2, c := 0, errors := [Seg.i], untouched := rightUntouched }, chosen := Edge.left, default := some none, deletion := [Seg.u, Seg.a, Seg.o, Seg.t, Seg.i] }, { tier := sibTier, contextsL := [Seg.sh, Seg.s, Seg.S], contextsR := [Seg.S], left := { n := 7, c := 2, errors := [Seg.sh, Seg.s], untouched := [Seg.s] }, right := { n := 2, c := 0, errors := [], untouched := rightUntouched }, chosen := Edge.left, default := some (some true), deletion := [Seg.u, Seg.a, Seg.o, Seg.t, Seg.i, Seg.sh, Seg.s] }, { tier := [Seg.S], contextsL := [Seg.S], contextsR := [Seg.S], left := { n := 2, c := 0, errors := [], untouched := rightUntouched }, right := { n := 2, c := 0, errors := [], untouched := rightUntouched }, chosen := Edge.left, default := none, deletion := [Seg.u, Seg.a, Seg.o, Seg.t, Seg.i, Seg.sh, Seg.s] }]

The parallel search for a dissimilatory rule ends with the tiers Σ, [+sib] and {S}.

theorem Belth2026.Toy.learn_disagree (sat : ℕ → ℕ → Prop) [DecidableRel sat] (h1 : ¬sat 8 8) (h2 : ¬sat 7 5) : problem.learn Phonology.SearchCopy.Relation.disagree sat = none

The dissimilatory search finds no rule under any criterion that rejects eight exceptions in eight and five in seven.

Tolerance at the toy's iterations

theorem Belth2026.not_tolerates_8_7 : ¬Yang2016.tolerates 8 7

Seven exceptions among eight applications are not tolerated, since 7 > 8 / ln 8.

theorem Belth2026.not_tolerates_8_4 : ¬Yang2016.tolerates 8 4

Four exceptions among eight applications are not tolerated, since 4 > 8 / ln 8.

theorem Belth2026.Toy.learn_tolerates : problem.learn Phonology.SearchCopy.Relation.agree Yang2016.tolerates = some rule33

With Yang's Tolerance Principle as the criterion, D2L learns rule (33a) from (20).

Latin liquid dissimilation (54)

inductive Belth2026.LatSeg : Type

The segments of the paper's Latin transcriptions; L is the affix liquid unspecified for laterality, v the semivowel.

• a : LatSeg
• e : LatSeg
• i : LatSeg
• o : LatSeg
• u : LatSeg
• l : LatSeg
• r : LatSeg
• L : LatSeg
• n : LatSeg
• v : LatSeg
• s : LatSeg
• g : LatSeg
• f : LatSeg
• p : LatSeg
• b : LatSeg

@[instance_reducible]

instance Belth2026.instDecidableEqLatSeg : DecidableEq LatSeg

Equations

• Belth2026.instDecidableEqLatSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Belth2026.instReprLatSeg : Repr LatSeg

Equations

• Belth2026.instReprLatSeg = { reprPrec := Belth2026.instReprLatSeg.repr }

def Belth2026.instReprLatSeg.repr : LatSeg → ℕ → Std.Format

Equations

• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.a")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.e")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.i")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.o")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.u")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.l")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.r")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.L")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.n")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.v")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.s")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.g prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.g")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.f prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.f")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.p")).group prec✝
• Belth2026.instReprLatSeg.repr Belth2026.LatSeg.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Belth2026.LatSeg.b")).group prec✝

@[instance_reducible]

instance Belth2026.instFintypeLatSeg : Fintype LatSeg

Equations

• Belth2026.instFintypeLatSeg = { elems := { val := ↑Belth2026.LatSeg.enumList, nodup := Belth2026.LatSeg.enumList_nodup }, complete := Belth2026.instFintypeLatSeg._proof_1 }

def Belth2026.LatSeg.IsCons : LatSeg → Prop

The [+cons] tier, every segment but the vowels, L included.

Equations

• Belth2026.LatSeg.a.IsCons = False
• Belth2026.LatSeg.e.IsCons = False
• Belth2026.LatSeg.i.IsCons = False
• Belth2026.LatSeg.o.IsCons = False
• Belth2026.LatSeg.u.IsCons = False
• x✝.IsCons = True

@[instance_reducible]

instance Belth2026.LatSeg.instDecidablePredIsCons : DecidablePred IsCons

Equations

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

def Belth2026.LatSeg.isLat : LatSeg → Option Bool

Laterality, on which l alone is [+lat] and L is unspecified.

Equations

• Belth2026.LatSeg.l.isLat = some true
• Belth2026.LatSeg.L.isLat = none
• x✝.isLat = some false

def Belth2026.LatSeg.ofChar : Char → Option LatSeg

A letter of the transcription.

Equations

• Belth2026.LatSeg.ofChar 'a' = some Belth2026.LatSeg.a
• Belth2026.LatSeg.ofChar 'e' = some Belth2026.LatSeg.e
• Belth2026.LatSeg.ofChar 'i' = some Belth2026.LatSeg.i
• Belth2026.LatSeg.ofChar 'o' = some Belth2026.LatSeg.o
• Belth2026.LatSeg.ofChar 'u' = some Belth2026.LatSeg.u
• Belth2026.LatSeg.ofChar 'l' = some Belth2026.LatSeg.l
• Belth2026.LatSeg.ofChar 'r' = some Belth2026.LatSeg.r
• Belth2026.LatSeg.ofChar 'L' = some Belth2026.LatSeg.L
• Belth2026.LatSeg.ofChar 'n' = some Belth2026.LatSeg.n
• Belth2026.LatSeg.ofChar 'v' = some Belth2026.LatSeg.v
• Belth2026.LatSeg.ofChar 's' = some Belth2026.LatSeg.s
• Belth2026.LatSeg.ofChar 'g' = some Belth2026.LatSeg.g
• Belth2026.LatSeg.ofChar 'f' = some Belth2026.LatSeg.f
• Belth2026.LatSeg.ofChar 'p' = some Belth2026.LatSeg.p
• Belth2026.LatSeg.ofChar 'b' = some Belth2026.LatSeg.b
• Belth2026.LatSeg.ofChar x✝ = none

def Belth2026.latinDissimRule : Phonology.SearchCopy LatSeg

The rule D2L learns under the [+cons] tier is rule (54), Disagree([?lat], {lat}) / [+cons] __ ∘ proj(·, [+cons]), the liquid L taking the opposite laterality of the tier-adjacent consonant.

Equations

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

theorem Belth2026.latinDissimRule_isSubsequential : IsSubsequential Edge.left latinDissimRule.apply

The rule is subsequential, as every search-and-copy rule is.

def Belth2026.latinSegments (s : String) : List LatSeg

The segments of a transcription, the morpheme boundary dropped.

Equations

• Belth2026.latinSegments s = List.filterMap Belth2026.LatSeg.ofChar s.toList

def Belth2026.stem (s : String) : List Char

The stem of a transcription, before the morpheme boundary.

Equations

• Belth2026.stem s = List.takeWhile (fun (x : Char) => decide (x ≠ '-')) s.toList

def Belth2026.latinUR (e : Datum) : List LatSeg

The underlying form of a row, its stem with the affix -aLis.

Equations

• Belth2026.latinUR e = List.filterMap Belth2026.LatSeg.ofChar (Belth2026.stem e.primaryText) ++ [Belth2026.LatSeg.a, Belth2026.LatSeg.L, Belth2026.LatSeg.i, Belth2026.LatSeg.s]

def Belth2026.latinSR (e : Datum) : List LatSeg

The surface form of a row.

Equations

• Belth2026.latinSR e = Belth2026.latinSegments e.primaryText

def Belth2026.latinRows : List Datum

The Latin rows, (53).

Equations

• Belth2026.latinRows = List.filter (fun (x : Datum) => decide (x.language = "lati1261")) Belth2026.Examples.all

theorem Belth2026.latin_rows (e : Datum) : e ∈ latinRows → e.id ≠ "belth2026_53b2" → latinDissimRule.apply (latinUR e) = latinSR e

Rule (54) derives every form of (53) but lunaris, with dissimilation from a tier-adjacent stem l (53b) and its blocking by an intervening r (53c) or non-coronal consonant (53d).

theorem Belth2026.lunaris_mispredicted : latinDissimRule.apply (latinUR Examples.ex_53b2) ≠ latinSR Examples.ex_53b2 ∧ latinDissimRule.apply (latinUR Examples.ex_53b2) = latinSegments "lunalis"

In lunaris the tier-adjacent consonant is the nasal n, so the rule predicts [l], and the form is one of the exceptions the Tolerance Principle absorbs.

Finnish backness harmony (52)

def Belth2026.forms (e : Datum) : List String

The forms of a row listing several, its glossed tokens.

Equations

• Belth2026.forms e = List.map (fun (x : String × String) => x.1) e.glossedTokens

def Belth2026.Finnish.ofChar : Char → Option Phonology.Segment

ofChar c is the segment that the letter c of the paper's IPA transcription writes, which is the Fragment's spelling but for the vowels ɑ, æ and ø.

Equations

• Belth2026.Finnish.ofChar 'ɑ' = some Finnish.a
• Belth2026.Finnish.ofChar 'æ' = some Finnish.ä
• Belth2026.Finnish.ofChar 'ø' = some Finnish.ö
• Belth2026.Finnish.ofChar x✝ = Finnish.ofChar x✝

def Belth2026.Finnish.segments (cs : List Char) : List Phonology.Segment

The segments of a transcription, the morpheme boundary dropped.

Equations

• Belth2026.Finnish.segments cs = List.filterMap Belth2026.Finnish.ofChar cs

def Belth2026.Finnish.ur (form : String) : List Phonology.Segment

The underlying form of a stem with the essive -nA.

Equations

• Belth2026.Finnish.ur form = Belth2026.Finnish.segments (Belth2026.stem form) ++ [Finnish.n, Finnish.A]

theorem Belth2026.Finnish.rows (f : String) : f ∈ forms Examples.ex_51 → Finnish.palatalHarmony.searchCopy.apply (ur f) = segments f.toList

Rule (52) is the search-and-copy reading of the fragment's harmony, whose tier excludes consonants and the neutral vowels and whose Elsewhere default is [−back]; it derives the four forms of (51).

Turkish vowel harmony (49)

def Belth2026.Turkish.ofChar : Char → Option Phonology.Segment

ofChar c is the segment that the letter c of the paper's IPA transcription writes, which is the Fragment's spelling but for the vowels ɑ, ɯ, y and ø and the glide j.

Equations

• Belth2026.Turkish.ofChar 'ɑ' = some Turkish.Phonology.a
• Belth2026.Turkish.ofChar 'ɯ' = some Turkish.Phonology.ı
• Belth2026.Turkish.ofChar 'y' = some Turkish.Phonology.ü
• Belth2026.Turkish.ofChar 'ø' = some Turkish.Phonology.ö
• Belth2026.Turkish.ofChar 'j' = some Turkish.Phonology.y
• Belth2026.Turkish.ofChar x✝ = Turkish.Phonology.ofChar x✝

def Belth2026.Turkish.ofAffixChar : Char → Option Phonology.Segment

A letter of an affix, its vowel the archiphoneme unspecified for the harmonic features.

Equations

• Belth2026.Turkish.ofAffixChar 'ɑ' = some Turkish.Phonology.A
• Belth2026.Turkish.ofAffixChar 'e' = some Turkish.Phonology.A
• Belth2026.Turkish.ofAffixChar 'ɯ' = some Turkish.Phonology.I
• Belth2026.Turkish.ofAffixChar 'i' = some Turkish.Phonology.I
• Belth2026.Turkish.ofAffixChar 'u' = some Turkish.Phonology.I
• Belth2026.Turkish.ofAffixChar 'y' = some Turkish.Phonology.I
• Belth2026.Turkish.ofAffixChar x✝ = Belth2026.Turkish.ofChar x✝

def Belth2026.Turkish.segments (s : String) : List Phonology.Segment

The segments of a form, the morpheme boundaries dropped.

Equations

• Belth2026.Turkish.segments s = List.filterMap Belth2026.Turkish.ofChar s.toList

def Belth2026.Turkish.ur (form : String) : List Phonology.Segment

The underlying form of a stem with its affixes, whose vowels are archiphonemes.

Equations

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

theorem Belth2026.Turkish.rows (e : Datum) : e ∈ [Examples.ex_46, Examples.ex_47] → ∀ f ∈ forms e, Turkish.Phonology.surface (ur f) = segments f

Rule (49a), backness and rounding from the tier-preceding vowel, is the fragment's two harmonies applied in turn; its surface forms derive the forms of (46) and (47).