inductive Semantics.Scope.ScopeConfig : Type

General scope configuration for two operators

• surface : ScopeConfig
• inverse : ScopeConfig

@[implicit_reducible]

instance Semantics.Scope.instDecidableEqScopeConfig : DecidableEq ScopeConfig

Equations

• Semantics.Scope.instDecidableEqScopeConfig x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Scope.instReprScopeConfig.repr : ScopeConfig → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Scope.instReprScopeConfig : Repr ScopeConfig

Equations

• Semantics.Scope.instReprScopeConfig = { reprPrec := Semantics.Scope.instReprScopeConfig.repr }

@[implicit_reducible]

instance Semantics.Scope.instInhabitedScopeConfig : Inhabited ScopeConfig

Equations

• Semantics.Scope.instInhabitedScopeConfig = { default := Semantics.Scope.instInhabitedScopeConfig.default }

def Semantics.Scope.instInhabitedScopeConfig.default : ScopeConfig

Equations

• Semantics.Scope.instInhabitedScopeConfig.default = Semantics.Scope.ScopeConfig.surface

inductive Semantics.Scope.QNScope : Type

Specific quantifier-negation scope orderings

• forallNeg : QNScope
• negForall : QNScope

@[implicit_reducible]

instance Semantics.Scope.instDecidableEqQNScope : DecidableEq QNScope

Equations

• Semantics.Scope.instDecidableEqQNScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Scope.instReprQNScope : Repr QNScope

Equations

• Semantics.Scope.instReprQNScope = { reprPrec := Semantics.Scope.instReprQNScope.repr }

def Semantics.Scope.instReprQNScope.repr : QNScope → ℕ → Std.Format

Equations

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

def Semantics.Scope.instInhabitedQNScope.default : QNScope

Equations

• Semantics.Scope.instInhabitedQNScope.default = Semantics.Scope.QNScope.forallNeg

@[implicit_reducible]

instance Semantics.Scope.instInhabitedQNScope : Inhabited QNScope

Equations

• Semantics.Scope.instInhabitedQNScope = { default := Semantics.Scope.instInhabitedQNScope.default }

def Semantics.Scope.toQNScope : ScopeConfig → QNScope

Convert general config to QN-specific scope

Equations

• Semantics.Scope.toQNScope Semantics.Scope.ScopeConfig.surface = Semantics.Scope.QNScope.forallNeg
• Semantics.Scope.toQNScope Semantics.Scope.ScopeConfig.inverse = Semantics.Scope.QNScope.negForall

def Semantics.Scope.ScopeConfig.toScopeReading (s : ScopeConfig) (op1 op2 : String) : ScopeTheory.ScopeReading

Convert ScopeConfig to abstract ScopeReading for binary scope

Equations

• Semantics.Scope.ScopeConfig.surface.toScopeReading op1 op2 = ScopeTheory.ScopeReading.surface [op1, op2]
• Semantics.Scope.ScopeConfig.inverse.toScopeReading op1 op2 = ScopeTheory.ScopeReading.inverse [op1, op2]

def Semantics.Scope.toAvailableScopes (configs : List ScopeConfig) (op1 op2 : String) : ScopeTheory.AvailableScopes

Convert list of ScopeConfigs to AvailableScopes (defaults to binary if empty)

Equations

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

structure Semantics.Scope.ScopeDerivation (F : Core.Logic.Intensional.Frame) (τ : Core.Logic.Intensional.Ty) : Type

A derivation that can be interpreted under multiple scope readings.

The same syntactic derivation can yield different semantic values depending on scope resolution.

• surface : String

  Surface form (string representation)

• meaningAt : ScopeConfig → F.Denot τ

  Semantic value as function of scope config

• availableScopes : List ScopeConfig

  Available scope readings

def Semantics.Scope.ScopeDerivation.allMeanings {F : Core.Logic.Intensional.Frame} {τ : Core.Logic.Intensional.Ty} (d : ScopeDerivation F τ) : List (ScopeConfig × F.Denot τ)

