Reading example data

This file defines the lookups a study makes on the rows of Data/Examples/, the Datums of Data/Examples/Schema.lean, and the statements it makes by fitting a prediction to them. A reader Datum → Option α reads a value off a row; a fit compares a prediction about that value with the row's judgment, through the three bands of the severity order of judgments, or with its truth-value verdict, and a check bundles the fit over a cluster of rows with the number of rows the reader reads, so that the fit cannot go silently vacuous.

Main definitions

• Datum.feature?, Datum.features: the first value and every value of a key of paperFeatures.
• Datum.parse?, Datum.parseAll?: the first value and every value of a key read through a table.
• Datum.byLanguage: the entry of a table under a row's language, keyed by the Glottocode constants of Data/Examples/Languages.lean.
• Datum.digits?, Datum.nat?, Datum.int?, Datum.decimal?: numerals.
• Datum.bool?: a truth value written true or false.
• Datum.judgments, Datum.JudgedFelicitous: every printed mark, and felicity as the mark and the prose give it.
• Judgment.Band, Judgment.band: the three bands of the severity order that a prediction targets.
• Datum.Fits, Datum.ReadCount: a prediction's fit with the judgment band of what a reader reads off a row, and the count of rows a reader reads, the coverage witness beside a fit.
• Datum.FitsVerdict: a prediction's fit with the truth-value judgment of a row whose task is truth in the context.
• Datum.Checks, Datum.ChecksVerdict: the statement a study makes, a fit over the rows bundled with its coverage count.

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

• A feature is either a stimulus column, naming in the paper's own taxonomy the items, construction or condition the example instantiates, or a claim column, recording what the paper says the judgment shows. Only stimulus columns may feed a prediction (Datum.Fits): predicting a judgment from the paper's claim about that judgment checks nothing. A claim column is read as a target, checking that the formal account derives what the paper asserts, or stands as documentation; prose commentary belongs in comment. A stimulus value is a key into a finite taxonomy, so a parse? table can read it. A truth-value judgment in a context is the verdict field, never a feature: the response of a truth task is a field of the datum, like the mark of an acceptability task, which on such a row records only well-formedness.
• A datum answers a question put about the expression, and each question has its own response channel. Is it acceptable? — the mark in judgment, fitted through Judgment.band. Is it true in this context? — verdict, fitted through FitsVerdict. Can it mean this? — that reading's entry in readings. Is this variant acceptable in the same frame? — its entry in alternatives. Is it felicitous, though well formed? — the felicity feature that JudgedFelicitous reads. A study fits its prediction against the channel whose question the paper asked. Implication judgments, whether an utterance conveys an inference, and relational judgments, whether two sentences are equivalent or contradictory, have no channel yet and sit in claim columns.
• 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.

inductive Judgment.Band : Type

The three bands of the severity order that a prediction targets: the unmarked judgment, the middle marks ? and %, on which speakers or grammars divide, and the rejected marks ??, # and *. Which mark a paper prints within a band is its editorial choice, not a prediction.

• accepted : Band
• divided : Band
• rejected : Band

@[instance_reducible]

instance Judgment.instDecidableEqBand : DecidableEq Band

Equations

• Judgment.instDecidableEqBand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Judgment.instReprBand.repr : Band → ℕ → Std.Format

Equations

• Judgment.instReprBand.repr Judgment.Band.accepted prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Judgment.Band.accepted")).group prec✝
• Judgment.instReprBand.repr Judgment.Band.divided prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Judgment.Band.divided")).group prec✝
• Judgment.instReprBand.repr Judgment.Band.rejected prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Judgment.Band.rejected")).group prec✝

@[instance_reducible]

instance Judgment.instReprBand : Repr Band

Equations

• Judgment.instReprBand = { reprPrec := Judgment.instReprBand.repr }

def Judgment.band : Judgment → Band

The band of a mark.

Equations

• Judgment.acceptable.band = Judgment.Band.accepted
• Judgment.marginal.band = Judgment.Band.divided
• Judgment.variable.band = Judgment.Band.divided
• Judgment.questionable.band = Judgment.Band.rejected
• Judgment.unacceptable.band = Judgment.Band.rejected
• Judgment.ungrammatical.band = Judgment.Band.rejected

def Judgment.Band.ofProp (p : Prop) [Decidable p] : Band

The band of a two-way prediction: accepted where p holds and rejected where it fails.

Equations

• Judgment.Band.ofProp p = if p then Judgment.Band.accepted else Judgment.Band.rejected

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.parseAll? (e : Datum) (key : String) {α : Type u_1} (table : List (String × α)) : Option (List α)

