Judgments

This file defines Judgment, the mark a paper puts before an example, the CLDF 1.3 grammaticalityJudgement of [FCL+24]: unmarked, ?, ??, # or *.

Main definitions

• Judgment: the five marks.
• Judgment.rank: the position of a mark on the scale, and the LinearOrder lifted along it.
• Judgment.ofName?: the judgment a data file names.

Implementation notes

• The marks are ordered by severity, so ≤ reads "at most as acceptable as" and a study writes .marginal ≤ e.judgment for an example the paper accepts with at most one question mark. The order is a modelling convention rather than a scale from the literature. It ranks # above * because an example marked # is well formed but infelicitous; the two constructors keep the difference in kind.
• A split mark a paper prints, such as */?? for speakers who differ, is several marks for one sentence. An example records the first as its judgment and each further mark as an alsoJudged paper feature, and a study reading them all reads Datum.judgments. Gradient ratings are results, recorded in Data/Experiments/.

References

• [FCL+24]

inductive Judgment : Type

The mark a paper puts before an example.

• acceptable : Judgment

  The paper accepts the example and leaves it unmarked.

• marginal : Judgment

  The mark ? calls the example marginal.

• questionable : Judgment

  The mark ?? calls the example questionable.

• unacceptable : Judgment

  The mark # calls the example well formed but infelicitous or semantically anomalous.

• ungrammatical : Judgment

  The mark * calls the example ungrammatical.

@[instance_reducible]

instance instDecidableEqJudgment : DecidableEq Judgment

Equations

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

@[instance_reducible]

instance instReprJudgment : Repr Judgment

Equations

• instReprJudgment = { reprPrec := instReprJudgment.repr }

def instReprJudgment.repr : Judgment → ℕ → Std.Format

Equations

• instReprJudgment.repr Judgment.acceptable prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Judgment.acceptable")).group prec✝
• instReprJudgment.repr Judgment.marginal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Judgment.marginal")).group prec✝
• instReprJudgment.repr Judgment.questionable prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Judgment.questionable")).group prec✝
• instReprJudgment.repr Judgment.unacceptable prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Judgment.unacceptable")).group prec✝
• instReprJudgment.repr Judgment.ungrammatical prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Judgment.ungrammatical")).group prec✝

@[instance_reducible]

instance instInhabitedJudgment : Inhabited Judgment

Equations

• instInhabitedJudgment = { default := instInhabitedJudgment.default }

@[instance_reducible]

instance instFintypeJudgment : Fintype Judgment

Equations

• instFintypeJudgment = { elems := { val := ↑Judgment.enumList, nodup := Judgment.enumList_nodup }, complete := instFintypeJudgment._proof_1 }

def Judgment.rank : Judgment → Fin 5

The position of a mark on the scale, ungrammatical lowest.

Equations

• Judgment.ungrammatical.rank = 0
• Judgment.unacceptable.rank = 1
• Judgment.questionable.rank = 2
• Judgment.marginal.rank = 3
• Judgment.acceptable.rank = 4

@[instance_reducible]

instance instLinearOrderJudgment : LinearOrder Judgment

Equations

• instLinearOrderJudgment = LinearOrder.lift' Judgment.rank instLinearOrderJudgment._proof_1

def Judgment.ofName? : String → Option Judgment

Judgment.ofName? s is the judgment the data files write as s.

Equations

• Judgment.ofName? "acceptable" = some Judgment.acceptable
• Judgment.ofName? "marginal" = some Judgment.marginal
• Judgment.ofName? "questionable" = some Judgment.questionable
• Judgment.ofName? "unacceptable" = some Judgment.unacceptable
• Judgment.ofName? "ungrammatical" = some Judgment.ungrammatical
• Judgment.ofName? x✝ = none