Documentation

Linglib.Data.PHOIBLE.Schema

PHOIBLE 2.0 schema #

@cite{moran-mccloy-2019}

Substrate types for the PHOIBLE 2.0 phonological inventory database (Moran & McCloy 2019, http://phoible.org, DOI 10.5281/zenodo.2626687).

PHOIBLE 2.0 contains 3000+ inventories (doculects) covering 2100+ ISO 639-3 language codes. Each entry is a (languoid × phoneme) pair with distinctive- feature decomposition. The CSV data/phoible-2019/phoible.csv has 49 columns and ~105K rows.

This Lean substrate mirrors the row-level structure: an Inventory is a list of Phonemes, each carrying a FeatureMatrix of 37 PHOIBLE features. Per-inventory data lives in Data/PHOIBLE/Inventories/{Lang}.lean, auto-generated by scripts/gen_phoible.py.

Relation to WALS / Maddieson 2013 #

PHOIBLE 2.0 is the field-canonical successor to UPSID and to WALS Maddieson chapters 1–19 for inventory facts: ~3000 inventories vs. WALS's ~563 languages, with the original transcribed inventory preserved (rather than collapsed into Maddieson's 5-bin partition). The two are complementary: WALS gives partition-based typology; PHOIBLE gives the underlying inventories. Bridge theorems WALS↔PHOIBLE (e.g. WALS Ch 1 inventory-size bin matches PHOIBLE inventory cardinality) live in Phenomena/Phonology/Studies/Maddieson2013.lean (when written).

Citation #

Moran, Steven & McCloy, Daniel (eds.) 2019. PHOIBLE 2.0. Jena: Max Planck Institute for the Science of Human History. http://phoible.org. DOI: 10.5281/zenodo.2626687

inductive Data.PHOIBLE.FeatureValue :

A PHOIBLE distinctive-feature value: present (+), absent (-), or not applicable (0). PHOIBLE encodes underspecification with 0, not by omission.

plus : FeatureValue
minus : FeatureValue
zero : FeatureValue

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instDecidableEqFeatureValue :

DecidableEq FeatureValue

Equations

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

@[implicit_reducible]

instance Data.PHOIBLE.instBEqFeatureValue :

BEq FeatureValue

Equations

Data.PHOIBLE.instBEqFeatureValue = { beq := Data.PHOIBLE.instBEqFeatureValue.beq }

def Data.PHOIBLE.instBEqFeatureValue.beq :

FeatureValue → FeatureValue → Bool

Equations

Data.PHOIBLE.instBEqFeatureValue.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instReprFeatureValue :

Repr FeatureValue

Equations

Data.PHOIBLE.instReprFeatureValue = { reprPrec := Data.PHOIBLE.instReprFeatureValue.repr }

def Data.PHOIBLE.instReprFeatureValue.repr :

FeatureValue → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instInhabitedFeatureValue :

Inhabited FeatureValue

Equations

Data.PHOIBLE.instInhabitedFeatureValue = { default := Data.PHOIBLE.instInhabitedFeatureValue.default }

def Data.PHOIBLE.instInhabitedFeatureValue.default :

Equations

Data.PHOIBLE.instInhabitedFeatureValue.default = Data.PHOIBLE.FeatureValue.plus

Instances For

inductive Data.PHOIBLE.SegmentClass :

PHOIBLE segment class (the SegmentClass column).

consonant : SegmentClass
vowel : SegmentClass
tone : SegmentClass

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instDecidableEqSegmentClass :

DecidableEq SegmentClass

Equations

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

def Data.PHOIBLE.instBEqSegmentClass.beq :

SegmentClass → SegmentClass → Bool

Equations

Data.PHOIBLE.instBEqSegmentClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instBEqSegmentClass :

BEq SegmentClass

Equations

Data.PHOIBLE.instBEqSegmentClass = { beq := Data.PHOIBLE.instBEqSegmentClass.beq }

@[implicit_reducible]

instance Data.PHOIBLE.instReprSegmentClass :

Repr SegmentClass

Equations

Data.PHOIBLE.instReprSegmentClass = { reprPrec := Data.PHOIBLE.instReprSegmentClass.repr }

def Data.PHOIBLE.instReprSegmentClass.repr :