Get all meanings for a scope derivation

Equations

• d.allMeanings = List.map (fun (s : Semantics.Scope.ScopeConfig) => (s, d.meaningAt s)) d.availableScopes

structure Semantics.Scope.ScopedForm : Type

A form (utterance) with scope ambiguity.

This is the Montague-side representation of scope:

• What scope readings are available
• Identifiers for the scope-takers

Note: World-parametric meaning (for RSA) is handled separately in RSA/.

• surface : String

  Surface form (string representation)

• availableScopes : List ScopeConfig

  Available scope readings

• scopeTaker1 : String

  First scope-taker identifier

• scopeTaker2 : String

  Second scope-taker identifier

def Semantics.Scope.instReprScopedForm.repr : ScopedForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Scope.instReprScopedForm : Repr ScopedForm

Equations

• Semantics.Scope.instReprScopedForm = { reprPrec := Semantics.Scope.instReprScopedForm.repr }

def Semantics.Scope.ScopedForm.toAvailableScopes (f : ScopedForm) : ScopeTheory.AvailableScopes

Get available scopes as abstract ScopeReadings

Equations

• f.toAvailableScopes = Semantics.Scope.toAvailableScopes f.availableScopes f.scopeTaker1 f.scopeTaker2

def Semantics.Scope.allScopeConfigs : List ScopeConfig

All binary scope configurations

Equations

• Semantics.Scope.allScopeConfigs = [Semantics.Scope.ScopeConfig.surface, Semantics.Scope.ScopeConfig.inverse]

def Semantics.Scope.allQNScopes : List QNScope

All QN scope orderings

Equations

• Semantics.Scope.allQNScopes = [Semantics.Scope.QNScope.forallNeg, Semantics.Scope.QNScope.negForall]

def Semantics.Scope.scopeYieldsTrue {F : Core.Logic.Intensional.Frame} [(p : F.Denot Core.Logic.Intensional.Ty.t) → Decidable p] (d : ScopeDerivation F Core.Logic.Intensional.Ty.t) (s : ScopeConfig) : Bool

Check if scope config yields true under given semantics

Equations

• Semantics.Scope.scopeYieldsTrue d s = decide (d.meaningAt s)

inductive Semantics.Scope.ScopeEntailment : Type

Entailment structure between scope readings. Determines whether a quantifier-negation pair is diagnostic for scope preferences: independent readings allow contexts where exactly one reading is true; nested readings (one entails the other) do not.

• surfaceEntailsInverse : ScopeEntailment
• inverseEntailsSurface : ScopeEntailment
• independent : ScopeEntailment
• equivalent : ScopeEntailment

@[implicit_reducible]

instance Semantics.Scope.instDecidableEqScopeEntailment : DecidableEq ScopeEntailment

Equations

• Semantics.Scope.instDecidableEqScopeEntailment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Scope.instReprScopeEntailment : Repr ScopeEntailment

Equations

• Semantics.Scope.instReprScopeEntailment = { reprPrec := Semantics.Scope.instReprScopeEntailment.repr }

def Semantics.Scope.instReprScopeEntailment.repr : ScopeEntailment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Scope.instInhabitedScopeEntailment : Inhabited ScopeEntailment

Equations

• Semantics.Scope.instInhabitedScopeEntailment = { default := Semantics.Scope.instInhabitedScopeEntailment.default }

def Semantics.Scope.instInhabitedScopeEntailment.default : ScopeEntailment

Equations

• Semantics.Scope.instInhabitedScopeEntailment.default = Semantics.Scope.ScopeEntailment.surfaceEntailsInverse

def Semantics.Scope.classifyScopeEntailment {W : Type} (worlds : List W) (surface inverse : W → Bool) : ScopeEntailment

Classify scope entailment from truth-value functions over a world list.

Equations

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