Felicity Condition

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

Abstract interface for felicity/oddness predictions, following the ImplicatureTheory pattern. Provides a unified type for comparing @cite{katzir-singh-2015}, @cite{magri-2009}, @cite{spector-2014}, @cite{fox-hackl-2006}, and future felicity theories.

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 ⋯

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

Equations

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

instance Interfaces.instBEqFelicityStatus : BEq FelicityStatus

Equations

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

instance Interfaces.instReprFelicityStatus : Repr FelicityStatus

Equations

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

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

Equations

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

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.

• 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 ⋯

instance Interfaces.instBEqOddnessSource : BEq OddnessSource

Equations

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

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

Equations

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

instance Interfaces.instReprOddnessSource : Repr OddnessSource

Equations

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

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

Equations

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

structure Interfaces.FelicityResult : Type

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

• status : FelicityStatus
• source : Option OddnessSource

instance Interfaces.instReprFelicityResult : Repr FelicityResult

Equations

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

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

Equations

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

class Interfaces.FelicityCondition (T : Type u_1) : Type u_1

A theory that makes predictions about utterance felicity/oddness.

• name : String

  Name of the theory.

• check : T → FelicityResult

  Check whether an input is felicitous, odd, or borderline.

def Interfaces.isFelicitous {T : Type u_1} [FelicityCondition T] (t : T) : Bool

Is the input felicitous?

Equations

• Interfaces.isFelicitous t = ((Interfaces.FelicityCondition.check t).status == Interfaces.FelicityStatus.felicitous)

def Interfaces.isOdd {T : Type u_1} [FelicityCondition T] (t : T) : Bool

Is the input odd?

Equations

• Interfaces.isOdd t = ((Interfaces.FelicityCondition.check t).status == Interfaces.FelicityStatus.odd)

def Interfaces.felicityAgree {α : Type u_1} {T₁ : Type u_2} {T₂ : Type u_3} [FelicityCondition T₁] [FelicityCondition T₂] (f : α → T₁) (g : α → T₂) (a : α) : Bool

Two felicity theories agree on an input if they give the same status.

Equations

• Interfaces.felicityAgree f g a = ((Interfaces.FelicityCondition.check (f a)).status == (Interfaces.FelicityCondition.check (g a)).status)