e.parseAll? key table is every value of key in e read through table, if table lists them all.

Equations

• e.parseAll? key table = List.mapM (fun (x : String) => List.lookup x table) (e.features key)

def Datum.byLanguage (e : Datum) {α : Type u_1} (table : List (Glottocode × α)) : Option α

e.byLanguage table is the entry of table under the language of e, if table lists it: how a study reads a row through the languages of its sample.

Equations

• e.byLanguage table = List.lookup e.language 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.bool? (e : Datum) (key : String) : Option Bool

e.bool? key is the first value of key in e read as true or false.

Equations

• e.bool? key = e.parse? key [("true", true), ("false", false)]

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 := ⋯ }

def Datum.Fits (e : Datum) {α : Type u_1} (f : Datum → Option α) (P : α → Judgment.Band) : Prop

The prediction P over what the reader f reads off e fits the row: the band of e's judgment is the predicted band. A row the reader does not read is unconstrained, so a Fits theorem is paired with a Datum.ReadCount for its reader.

Equations

• e.Fits f P = ∀ a ∈ f e, e.judgment.band = P a

@[instance_reducible]

instance Datum.instDecidableFits (e : Datum) {α : Type u_1} (f : Datum → Option α) (P : α → Judgment.Band) : Decidable (e.Fits f P)

Equations

• e.instDecidableFits f P = Datum.instDecidableFits._aux_1 e f P

def Datum.FitsVerdict (e : Datum) {α : Type u_1} (f : Datum → Option α) (P : α → Bool) : Prop

The prediction P over what the reader f reads off e fits the row's truth-value judgment: where the source reports a verdict, it is the predicted one. The judgment of such a row records only that the expression is well formed, so a truth-value row is read by FitsVerdict, not Fits.

Equations

• e.FitsVerdict f P = ∀ a ∈ f e, ∀ b ∈ e.verdict, b = P a

@[instance_reducible]

instance Datum.instDecidableFitsVerdict (e : Datum) {α : Type u_1} (f : Datum → Option α) (P : α → Bool) : Decidable (e.FitsVerdict f P)

Equations

• e.instDecidableFitsVerdict f P = Datum.instDecidableFitsVerdict._aux_1 e f P

def Datum.ReadCount {α : Type u_1} (f : Datum → Option α) (rows : List Datum) (n : ℕ) : Prop

The reader f reads exactly n of rows: the coverage witness beside a Fits or other row-quantified theorem, without which the theorem goes silently vacuous when a feature key or a table value drifts.

Equations

• Datum.ReadCount f rows n = ((List.filterMap f rows).length = n)

@[instance_reducible]

instance Datum.instDecidableReadCount {α : Type u_1} (f : Datum → Option α) (rows : List Datum) (n : ℕ) : Decidable (ReadCount f rows n)

Equations

• Datum.instDecidableReadCount f rows n = { decide := (List.filterMap f rows).length.beq n, reflects_decide := ⋯ }

def Datum.Checks {α : Type u_1} (f : Datum → Option α) (P : α → Judgment.Band) (rows : List Datum) (n : ℕ) : Prop

The prediction P fits every row of rows the reader f reads, and f reads exactly n of them: the one statement a study makes about a cluster of rows.

Equations

• Datum.Checks f P rows n = ((∀ e ∈ rows, e.Fits f P) ∧ Datum.ReadCount f rows n)

@[instance_reducible]

instance Datum.instDecidableChecks {α : Type u_1} (f : Datum → Option α) (P : α → Judgment.Band) (rows : List Datum) (n : ℕ) : Decidable (Checks f P rows n)

Equations

• Datum.instDecidableChecks f P rows n = { decide := decide (∀ e ∈ rows, e.Fits f P) && decide (Datum.ReadCount f rows n), reflects_decide := ⋯ }

def Datum.ChecksVerdict {α : Type u_1} (f : Datum → Option α) (P : α → Bool) (rows : List Datum) (n : ℕ) : Prop

The truth-value counterpart of Datum.Checks: the prediction matches every reported verdict on a row the reader reads, and exactly n rows have both.

Equations

• Datum.ChecksVerdict f P rows n = ((∀ e ∈ rows, e.FitsVerdict f P) ∧ (List.filter (fun (e : Datum) => decide ((f e).isSome = true ∧ e.verdict.isSome = true)) rows).length = n)

@[instance_reducible]

instance Datum.instDecidableChecksVerdict {α : Type u_1} (f : Datum → Option α) (P : α → Bool) (rows : List Datum) (n : ℕ) : Decidable (ChecksVerdict f P rows n)

Equations

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

@[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