Data from examples

This file defines the data a study reads off a paper's examples, and the lookups it makes on them. An example is what the paper prints under a number; a Datum is one piece of data the paper reports with it in the sense of Tonhauser and Matthewson: an expression (the example, or one alternant of it), the context it is judged in, and the judgment, less the information about the speakers that papers seldom give. A datum is a row of the Examples component of the Cross-Linguistic Data Formats of Forkel et al., in version 1.3, and the sentence-level counterpart of Data/Forms/.

Main definitions

• Datum: a piece of data about an example, with the judgment layer (judgment, alternatives, readings) and the paper's own columns (paperFeatures).
• SourceRef: a reference to a paper, a bibkey with a locator.
• Datum.feature?, Datum.features: the first value and every value of a key of paperFeatures.
• Datum.parse?: the first value of a key read through a table.
• Datum.digits?, Datum.nat?, Datum.int?: numerals.
• Datum.judgments, Datum.JudgedFelicitous: every printed mark, and felicity as the mark and the prose give it.

Main statements

• mem_features, features_eq_nil, head?_features, feature?_eq_none: the lookups in terms of membership in paperFeatures, in the shape of List.mem_lookupAll, List.lookupAll_eq_nil, List.head?_lookupAll and List.dlookup_eq_none.

Implementation notes

