Felicity Types

@cite{fox-hackl-2006} @cite{katzir-singh-2015} @cite{magri-2009} @cite{spector-2014}

Theory-neutral data types for felicity/oddness predictions.

inductive Interfaces.FelicityStatus : Type

Felicity status for an utterance in context.

• felicitous : FelicityStatus

  The utterance is felicitous (no oddness).

• odd : FelicityStatus

  The utterance is odd (# marks in linguistics).

• borderline : FelicityStatus

  Borderline: some conditions met, others not.

instance Interfaces.instDecidableEqFelicityStatus : DecidableEq FelicityStatus

Equations

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

instance Interfaces.instBEqFelicityStatus : BEq FelicityStatus

Equations

• Interfaces.instBEqFelicityStatus = { beq := Interfaces.instBEqFelicityStatus.beq }

def Interfaces.instBEqFelicityStatus.beq : FelicityStatus → FelicityStatus → Bool

Equations

• Interfaces.instBEqFelicityStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Interfaces.instReprFelicityStatus.repr : FelicityStatus → Nat → Std.Format

Equations

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

instance Interfaces.instReprFelicityStatus : Repr FelicityStatus

Equations

• Interfaces.instReprFelicityStatus = { reprPrec := Interfaces.instReprFelicityStatus.repr }

inductive Interfaces.OddnessSource : Type

Source of oddness (which condition was violated).

• questionCondition : OddnessSource

  Question Condition: QUD trivially settled by CK.

• answerCondition : OddnessSource

  Answer Condition: needlessly inferior alternative exists.

• both : OddnessSource

  Both conditions violated.

• blindMismatch : OddnessSource

  Blind Mismatch: strengthened meaning contradicts common knowledge (@cite{magri-2009} Mismatch Hypothesis, §3.2.2).

• blindPresupMismatch : OddnessSource

  Blind Presuppositional Mismatch: strengthened presupposition contradicts common knowledge (@cite{magri-2009} MH_prs, §3.4).

• unspecified : OddnessSource

  Theory doesn't distinguish sources.

instance Interfaces.instDecidableEqOddnessSource : DecidableEq OddnessSource

Equations

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

def Interfaces.instBEqOddnessSource.beq : OddnessSource → OddnessSource → Bool

Equations

• Interfaces.instBEqOddnessSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Interfaces.instBEqOddnessSource : BEq OddnessSource

Equations

• Interfaces.instBEqOddnessSource = { beq := Interfaces.instBEqOddnessSource.beq }

def Interfaces.instReprOddnessSource.repr : OddnessSource → Nat → Std.Format

Equations

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

instance Interfaces.instReprOddnessSource : Repr OddnessSource

Equations

• Interfaces.instReprOddnessSource = { reprPrec := Interfaces.instReprOddnessSource.repr }

structure Interfaces.FelicityResult : Type

Result of a felicity check: status + optional source information.

• status : FelicityStatus
• source : Option OddnessSource

def Interfaces.instReprFelicityResult.repr : FelicityResult → Nat → Std.Format

Equations

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

instance Interfaces.instReprFelicityResult : Repr FelicityResult

Equations

• Interfaces.instReprFelicityResult = { reprPrec := Interfaces.instReprFelicityResult.repr }