CCG Scope Theory

Derivation-type analysis of quantifier scope: derivations built by composition or type-raising license scope flexibility that pure application does not. [Ste00a] §6.8 uses this contrast for West Germanic verb-cluster word orders (consumed by Linglib.Studies.Steedman2000); the book's fuller account (§4.4) refines the bare derivation–scope link, which Steedman notes overgenerates as stated.

structure CCG.Scope.ScopeTaker : Type

A scope-taking element in a CCG derivation.

• id : String
• surfacePosition : ℕ
• cat : Cat

def CCG.Scope.instReprScopeTaker.repr : ScopeTaker → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CCG.Scope.instReprScopeTaker : Repr ScopeTaker

Equations

• CCG.Scope.instReprScopeTaker = { reprPrec := CCG.Scope.instReprScopeTaker.repr }

inductive CCG.Scope.DerivationType : Type

Derivation type for scope analysis.

• directApp : DerivationType
• typeRaised : DerivationType
• composed : DerivationType

@[implicit_reducible]

instance CCG.Scope.instDecidableEqDerivationType : DecidableEq DerivationType

Equations

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

def CCG.Scope.instReprDerivationType.repr : DerivationType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CCG.Scope.instReprDerivationType : Repr DerivationType

Equations

• CCG.Scope.instReprDerivationType = { reprPrec := CCG.Scope.instReprDerivationType.repr }

def CCG.Scope.analyzeDerivation : DerivStep → DerivationType

Analyze derivation to determine its type.

Equations

• One or more equations did not get rendered due to their size.
• CCG.Scope.analyzeDerivation (CCG.DerivStep.lex a) = CCG.Scope.DerivationType.directApp
• CCG.Scope.analyzeDerivation (a.fcomp a_1) = CCG.Scope.DerivationType.composed
• CCG.Scope.analyzeDerivation (a.bcomp a_1) = CCG.Scope.DerivationType.composed
• CCG.Scope.analyzeDerivation (a.fcompx a_1) = CCG.Scope.DerivationType.composed
• CCG.Scope.analyzeDerivation (a.ftr a_1) = CCG.Scope.DerivationType.typeRaised
• CCG.Scope.analyzeDerivation (a.btr a_1) = CCG.Scope.DerivationType.typeRaised

def CCG.Scope.derivationTypeToAvailability : DerivationType → ScopeTheory.BinaryScopeAvailability

Determine scope availability from derivation type.

Equations

• CCG.Scope.derivationTypeToAvailability CCG.Scope.DerivationType.directApp = ScopeTheory.BinaryScopeAvailability.surfaceOnly
• CCG.Scope.derivationTypeToAvailability CCG.Scope.DerivationType.typeRaised = ScopeTheory.BinaryScopeAvailability.ambiguous
• CCG.Scope.derivationTypeToAvailability CCG.Scope.DerivationType.composed = ScopeTheory.BinaryScopeAvailability.ambiguous

structure CCG.Scope.ScopedDerivation : Type

A CCG derivation annotated with scope-taker information.

• deriv : DerivStep
• scopeTakers : List ScopeTaker
• hasTwoOrMore : self.scopeTakers.length ≥ 2

def CCG.Scope.instReprScopedDerivation.repr : ScopedDerivation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CCG.Scope.instReprScopedDerivation : Repr ScopedDerivation

Equations

• CCG.Scope.instReprScopedDerivation = { reprPrec := CCG.Scope.instReprScopedDerivation.repr }

def CCG.Scope.ScopedDerivation.availability (sd : ScopedDerivation) : ScopeTheory.BinaryScopeAvailability

Equations

• sd.availability = CCG.Scope.derivationTypeToAvailability (CCG.Scope.analyzeDerivation sd.deriv)

def CCG.Scope.ScopedDerivation.toAvailableScopes (sd : ScopedDerivation) : ScopeTheory.AvailableScopes

Equations

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

def CCG.Scope.everyHorse_surface : DerivStep

Equations

• CCG.Scope.everyHorse_surface = (CCG.DerivStep.lex { form := "every horse", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "didn't jump", cat := CCG.IV })

def CCG.Scope.everyHorse_inverse : DerivStep

Equations

• CCG.Scope.everyHorse_inverse = ((CCG.DerivStep.lex { form := "every horse", cat := CCG.NP }).ftr CCG.S).fcomp (CCG.DerivStep.lex { form := "didn't jump", cat := CCG.IV })