SegmentClass → Nat → Std.Format

Equations

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

Instances For

inductive Data.PHOIBLE.Source :

PHOIBLE source database (the Source column). PHOIBLE aggregates nine donor databases.

spa : Source
Stanford Phonology Archive.
upsid : Source
UCLA Phonological Segment Inventory Database.
aa : Source
Alphabets of Africa (Hartell 1993, Chanard 2006).
gm : Source
Sounds of the World's Languages (Maddieson & Disner 1984).
ph : Source
Christopher Green & Steven Moran's African inventories.
ra : Source
Ramaswami's Indian languages collection (1999).
saphon : Source
South American Phonological Inventory Database (Michael et al.).
ea : Source
Eurasia (Nikolaev).
er : Source
Eric Round's Australian.

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instDecidableEqSource :

DecidableEq Source

Equations

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

@[implicit_reducible]

instance Data.PHOIBLE.instBEqSource :

Equations

Data.PHOIBLE.instBEqSource = { beq := Data.PHOIBLE.instBEqSource.beq }

def Data.PHOIBLE.instBEqSource.beq :

Source → Source → Bool

Equations

Data.PHOIBLE.instBEqSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Data.PHOIBLE.instReprSource.repr :

Source → Nat → Std.Format

Equations

Data.PHOIBLE.instReprSource.repr Data.PHOIBLE.Source.spa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.PHOIBLE.Source.spa")).group prec✝
Data.PHOIBLE.instReprSource.repr Data.PHOIBLE.Source.upsid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.PHOIBLE.Source.upsid")).group prec✝
Data.PHOIBLE.instReprSource.repr Data.PHOIBLE.Source.aa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.PHOIBLE.Source.aa")).group prec✝
Data.PHOIBLE.instReprSource.repr Data.PHOIBLE.Source.gm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.PHOIBLE.Source.gm")).group prec✝
Data.PHOIBLE.instReprSource.repr Data.PHOIBLE.Source.ph prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.PHOIBLE.Source.ph")).group prec✝
Data.PHOIBLE.instReprSource.repr Data.PHOIBLE.Source.ra prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.PHOIBLE.Source.ra")).group prec✝
Data.PHOIBLE.instReprSource.repr Data.PHOIBLE.Source.saphon prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.PHOIBLE.Source.saphon")).group prec✝
Data.PHOIBLE.instReprSource.repr Data.PHOIBLE.Source.ea prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.PHOIBLE.Source.ea")).group prec✝
Data.PHOIBLE.instReprSource.repr Data.PHOIBLE.Source.er prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.PHOIBLE.Source.er")).group prec✝

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instReprSource :

Equations

Data.PHOIBLE.instReprSource = { reprPrec := Data.PHOIBLE.instReprSource.repr }

structure Data.PHOIBLE.FeatureMatrix :

PHOIBLE 37-feature distinctive-feature matrix. Each value is +/-/0 per the PHOIBLE feature mapping tables. The feature inventory follows the PHOIBLE-Hayes feature system (cf. phoible/dev/raw-data/FEATURES/).

syllabic : FeatureValue
short_ : FeatureValue
long_ : FeatureValue
consonantal : FeatureValue
sonorant : FeatureValue
continuant : FeatureValue
delayedRelease : FeatureValue
approximant : FeatureValue
tap : FeatureValue
trill : FeatureValue
nasal : FeatureValue
lateral : FeatureValue
labial : FeatureValue
round_ : FeatureValue
labiodental : FeatureValue
coronal : FeatureValue
anterior : FeatureValue
distributed : FeatureValue
strident : FeatureValue
dorsal : FeatureValue
high : FeatureValue
low : FeatureValue
front : FeatureValue
back : FeatureValue
tense : FeatureValue
retractedTongueRoot : FeatureValue
advancedTongueRoot : FeatureValue
periodicGlottalSource : FeatureValue
epilaryngealSource : FeatureValue
spreadGlottis : FeatureValue
constrictedGlottis : FeatureValue
fortis : FeatureValue
lenis : FeatureValue
raisedLarynxEjective : FeatureValue
loweredLarynxImplosive : FeatureValue
click : FeatureValue
tone : FeatureValue
The PHOIBLE-flagged tone feature (column "tone").
stress : FeatureValue
The PHOIBLE-flagged stress feature (column "stress").

