Features.Acceptability — Linguistic Acceptability Diacritics

Standard acceptability diacritics used in linguistic papers, encoded as a six-way taxonomy. These correspond to the conventional marks placed before example sentences:

• (unmarked) = fully acceptable
• ? = degraded/marginal
• ?? = quite degraded
• * = clearly unacceptable
• # = semantically/pragmatically anomalous (syntactically well-formed)
• % = dialectally variable / speaker-dependent

The semantic-vs-syntactic split (# vs *) and dialect marker (%) are linguistically substantive distinctions, not just gradient acceptability; this is why the type is a labeled enum rather than a Likert-style ordinal.

Judgment is the ordinal cousin: the Schütze/Sprouse five-level acceptability scale, ordered worst-to-last so that "rated worse than" comparisons come from the derived Ord. It is the judgment type carried by Linglib/Data/Examples/Schema.lean's LinguisticExample and by the minimal-pair vocabulary in Linglib/Features/MinimalPairs.lean. For factorial-design machinery over experimental ratings (difference-in- differences scores etc.), see Linglib/Studies/SprouseEtAl2012.lean.

inductive Features.Acceptability : Type

Standard acceptability diacritics used in linguistic papers.

• ok : Acceptability

  (unmarked) fully acceptable

• marginal : Acceptability

  ? degraded but not out

• degraded : Acceptability

  ?? quite degraded

• unacceptable : Acceptability

  * clearly unacceptable

• anomalous : Acceptability

  # semantically/pragmatically odd

• variable : Acceptability

  % dialectally variable

def Features.instReprAcceptability.repr : Acceptability → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprAcceptability : Repr Acceptability

Equations

• Features.instReprAcceptability = { reprPrec := Features.instReprAcceptability.repr }

@[implicit_reducible]

instance Features.instDecidableEqAcceptability : DecidableEq Acceptability

Equations

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

inductive Features.Judgment : Type

Acceptability / felicity judgment on the Schütze/Sprouse five-level scale. Constructor order encodes "worse" (acceptable is best, ungrammatical worst); the derived Ord makes "this paper rates X worse than Y" comparisons available without an extra wrapper.

Use .acceptable for clean grammatical/felicitous data; reserve .ungrammatical for hard star judgments and .unacceptable for pragmatic/felicity failure short of ungrammaticality.

• acceptable : Judgment
• marginal : Judgment
• questionable : Judgment
• unacceptable : Judgment
• ungrammatical : Judgment

@[implicit_reducible]

instance Features.instDecidableEqJudgment : DecidableEq Judgment

Equations

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

@[implicit_reducible]

instance Features.instBEqJudgment : BEq Judgment

Equations

• Features.instBEqJudgment = { beq := Features.instBEqJudgment.beq }

def Features.instBEqJudgment.beq : Judgment → Judgment → Bool

Equations

• Features.instBEqJudgment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Features.instReprJudgment.repr : Judgment → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Features.instReprJudgment.repr Features.Judgment.marginal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Judgment.marginal")).group prec✝

@[implicit_reducible]

instance Features.instReprJudgment : Repr Judgment

Equations

• Features.instReprJudgment = { reprPrec := Features.instReprJudgment.repr }

@[implicit_reducible]

instance Features.instInhabitedJudgment : Inhabited Judgment

Equations

• Features.instInhabitedJudgment = { default := Features.instInhabitedJudgment.default }

@[implicit_reducible]

instance Features.instOrdJudgment : Ord Judgment

Equations

• Features.instOrdJudgment = { compare := Features.instOrdJudgment.ord }

def Features.instOrdJudgment.ord : Judgment → Judgment → Ordering

Equations

• Features.instOrdJudgment.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx