PHOIBLE 2.0

PHOIBLE 2.0 is a database of 3,020 phoneme inventories, drawn from eight source databases, in which every phoneme is decomposed into distinctive features. Its table has a row for each phoneme of each inventory. An Inventory collects the rows of one inventory, and each of its Phonemes carries the phoneme's glyph, its FeatureMatrix and what the source records about it. The generated inventories are in Data/PHOIBLE/Inventories/, and Data/PHOIBLE/Chart.lean gives the feature matrix of each glyph.

Main definitions

• Data.PHOIBLE.Feature: the features, one column of the table each.
• Data.PHOIBLE.FeatureMatrix: an assignment of + and − to some of the features.
• Data.PHOIBLE.Source: the source databases.
• Data.PHOIBLE.Phoneme, Data.PHOIBLE.Inventory: a phoneme of an inventory, and an inventory.
• Data.PHOIBLE.Inventory.featureMatrices: the feature matrices of an inventory's phonemes.

Implementation notes

Where PHOIBLE has NA, a field is none. This means that the source does not record the value, not that it records an absence; Source says what each source records. A blank dialect, which the SAPHON source writes in place of NA, is none too.

A complex segment, such as a prenasalized stop or a diphthong, has a contour value such as +,- on a feature that changes within it. The feature matrix of such a segment takes the meet of the contour's values in the subsumption order, so it leaves that feature unspecified.

References

• [MMcC19]
• [Hay09]

inductive Data.PHOIBLE.SegmentClass : Type

The class of a segment, the SegmentClass column.

• consonant : SegmentClass
• vowel : SegmentClass
• tone : SegmentClass

@[instance_reducible]

instance Data.PHOIBLE.instDecidableEqSegmentClass : DecidableEq SegmentClass

Equations

• Data.PHOIBLE.instDecidableEqSegmentClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.PHOIBLE.instFintypeSegmentClass : Fintype SegmentClass

Equations

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

inductive Data.PHOIBLE.Source : Type

The source database of an inventory, the Source column. The sources differ in what they record. The AA, PH and SPA sources list the allophones of every phoneme and the others of none, and all but RA, SAPHON and SPA say of every phoneme whether it is marginal. Tones appear only in inventories from AA, PH, RA and SPA.

• spa : Source

  The Stanford Phonology Archive.

• upsid : Source

  The UCLA Phonological Segment Inventory Database.

• aa : Source

  Hartell's Alphabets des langues africaines, as digitized by Chanard.

• ph : Source

  The inventories the PHOIBLE contributors took from grammars, articles and theses, with Christopher Green and Steven Moran's inventories of African and Southeast Asian languages.

• ra : Source

  Ramaswami's survey of the phonetics of the languages of India.

• saphon : Source

  The South American Phonological Inventory Database.

• ea : Source

  The Database of Eurasian Phonological Inventories.

• er : Source

  Erich Round's phonemic inventories of Australian languages.

@[instance_reducible]

instance Data.PHOIBLE.instDecidableEqSource : DecidableEq Source

Equations

• Data.PHOIBLE.instDecidableEqSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.PHOIBLE.instFintypeSource : Fintype Source

Equations

• Data.PHOIBLE.instFintypeSource = { elems := { val := ↑Data.PHOIBLE.Source.enumList, nodup := Data.PHOIBLE.Source.enumList_nodup }, complete := Data.PHOIBLE.instFintypeSource._proof_1 }

inductive Data.PHOIBLE.Feature : Type

Each PHOIBLE feature is a column of the table. The feature system is loosely based on Hayes's and goes beyond it, with features for length, tone and stress among others.

• syllabic : Feature
• short : Feature
• long : Feature
• consonantal : Feature
• sonorant : Feature
• continuant : Feature
• delayedRelease : Feature
• approximant : Feature
• tap : Feature
• trill : Feature
• nasal : Feature
• lateral : Feature
• labial : Feature
• round : Feature
• labiodental : Feature
• coronal : Feature
• anterior : Feature
• distributed : Feature
• strident : Feature
• dorsal : Feature
• high : Feature
• low : Feature
• front : Feature
• back : Feature
• tense : Feature
• retractedTongueRoot : Feature
• advancedTongueRoot : Feature
• periodicGlottalSource : Feature
• epilaryngealSource : Feature
• spreadGlottis : Feature
• constrictedGlottis : Feature
• fortis : Feature
• lenis : Feature
• raisedLarynxEjective : Feature
• loweredLarynxImplosive : Feature
• click : Feature
• tone : Feature
• stress : Feature

@[instance_reducible]

instance Data.PHOIBLE.instDecidableEqFeature : DecidableEq Feature

Equations

• Data.PHOIBLE.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.PHOIBLE.instFintypeFeature : Fintype Feature

Equations

• Data.PHOIBLE.instFintypeFeature = { elems := { val := ↑Data.PHOIBLE.Feature.enumList, nodup := Data.PHOIBLE.Feature.enumList_nodup }, complete := Data.PHOIBLE.instFintypeFeature._proof_1 }

@[reducible, inline]

abbrev Data.PHOIBLE.FeatureMatrix : Type

A feature matrix gives some features the value + (true) or − (false) and leaves the others unspecified, as PHOIBLE's value 0, not applicable, does.

Equations

• Data.PHOIBLE.FeatureMatrix = (Data.PHOIBLE.Feature → Flat Bool)

def Data.PHOIBLE.FeatureMatrix.ofList (l : List (Feature × Bool)) : FeatureMatrix

The feature matrix that gives each listed feature its value, the first where a feature is listed twice, and leaves the others unspecified.

Equations

• Data.PHOIBLE.FeatureMatrix.ofList l f = List.lookup f l

structure Data.PHOIBLE.Phoneme : Type

A phoneme of an inventory is a glyph with its feature matrix and what the inventory's source records about it.

• glyph : String

  The IPA glyph.

• allophones : Option (List String)

  The allophones, among them the glyph itself, and none when the source lists none.

• marginal : Option Bool

  Whether the phoneme is marginal in the inventory, none when the source does not say.

• segmentClass : SegmentClass

  The class of the glyph.

• features : FeatureMatrix

  The feature matrix of the glyph.

structure Data.PHOIBLE.Inventory : Type

An inventory is a list of phonemes with the language variety it describes and its source.

• id : ℕ

  The PHOIBLE inventory identifier.

• glottocode : Option String

  The Glottocode of the variety.

• iso : String

  The ISO 639-3 code of the language.

• languageName : String

  The name of the language.

• specificDialect : Option String

  The dialect described, when the source names one.

• source : Source

  The source database.

• phonemes : List Phoneme

  The phonemes.

def Data.PHOIBLE.Inventory.featureMatrices (I : Inventory) : Finset FeatureMatrix

The feature matrices of an inventory's phonemes.

Equations

• I.featureMatrices = (List.map (fun (x : Data.PHOIBLE.Phoneme) => x.features) I.phonemes).toFinset

@[simp]

theorem Data.PHOIBLE.Inventory.mem_featureMatrices {I : Inventory} {m : FeatureMatrix} : m ∈ I.featureMatrices ↔ ∃ y ∈ I.phonemes, y.features = m

theorem Data.PHOIBLE.Inventory.subset_image_featureMatrices_iff {β : Type u_1} [DecidableEq β] {I : Inventory} {f : FeatureMatrix → β} {S : Finset β} : S ⊆ Finset.image f I.featureMatrices ↔ ∀ x ∈ S, ∃ y ∈ I.phonemes, f y.features = x

A set lies in an image of the feature matrices when each of its elements is the image of a phoneme's matrix, a condition decide checks without deduplicating the inventory.