Evaluating accounts against data

This library evaluates the accounts that linglib formalizes against the data it records. An account's verdict on an observation is right, wrong, or silent when the account predicts nothing about it or nothing was observed (Eval.Verdict). A verdict is always derived from the account's own definitions and the recorded data, and the comparison it makes is fixed by the type of the prediction, never by a label attached to an account or a datum.

An experiment is scored cell by cell (Eval.Experiment): it records the outcome observed in each cell of its design, and its linking hypothesis says what outcome a theory predicts there. The verdict on a theory in a cell compares the two (Experiment.verdict). Whatever a theory brings to the comparison, such as how it parses the experiment's sentences, is part of what is scored, so that the cells are the facts alone.

The library is linglib's part of the Co-Linguistics project of Chemla, Spector, Kalomoiros and Schlenker, which compares formalized theories against data.

References

• [CSKS26]

inductive Eval.Verdict : Type

An account's verdict on an observation.

• correct : Verdict

  The prediction matches the observation.

• wrong : Verdict

  The prediction differs from the observation.

• silent : Verdict

  The account predicts nothing, or nothing was observed.

@[instance_reducible]

instance Eval.instDecidableEqVerdict : DecidableEq Verdict

Equations

• Eval.instDecidableEqVerdict x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Eval.instReprVerdict : Repr Verdict

Equations

• Eval.instReprVerdict = { reprPrec := Eval.instReprVerdict.repr }

def Eval.instReprVerdict.repr : Verdict → Nat → Std.Format

Equations

• Eval.instReprVerdict.repr Eval.Verdict.correct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Eval.Verdict.correct")).group prec✝
• Eval.instReprVerdict.repr Eval.Verdict.wrong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Eval.Verdict.wrong")).group prec✝
• Eval.instReprVerdict.repr Eval.Verdict.silent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Eval.Verdict.silent")).group prec✝

def Eval.Verdict.of {α : Type u_1} [DecidableEq α] : Option α → Option α → Verdict

The verdict of a prediction on an observation of the same type.

Equations

• Eval.Verdict.of (some p) (some o) = if p = o then Eval.Verdict.correct else Eval.Verdict.wrong
• Eval.Verdict.of x✝¹ x✝ = Eval.Verdict.silent

structure Eval.Experiment (Θ : Type u_1) (C : Type u_2) (O : Type u_3) : Type (max (max u_1 u_2) u_3)

An experiment scoring theories Θ, with cells C and outcomes O: the outcome observed in each cell, and the outcome its linking hypothesis has a theory predict there.

• observed : C → Option O

  The outcome observed in a cell, if the cell was run.

• predicted : Θ → C → Option O

  The outcome a theory predicts in a cell by the linking hypothesis, if it predicts one.

def Eval.Experiment.verdict {Θ : Type u_1} {C : Type u_2} {O : Type u_3} [DecidableEq O] (X : Experiment Θ C O) (T : Θ) (c : C) : Verdict

The verdict on a theory in a cell of an experiment.

Equations

• X.verdict T c = Eval.Verdict.of (X.predicted T c) (X.observed c)