Instances For

def Data.PHOIBLE.instReprFeatureMatrix.repr :

FeatureMatrix → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instReprFeatureMatrix :

Repr FeatureMatrix

Equations

Data.PHOIBLE.instReprFeatureMatrix = { reprPrec := Data.PHOIBLE.instReprFeatureMatrix.repr }

def Data.PHOIBLE.instDecidableEqFeatureMatrix.decEq (x✝ x✝¹ : FeatureMatrix) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instDecidableEqFeatureMatrix :

DecidableEq FeatureMatrix

Equations

Data.PHOIBLE.instDecidableEqFeatureMatrix = Data.PHOIBLE.instDecidableEqFeatureMatrix.decEq

structure Data.PHOIBLE.Phoneme :

A single PHOIBLE phoneme entry: IPA glyph + feature matrix + metadata.

glyph : String
IPA representation (the Phoneme column).
glyphId : String
Hex-encoded Unicode codepoint sequence (the GlyphID column).
allophones : List String
Allophones as a space-separated IPA list (the Allophones column). Empty when NA in source.
marginal : Bool
Whether the segment is marginal in the inventory (the Marginal column: + → true, NA → false).
segmentClass : SegmentClass
features : FeatureMatrix

Instances For

def Data.PHOIBLE.instReprPhoneme.repr :

Phoneme → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instReprPhoneme :

Equations

Data.PHOIBLE.instReprPhoneme = { reprPrec := Data.PHOIBLE.instReprPhoneme.repr }

def Data.PHOIBLE.instDecidableEqPhoneme.decEq (x✝ x✝¹ : Phoneme) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instDecidableEqPhoneme :

DecidableEq Phoneme

Equations

Data.PHOIBLE.instDecidableEqPhoneme = Data.PHOIBLE.instDecidableEqPhoneme.decEq

structure Data.PHOIBLE.Inventory :

A PHOIBLE inventory: one row per (inventory × phoneme) collapsed into one struct per inventory.

id : Nat
PHOIBLE InventoryID (unique per inventory).
glottocode : String
Glottolog code.
iso : String
ISO 639-3 code (may be empty for some doculects).
languageName : String
specificDialect : String
Specific dialect, if recorded; empty when NA in source.
source : Source
phonemes : List Phoneme
The inventory's full phoneme list.

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instReprInventory :

Equations

Data.PHOIBLE.instReprInventory = { reprPrec := Data.PHOIBLE.instReprInventory.repr }

def Data.PHOIBLE.instReprInventory.repr :

Inventory → Nat → Std.Format

Equations

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

Instances For

def Data.PHOIBLE.instDecidableEqInventory.decEq (x✝ x✝¹ : Inventory) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Data.PHOIBLE.instDecidableEqInventory :

DecidableEq Inventory

Equations

Data.PHOIBLE.instDecidableEqInventory = Data.PHOIBLE.instDecidableEqInventory.decEq

def Data.PHOIBLE.Inventory.size (inv : Inventory) :

Nat

Number of phonemes in an inventory.

Equations

inv.size = inv.phonemes.length

Instances For

def Data.PHOIBLE.Inventory.consonantCount (inv : Inventory) :

Nat

Number of consonants in an inventory.

Equations

inv.consonantCount = (List.filter (fun (x : Data.PHOIBLE.Phoneme) => x.segmentClass == Data.PHOIBLE.SegmentClass.consonant) inv.phonemes).length

Instances For

def Data.PHOIBLE.Inventory.vowelCount (inv : Inventory) :

Nat

Number of vowels in an inventory.

Equations

inv.vowelCount = (List.filter (fun (x : Data.PHOIBLE.Phoneme) => x.segmentClass == Data.PHOIBLE.SegmentClass.vowel) inv.phonemes).length

Instances For

def Data.PHOIBLE.Inventory.toneCount (inv : Inventory) :

Nat

Number of distinct tones in an inventory.

Equations

inv.toneCount = (List.filter (fun (x : Data.PHOIBLE.Phoneme) => x.segmentClass == Data.PHOIBLE.SegmentClass.tone) inv.phonemes).length

Instances For