RSA Scalar Implicatures

@cite{bergen-levy-goodman-2016} @cite{frank-goodman-2012} @cite{goodman-frank-2016}

RSA scalar implicature infrastructure. Scale positions are looked up from word forms via Alternatives.scaleOf.

Status

The ℚ-based RSA evaluation infrastructure (RSA.Eval, boolToRat, RSAScenario) has been removed. The scalar implicature results and RSA ImplicatureTheory instance need to be re-implemented using the new RSAConfig framework.

inductive RSA.ScalarImplicatures.ScalarWorld : Type

World states for scalar implicature reasoning (coarser partition)

• none : ScalarWorld
• some : ScalarWorld
• all : ScalarWorld

instance RSA.ScalarImplicatures.instDecidableEqScalarWorld : DecidableEq ScalarWorld

Equations

• RSA.ScalarImplicatures.instDecidableEqScalarWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.ScalarImplicatures.instBEqScalarWorld.beq : ScalarWorld → ScalarWorld → Bool

Equations

• RSA.ScalarImplicatures.instBEqScalarWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.ScalarImplicatures.instBEqScalarWorld : BEq ScalarWorld

Equations

• RSA.ScalarImplicatures.instBEqScalarWorld = { beq := RSA.ScalarImplicatures.instBEqScalarWorld.beq }

instance RSA.ScalarImplicatures.instReprScalarWorld : Repr ScalarWorld

Equations

• RSA.ScalarImplicatures.instReprScalarWorld = { reprPrec := RSA.ScalarImplicatures.instReprScalarWorld.repr }

def RSA.ScalarImplicatures.instReprScalarWorld.repr : ScalarWorld → ℕ → Std.Format

Equations

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

def RSA.ScalarImplicatures.instInhabitedScalarWorld.default : ScalarWorld

Equations

• RSA.ScalarImplicatures.instInhabitedScalarWorld.default = RSA.ScalarImplicatures.ScalarWorld.none

instance RSA.ScalarImplicatures.instInhabitedScalarWorld : Inhabited ScalarWorld

Equations

• RSA.ScalarImplicatures.instInhabitedScalarWorld = { default := RSA.ScalarImplicatures.instInhabitedScalarWorld.default }

structure RSA.ScalarImplicatures.RSAScalarResult : Type

RSA scalar implicature result.

• utterance : String
• probSomeNotAll : ℚ
• probAll : ℚ
• implicatureHolds : Bool

def RSA.ScalarImplicatures.instReprRSAScalarResult.repr : RSAScalarResult → ℕ → Std.Format

Equations

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

instance RSA.ScalarImplicatures.instReprRSAScalarResult : Repr RSAScalarResult

Equations

• RSA.ScalarImplicatures.instReprRSAScalarResult = { reprPrec := RSA.ScalarImplicatures.instReprRSAScalarResult.repr }

def RSA.ScalarImplicatures.hasSomeQuantifier (words : List String) : Bool

Check if any word in the list is a "some" quantifier.

Equations

• RSA.ScalarImplicatures.hasSomeQuantifier words = words.any fun (w : String) => Alternatives.scaleOf w == some (Alternatives.ScaleMembership.quantifier Alternatives.Quantifiers.QuantExpr.some_)

def RSA.ScalarImplicatures.hasAllQuantifier (words : List String) : Bool

Check if any word in the list is an "all/every" quantifier.

Equations

• RSA.ScalarImplicatures.hasAllQuantifier words = words.any fun (w : String) => Alternatives.scaleOf w == some (Alternatives.ScaleMembership.quantifier Alternatives.Quantifiers.QuantExpr.all)