Chandlee et al. (2019): Learning with Partially Ordered Representations

The paper models strings by structures in which a position may carry several properties, so that sounds share the values of their features, orders structures by the subfactor relation, and takes a grammar to be a set of forbidden subfactors (Definition 8). Its phonological example (section 5.2) bans an alveolar sibilant before a postalveolar one by a single forbidden subfactor of the feature-labelled precedence model, [+str, +ant] before [+str, −ant], where a model with one label per segment must ban sʃ, zʃ, sʒ and zʒ separately. Subfactors are factors in the sense of Core/ModelTheory/Factor.lean, and the models of segment words are Subregular.WordModel with the structure for the feature values, so a feature specification is a one-position subfactor occurring where a segment of its natural class does, and a word's diagram occurs exactly in the words with a subsequence above it. Hansson's symmetric Navajo harmony is the grammar of the paper's subfactor and its mirror image (mem_navajoSibilantHarmony_iff), which the paper's subfactor alone does not express (esh_s_mem_language).

Implementation notes

The learning algorithm of sections 4 and 6 and its correctness are not formalized, nor are the tree models of section 2.

References

• [CEH+19]
• [Han10]

@[reducible, inline]

abbrev ChandleeEtAl2019.featureLanguage : FirstOrder.Language

The signature of feature-labelled models of segment words.

Equations

• ChandleeEtAl2019.featureLanguage = Subregular.wordLanguage (Phonology.Feature × Bool)

Natural classes as subfactors

def ChandleeEtAl2019.strident : Phonology.Segment

The class of the sibilants is [+strident].

Equations

• ChandleeEtAl2019.strident = Phonology.Segment.ofSpecs [(Phonology.Feature.strident, true)]

theorem ChandleeEtAl2019.strident_occurs_iff (w : List Phonology.Segment) : FirstOrder.Language.Factor.Occurs (Subregular.WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) (Subregular.WordModel.diagram (Phonology.Feature × Bool) [strident] ⋯) ↔ ∃ x ∈ w, x.IsSibilant

A one-position subfactor occurs exactly where a segment of its natural class does, so the [+strident] subfactor occurs in the words with a sibilant.

The grammar of section 5.2

def ChandleeEtAl2019.alveolar : Phonology.Segment

The alveolar sibilants are [+strident, +anterior].

Equations

• ChandleeEtAl2019.alveolar = Phonology.Segment.ofSpecs [(Phonology.Feature.strident, true), (Phonology.Feature.anterior, true)]

def ChandleeEtAl2019.postalveolar : Phonology.Segment

The postalveolar sibilants are [+strident, −anterior].

Equations

• ChandleeEtAl2019.postalveolar = Phonology.Segment.ofSpecs [(Phonology.Feature.strident, true), (Phonology.Feature.anterior, false)]

def ChandleeEtAl2019.antPost : featureLanguage.Factor 2

The forbidden subfactor of section 5.2 is an alveolar sibilant before a postalveolar one.

Equations

• ChandleeEtAl2019.antPost = Subregular.WordModel.diagram (Phonology.Feature × Bool) [ChandleeEtAl2019.alveolar, ChandleeEtAl2019.postalveolar] ChandleeEtAl2019.antPost._proof_1

def ChandleeEtAl2019.postAnt : featureLanguage.Factor 2

The mirror image is a postalveolar sibilant before an alveolar one.

Equations

• ChandleeEtAl2019.postAnt = Subregular.WordModel.diagram (Phonology.Feature × Bool) [ChandleeEtAl2019.postalveolar, ChandleeEtAl2019.alveolar] ChandleeEtAl2019.postAnt._proof_1

def ChandleeEtAl2019.language : Set (List Phonology.Segment)

The language of the grammar, Definition 8, holds the words whose subfactors avoid the forbidden one.

Equations

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

theorem ChandleeEtAl2019.language_isStrictlyLocal : featureLanguage.IsStrictlyLocal (fun (w : List Phonology.Segment) => Subregular.WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) 2 language

theorem ChandleeEtAl2019.mem_language_iff (w : List Phonology.Segment) : w ∈ language ↔ ¬FirstOrder.Language.Factor.Occurs (Subregular.WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) antPost

theorem ChandleeEtAl2019.diagram_pair_occurs_iff (d e : Phonology.Segment) (w : List Phonology.Segment) : FirstOrder.Language.Factor.Occurs (Subregular.WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) (Subregular.WordModel.diagram (Phonology.Feature × Bool) [d, e] ⋯) ↔ ∃ (a : Phonology.Segment) (b : Phonology.Segment), [a, b].Sublist w ∧ d ≤ a ∧ e ≤ b

A two-position diagram occurs exactly where a subsequence of two segments lies above it.

theorem ChandleeEtAl2019.alveolar_le_iff (x : Phonology.Segment) : alveolar ≤ x ↔ Hansson2010.sibilantClass x = some true

theorem ChandleeEtAl2019.postalveolar_le_iff (x : Phonology.Segment) : postalveolar ≤ x ↔ Hansson2010.sibilantClass x = some false

theorem ChandleeEtAl2019.antPost_occurs_sibilant_pairs (x : Phonology.Segment) : x ∈ [Hansson2010.s, Hansson2010.z] → ∀ y ∈ [Hansson2010.esh, Hansson2010.ezh], FirstOrder.Language.Factor.Occurs (Subregular.WordModel [x, y] fun (x1 x2 : Fin [x, y].length) => x1 < x2) antPost

One feature-labelled subfactor stands for the four segment factors sʃ, zʃ, sʒ and zʒ.

Symmetric harmony

theorem ChandleeEtAl2019.mem_navajoSibilantHarmony_iff (w : List Phonology.Segment) : w ∈ Hansson2010.navajoSibilantHarmony.language ↔ ¬FirstOrder.Language.Factor.Occurs (Subregular.WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) antPost ∧ ¬FirstOrder.Language.Factor.Occurs (Subregular.WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) postAnt

Hansson's Navajo sibilant harmony is the language of the paper's forbidden subfactor together with its mirror image.

theorem ChandleeEtAl2019.esh_s_mem_language : [Hansson2010.esh, Hansson2010.s] ∈ language ∧ [Hansson2010.esh, Hansson2010.s] ∉ Hansson2010.navajoSibilantHarmony.language

The paper's subfactor alone admits a postalveolar sibilant before an alveolar one, which Navajo's symmetric harmony bans.