• Per-paper data lives in Linglib/Data/Examples/{AuthorYear}.json and is compiled by scripts/gen_examples.py into Linglib/Data/Examples/{AuthorYear}.lean, declaring namespace {AuthorYear}.Examples. The JSON keys are the field names, and id uses only the characters of a CLDF identifier. scripts/export_examples_cldf.py writes the data as a CLDF dataset, which CI validates.
• Four JSON keys are the source's record and not fields, since no theorem reads them and every field is paid for when a kernel decide reduces a row: translation (Translated_Text, empty for an English example), discourseSegments (the utterances of a discourse), comment, and verified (how the row was last checked against its source). The generator validates them and the CLDF export carries them.
• language is a Glottocode, which the generator checks against languages.csv, the language table of the data drawn from Glottolog; it is empty for a constructed string that belongs to no language, such as a pattern of a formal language.
• glossedTokens pairs each analysed word with its gloss, so the word-by-word alignment of Rule 1 of the Leipzig Glossing Rules holds by construction. CLDF's LGR_Conformance column is not stored: whether a gloss also aligns morpheme by morpheme (Rule 2) is a property of the pairs.
• Translations are into English, the default of CLDF's Meta_Language_ID, which is therefore not stored.
• A discourse is one datum: primaryText joins its utterances with single spaces, and the judgment is of the last utterance in the context of the others.
• paperFeatures are the paper's own columns: what the paper states about the datum, such as the cell of its design or the class it assigns. The results a paper prints for an experiment belong in Data/Experiments/, and an analysis the formaliser derives belongs in the study. A key repeats when the expression bears the property twice (two indefinite series in one clause), so the list is not a map: feature? reads the first value, features every value.
• Studies decide propositions over rows, so every lookup reduces in the kernel. digits? reads a numeral by a fold over its characters because String.toNat? is well-founded recursive and does not.
• The file imports no tactic library: every module with example data imports it, and names such a library brings into scope (mathlib's root Tree) would reach every study that reads rows.

TODO

• 86 rows in 21 papers with discourseSegments do not have their concatenation as primaryText (the discourse column of scripts/export_examples_cldf.py --report).

References

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

@[reducible, inline]

abbrev Glottocode : Type

A Glottolog language identifier, such as "stan1293" for Standard English.

Equations

• Glottocode = String

structure SourceRef : Type

A SourceRef is a CLDF source reference bibkey[locator] with its two parts kept apart.

• bibkey : String

  The key of the paper's entry in references.bib.

• paperLabel : String

  The locator in the paper: its example number, table or page.

def instDecidableEqSourceRef.decEq (x✝ x✝¹ : SourceRef) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqSourceRef.decEq { bibkey := a, paperLabel := a_1 } { bibkey := b, paperLabel := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqSourceRef : DecidableEq SourceRef

Equations

• instDecidableEqSourceRef = instDecidableEqSourceRef.decEq

def instReprSourceRef.repr : SourceRef → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprSourceRef : Repr SourceRef

Equations

• instReprSourceRef = { reprPrec := instReprSourceRef.repr }

structure Datum : Type

A Datum is a piece of data a paper reports with one of its examples [TM16]: an expression of a language with its gloss, the context it is judged in, the judgment, the forms and readings the paper judges with it, and the paper's own classifications of it. It is the part of a row of a CLDF ExampleTable that theorems read.

• id : String

  The ID column holds a stable identifier keyed to the paper, {authoryear}_{label}.

• source : SourceRef

  The paper that introduced the example.

• reportedIn : Option SourceRef

  The paper whose data file holds the row, when it only reports an example from source.

• language : Glottocode

  The Language_ID column holds the Glottocode of the language of the expression; empty for a constructed string of no language.

• primaryText : String

  The Primary_Text column holds the expression without judgment marks.

• glossedTokens : List (String × String)

  The Analyzed_Word and Gloss columns paired, each word with its gloss; empty when the source gives no gloss.

• context : String

  The scenario the source gives for the judgment; empty when it gives none.

• judgment : Judgment

  The judgment the source reports for the expression in the context.

• alternatives : List (String × Judgment)

  The other forms the source judges in the same frame, each a whole sentence, with their judgments.

• readings : List (String × Judgment)

  The readings the source distinguishes for the expression, each with its judgment.

• paperFeatures : List (String × String)

  The paper's own columns, as key-value pairs.

def instDecidableEqDatum.decEq (x✝ x✝¹ : Datum) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqDatum : DecidableEq Datum

Equations

• instDecidableEqDatum = instDecidableEqDatum.decEq

@[instance_reducible]

instance instReprDatum : Repr Datum

Equations

• instReprDatum = { reprPrec := instReprDatum.repr }

def instReprDatum.repr : Datum → ℕ → Std.Format

Equations

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

def Datum.digits? (cs : List Char) : Option ℕ

digits? cs is the number that the nonempty string of decimal digits cs denotes.

Equations

• Datum.digits? cs = if cs ≠ [] ∧ cs.all Char.isDigit = true then some (List.foldl (fun (n : ℕ) (c : Char) => 10 * n + (c.toNat - '0'.toNat)) 0 cs) else none

def Datum.surfaceTokens (e : Datum) : List String

e.surfaceTokens is the Analyzed_Word column, the words of e.glossedTokens.

Equations

• e.surfaceTokens = List.map Prod.fst e.glossedTokens

def Datum.glossLine (e : Datum) : List String

e.glossLine is the Gloss column, the glosses of e.glossedTokens.

Equations

• e.glossLine = List.map Prod.snd e.glossedTokens

def Datum.feature? (e : Datum) (key : String) : Option String

e.feature? key is the first value of key in e.paperFeatures, if there is one.

Equations

• e.feature? key = List.lookup key e.paperFeatures

def Datum.features (e : Datum) (key : String) : List String

e.features key is the list of values of key in e.paperFeatures, in order.

Equations

• e.features key = List.filterMap (fun (kv : String × String) => if kv.1 = key then some kv.2 else none) e.paperFeatures

def Datum.parse? (e : Datum) (key : String) {α : Type u_1} (table : List (String × α)) : Option α

e.parse? key table is the entry of table under the first value of key in e, if e has the key and table lists its value.

Equations

• e.parse? key table = (e.feature? key).bind fun (x : String) => List.lookup x table

def Datum.nat? (e : Datum) (key : String) : Option ℕ

e.nat? key is the first value of key in e read as a decimal numeral.

Equations

• e.nat? key = (e.feature? key).bind fun (s : String) => Datum.digits? s.toList

def Datum.int? (e : Datum) (key : String) : Option ℤ

e.int? key is the first value of key in e read as a decimal integer, an optional - followed by digits.

Equations

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

def Datum.decimal? (e : Datum) (key : String) : Option Rat

e.decimal? key is the first value of key in e read as an unsigned decimal numeral, digits with an optional fractional part after a point.

Equations

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

def Datum.judgments (e : Datum) : List Judgment

e.judgments is every mark the paper prints on e: its judgment, then the further marks of a split mark such as ??/*, recorded as alsoJudged.

Equations

• e.judgments = e.judgment :: List.filterMap Judgment.ofName? (e.features "alsoJudged")

def Datum.JudgedFelicitous (e : Datum) : Prop

The paper judges e felicitous: it prints no mark on e, and its prose does not call e infelicitous, which the row records as felicity: infelicitous.

Equations

• e.JudgedFelicitous = (e.judgment = Judgment.acceptable ∧ e.feature? "felicity" ≠ some "infelicitous")

@[instance_reducible]

instance Datum.instDecidableJudgedFelicitous (e : Datum) : Decidable e.JudgedFelicitous

Equations

• e.instDecidableJudgedFelicitous = { decide := decide (e.judgment = Judgment.acceptable) && decide (e.feature? "felicity" ≠ some "infelicitous"), reflects_decide := ⋯ }

@[simp]

theorem Datum.mem_features {e : Datum} {key v : String} : v ∈ e.features key ↔ (key, v) ∈ e.paperFeatures

theorem Datum.features_eq_nil {e : Datum} {key : String} : e.features key = [] ↔ ∀ (v : String), (key, v) ∉ e.paperFeatures

@[simp]

theorem Datum.head?_features {e : Datum} {key : String} : (e.features key).head? = e.feature? key

theorem Datum.feature?_eq_none {e : Datum} {key : String} : e.feature? key = none ↔ ∀ (v : String), (key, v) ∉ e.paperFeatures