Word forms

This file defines the rows of a paper's word-level data: the lexemes, the form of a lexeme in a cell, the relations, paradigms and root classes a source asserts over forms. The rows follow the Wordlist module of the Cross-Linguistic Data Formats and the Paralex standard for lexicons of inflected forms, which shares its column names. It is the morphological counterpart of Data/Examples/: the datum is a word and its parts rather than an utterance and its gloss.

Main definitions

• CLDF.Wordlist.Lexeme: a row of the LexemeTable, a word of a language by the concept it expresses.
• CLDF.Wordlist.Form: a row of the FormTable, the form of a lexeme in a cell, with the source's segmentation and its judgment of the form.
• CLDF.Wordlist.FormRelation: a row of the FormRelationTable, a relation a source asserts from one form to another.
• CLDF.Wordlist.Paradigm: a row of the ParadigmTable, the forms a source gives a lexeme as one column of its table.
• CLDF.Wordlist.RootClasses: a row of the RootClassTable, a source's judgment that the cells of a paradigm divide into classes sharing a root.

Implementation notes

• Per-paper data lives in Linglib/Data/Wordlist/{AuthorYear}.json and is compiled by scripts/gen_wordlist.py into {AuthorYear}.lean, declaring namespace {AuthorYear}.Forms: a Cell type, the lexemes, forms, relations, paradigms and root classes, the lists all of the forms the sources accept and marked of the others, and an Analysis table.
• A cell is a bundle of features. Universal Dependencies features are typed by UD.MorphFeatures; a dataset whose cells need features UD lacks extends it with generated enumerations, so Form is parametric in its cell type and Form.map changes it.
• A form carries the source's judgment of it in its cell, CLDF's grammaticalityJudgement: a form a source rejects is a row of its own, so disagreeing sources sit side by side.
• segments is the source's tokenization of the form into sound segments, at the source's granularity; morphs is the morph segmentation the source prints, ø marking a null exponent.
• Root identity is a judgment rather than a function of the forms: better and best share a root that no identity of strings shows, so a source's classes are rows of their own.
• What a paper's theory assigns to a form, such as an underlying representation, a root or a class, is that paper's parse and goes to the generated Analysis table, never to the form. The generator resolves every reference to an analysis, as it resolves every reference to a form: each form x has its analysis x.analysis, and a dataset with relations and analyses has its relations over the analyses too, so no study joins rows by identifier.
• Comments, the ParameterTable and the cognates a source lists are its record: the generator validates them and does not emit them.

TODO

• Cite the paper that introduces the Paralex standard (Beniamine and colleagues, 2023) once its bibliographic record is verified.

References

• [FLG+18]
• [FCL+24]

structure CLDF.Wordlist.Lexeme : Type

A Lexeme is a row of the LexemeTable, a word of a language, by the concept it expresses and its citation form.

• id : String

  The ID column holds a stable identifier keyed to the paper.

• languageId : Glottocode

  The Language_ID column holds the Glottocode of the language.

• variety : String

  The Variety column names the variety, where the source distinguishes varieties of one Glottolog languoid.

• parameterId : String

  The Parameter_ID column names the concept the lexeme expresses.

• label : String

  The Name column holds the citation form, where the source gives one.

• pos : Flat UD.UPOS

  The POS column holds the part of speech, where the source gives one.

@[instance_reducible]

instance CLDF.Wordlist.instDecidableEqLexeme : DecidableEq Lexeme

Equations

• CLDF.Wordlist.instDecidableEqLexeme = CLDF.Wordlist.instDecidableEqLexeme.decEq

def CLDF.Wordlist.instDecidableEqLexeme.decEq (x✝ x✝¹ : Lexeme) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance CLDF.Wordlist.instReprLexeme : Repr Lexeme

Equations

• CLDF.Wordlist.instReprLexeme = { reprPrec := CLDF.Wordlist.instReprLexeme.repr }

