inductive Core.Empirical.Acceptability : Type

Standard acceptability diacritics used in linguistic papers.

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

• ok : Acceptability
• marginal : Acceptability
• degraded : Acceptability
• unacceptable : Acceptability
• anomalous : Acceptability
• variable : Acceptability

instance Core.Empirical.instReprAcceptability : Repr Acceptability

Equations

• Core.Empirical.instReprAcceptability = { reprPrec := Core.Empirical.instReprAcceptability.repr }

def Core.Empirical.instReprAcceptability.repr : Acceptability → Nat → Std.Format

Equations

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

instance Core.Empirical.instDecidableEqAcceptability : DecidableEq Acceptability

Equations

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

instance Core.Empirical.instBEqAcceptability : BEq Acceptability

Equations

• Core.Empirical.instBEqAcceptability = { beq := Core.Empirical.instBEqAcceptability.beq }

def Core.Empirical.instBEqAcceptability.beq : Acceptability → Acceptability → Bool

Equations

• Core.Empirical.instBEqAcceptability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Core.Empirical.ScaleType : Type

Scale type for empirical measures.

• binary : ScaleType
• proportion : ScaleType
• ordinal : ScaleType
• continuous : ScaleType

instance Core.Empirical.instReprScaleType : Repr ScaleType

Equations

• Core.Empirical.instReprScaleType = { reprPrec := Core.Empirical.instReprScaleType.repr }

def Core.Empirical.instReprScaleType.repr : ScaleType → Nat → Std.Format

Equations

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

instance Core.Empirical.instDecidableEqScaleType : DecidableEq ScaleType

Equations

• Core.Empirical.instDecidableEqScaleType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Core.Empirical.TaskType : Type

Task type for data elicitation.

• grammaticalityJudgment : TaskType
• acceptabilityRating : TaskType
• truthValueJudgment : TaskType
• inferenceEndorsement : TaskType
• forcedChoice : TaskType
• production : TaskType
• selfPacedReading : TaskType
• eyeTracking : TaskType
• actOut : TaskType

def Core.Empirical.instReprTaskType.repr : TaskType → Nat → Std.Format

Equations

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

instance Core.Empirical.instReprTaskType : Repr TaskType

Equations

• Core.Empirical.instReprTaskType = { reprPrec := Core.Empirical.instReprTaskType.repr }

instance Core.Empirical.instDecidableEqTaskType : DecidableEq TaskType

Equations

• Core.Empirical.instDecidableEqTaskType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Core.Empirical.MeasureSpec : Type

Combined measure specification

• scale : ScaleType
• task : TaskType
• unit : String

  Unit or scale bounds (e.g., "percentage 0-100", "Likert 1-7", "ms")

instance Core.Empirical.instReprMeasureSpec : Repr MeasureSpec

Equations

• Core.Empirical.instReprMeasureSpec = { reprPrec := Core.Empirical.instReprMeasureSpec.repr }

def Core.Empirical.instReprMeasureSpec.repr : MeasureSpec → Nat → Std.Format

Equations

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

inductive Core.Empirical.ProcessingDimension : Type

Processing dimensions that a task type is sensitive to.

Different experimental paradigms tap different processing dimensions. This links TaskType to the dimensions in ProcessingModel.ProcessingProfile.

• locality : ProcessingDimension
• boundaries : ProcessingDimension
• referentialLoad : ProcessingDimension
• ease : ProcessingDimension

instance Core.Empirical.instReprProcessingDimension : Repr ProcessingDimension

Equations

• Core.Empirical.instReprProcessingDimension = { reprPrec := Core.Empirical.instReprProcessingDimension.repr }

def Core.Empirical.instReprProcessingDimension.repr : ProcessingDimension → Nat → Std.Format

Equations

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

instance Core.Empirical.instDecidableEqProcessingDimension : DecidableEq ProcessingDimension

Equations

• Core.Empirical.instDecidableEqProcessingDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Empirical.taskSensitiveDimensions : TaskType → List ProcessingDimension

Which processing dimensions a task type is sensitive to.

Self-paced reading and eye-tracking are sensitive to locality and boundaries (spillover regions, wrap-up effects). Acceptability ratings aggregate across all dimensions.

Equations

• One or more equations did not get rendered due to their size.
• Core.Empirical.taskSensitiveDimensions Core.Empirical.TaskType.selfPacedReading = [Core.Empirical.ProcessingDimension.locality, Core.Empirical.ProcessingDimension.boundaries]
• Core.Empirical.taskSensitiveDimensions x✝ = []

structure Core.Empirical.ProcessingObservation : Type

An empirical observation linked to processing dimensions.

Connects an observed behavioral measure to the processing profile dimensions it reflects.

• measure : MeasureSpec

  What was measured

• dimensions : List ProcessingDimension

  Which processing dimensions this observation reflects

• description : String

  Description of the observed pattern

def Core.Empirical.instReprProcessingObservation.repr : ProcessingObservation → Nat → Std.Format

Equations

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

instance Core.Empirical.instReprProcessingObservation : Repr ProcessingObservation

Equations

• Core.Empirical.instReprProcessingObservation = { reprPrec := Core.Empirical.instReprProcessingObservation.repr }