def CLDF.Wordlist.instReprLexeme.repr : Lexeme → ℕ → Std.Format

Equations

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

structure CLDF.Wordlist.Form (C : Type u_1) : Type u_1

A Form C is a row of the FormTable, the form of a lexeme in a cell of type C, with the source's segmentation and its judgment of the form.

• id : String

  The ID column holds a stable identifier keyed to the paper.

• lexeme : Lexeme

  The lexeme the Lexeme_ID column names.

• cell : C

  The cell the Cell column names.

• form : String

  The Form column holds the written form.

• segments : List String

  The Segments column holds the form's sound segments.

• morphs : List String

  The Morphs column holds the form's morphs as the source segments it.

• judgment : Judgment

  The Judgment column holds the source's mark on the form in its cell.

• source : List SourceRef

  The Source column holds the references, each a bibkey with a locator.

@[instance_reducible]

instance CLDF.Wordlist.instDecidableEqForm {C✝ : Type u_1} [DecidableEq C✝] : DecidableEq (Form C✝)

Equations

• CLDF.Wordlist.instDecidableEqForm = CLDF.Wordlist.instDecidableEqForm.decEq

def CLDF.Wordlist.instDecidableEqForm.decEq {C✝ : Type u_1} [DecidableEq C✝] (x✝ x✝¹ : Form C✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance CLDF.Wordlist.instReprForm {C✝ : Type u_1} [Repr C✝] : Repr (Form C✝)

Equations

• CLDF.Wordlist.instReprForm = { reprPrec := CLDF.Wordlist.instReprForm.repr }

def CLDF.Wordlist.instReprForm.repr {C✝ : Type u_1} [Repr C✝] : Form C✝ → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev CLDF.Wordlist.Form.languageId {C : Type u_1} (f : Form C) : Glottocode

The Glottocode of the form's language.

Equations

• f.languageId = f.lexeme.languageId

@[reducible, inline]

abbrev CLDF.Wordlist.Form.parameterId {C : Type u_1} (f : Form C) : String

The concept the form expresses.

Equations

• f.parameterId = f.lexeme.parameterId

def CLDF.Wordlist.Form.map {C : Type u_1} {D : Type u_2} (g : C → D) (f : Form C) : Form D

f.map g is f with its cell read through g.

Equations

• CLDF.Wordlist.Form.map g f = { id := f.id, lexeme := f.lexeme, cell := g f.cell, form := f.form, segments := f.segments, morphs := f.morphs, judgment := f.judgment, source := f.source }

@[simp]

theorem CLDF.Wordlist.Form.map_id {C : Type u_1} (f : Form C) : map _root_.id f = f

@[simp]

theorem CLDF.Wordlist.Form.map_map {C : Type u_1} {D : Type u_2} {E : Type u_3} (g : C → D) (h : D → E) (f : Form C) : map h (map g f) = map (h ∘ g) f

def CLDF.Wordlist.Form.slots {C : Type u_1} (f : Form C) (i : Fin f.segments.length) : Flat String

f.slots reads the segments of f as a slot-indexed item on the flat carrier, the shape the schemas of Morphology/ConstructionMorphology/ match.

Equations

• f.slots i = ↑f.segments[i]

def CLDF.Wordlist.Form.morphSlots {C : Type u_1} (f : Form C) (i : Fin f.morphs.length) : Flat String

f.morphSlots reads the morphs of f as a slot-indexed item on the flat carrier, one morph per slot.

Equations

• f.morphSlots i = ↑f.morphs[i]

structure CLDF.Wordlist.FormRelation (α : Type u_1) : Type u_1

A FormRelation α is a row of the FormRelationTable, a relation that a source asserts from one form to another, named by its term for it, with each form given as an α: the form itself, or its analysis.

• id : String

  The ID column holds the relation's identifier.

• form : α

  The form that the Form_ID column names.

• target : α

  The form that the Target_ID column names.

• relation : String

  The Relation column holds the source's name for the relation.

• source : List SourceRef

  The Source column holds the references, each a bibkey with a locator.

def CLDF.Wordlist.instDecidableEqFormRelation.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : FormRelation α✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance CLDF.Wordlist.instDecidableEqFormRelation {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (FormRelation α✝)

Equations

• CLDF.Wordlist.instDecidableEqFormRelation = CLDF.Wordlist.instDecidableEqFormRelation.decEq

def CLDF.Wordlist.instReprFormRelation.repr {α✝ : Type u_1} [Repr α✝] : FormRelation α✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CLDF.Wordlist.instReprFormRelation {α✝ : Type u_1} [Repr α✝] : Repr (FormRelation α✝)

Equations

• CLDF.Wordlist.instReprFormRelation = { reprPrec := CLDF.Wordlist.instReprFormRelation.repr }

structure CLDF.Wordlist.Paradigm (C : Type u_1) : Type u_1

A Paradigm C is a row of the ParadigmTable, the forms a source gives a lexeme as one column of its table, at most one to a cell.

• id : String

  The ID column holds a stable identifier keyed to the paper.

• lexeme : Lexeme

  The lexeme whose forms these are.

• forms : List (Form C)

  The forms that the Form_IDs column names.

• source : List SourceRef

  The Source column holds the references, each a bibkey with a locator.

def CLDF.Wordlist.instDecidableEqParadigm.decEq {C✝ : Type u_1} [DecidableEq C✝] (x✝ x✝¹ : Paradigm C✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance CLDF.Wordlist.instDecidableEqParadigm {C✝ : Type u_1} [DecidableEq C✝] : DecidableEq (Paradigm C✝)

Equations

• CLDF.Wordlist.instDecidableEqParadigm = CLDF.Wordlist.instDecidableEqParadigm.decEq

@[instance_reducible]

instance CLDF.Wordlist.instReprParadigm {C✝ : Type u_1} [Repr C✝] : Repr (Paradigm C✝)

Equations

• CLDF.Wordlist.instReprParadigm = { reprPrec := CLDF.Wordlist.instReprParadigm.repr }

def CLDF.Wordlist.instReprParadigm.repr {C✝ : Type u_1} [Repr C✝] : Paradigm C✝ → ℕ → Std.Format

Equations

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

structure CLDF.Wordlist.RootClasses (C : Type u_1) extends CLDF.Wordlist.Paradigm C : Type u_1

A RootClasses C is a row of the RootClassTable, a source's judgment that the cells of a paradigm divide into classes of cells whose forms share a root, each cell with the index of its class.

• id : String
• lexeme : Lexeme
• forms : List (Form C)
• source : List SourceRef
• classes : List (C × ℕ)

  The class of each cell, A as 0, B as 1, and so on.

def CLDF.Wordlist.instDecidableEqRootClasses.decEq {C✝ : Type u_1} [DecidableEq C✝] (x✝ x✝¹ : RootClasses C✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance CLDF.Wordlist.instDecidableEqRootClasses {C✝ : Type u_1} [DecidableEq C✝] : DecidableEq (RootClasses C✝)

Equations

• CLDF.Wordlist.instDecidableEqRootClasses = CLDF.Wordlist.instDecidableEqRootClasses.decEq

def CLDF.Wordlist.instReprRootClasses.repr {C✝ : Type u_1} [Repr C✝] : RootClasses C✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CLDF.Wordlist.instReprRootClasses {C✝ : Type u_1} [Repr C✝] : Repr (RootClasses C✝)

Equations

• CLDF.Wordlist.instReprRootClasses = { reprPrec := CLDF.Wordlist.instReprRootClasses.repr }

def CLDF.Wordlist.RootClasses.classOf {C : Type u_1} [DecidableEq C] (r : RootClasses C) (c : C) : Option ℕ

r.classOf c is the class of the cell c in the judgment r, if r classes c.

Equations

• r.classOf c = List.lookup c r.classes