def CCG.Combinators.B {α β γ : Type} (f : β → γ) (g : α → β) : α → γ

B combinator (composition): B f g x = f (g x).

Equations

• CCG.Combinators.B f g x = f (g x)

def CCG.Combinators.T {α β : Type} (x : α) : (α → β) → β

T combinator (type-raising): T x f = f x.

Equations

• CCG.Combinators.T x f = f x

def CCG.Combinators.S {α β γ : Type} (f : α → β → γ) (g : α → β) : α → γ

S combinator (substitution): S f g x = f x (g x).

Equations

• CCG.Combinators.S f g x = f x (g x)

def CCG.Combinators.I {α : Type} : α → α

I combinator (identity): I x = x.

Equations

• CCG.Combinators.I x = x

def CCG.Combinators.K {α β : Type} (x : α) : β → α

K combinator (constant): K x y = x.

Equations

• CCG.Combinators.K x x✝ = x

def CCG.Combinators.C {α β γ : Type} (f : α → β → γ) (x : β) (y : α) : γ

C combinator (commutation): C f x y = f y x.

Equations

• CCG.Combinators.C f x y = f y x

theorem CCG.Combinators.T_eq_CI {α β : Type} (x : α) : T x = C I x

T = CI: type-raising equals C applied to I (Steedman p. 206-207).

theorem CCG.Combinators.CI_is_T {α β : Type} : (fun (x : α) => C I x) = T

CI is T.

theorem CCG.Combinators.C_eq_B_T {α β γ : Type} (f : α → β → γ) (x : β) (y : α) : C f x y = B (T x) f y

C = B(T_) pointwise: C f x y = B (T x) f y (Church's result via Steedman p. 207).

theorem CCG.Combinators.C_from_B_T {α β γ : Type} (f : α → β → γ) (x : β) (y : α) : have Tx := T x; have fy := f y; C f x y = Tx fy

C from B and T pointwise.

theorem CCG.Combinators.B_comp {α β γ : Type} (f : β → γ) (g : α → β) : B f g = f ∘ g

B is function composition.

theorem CCG.Combinators.B_apply {α β γ : Type} (f : β → γ) (g : α → β) (x : α) : B f g x = f (g x)

B f g x = f (g x).

theorem CCG.Combinators.T_apply {α β : Type} (x : α) (f : α → β) : T x f = f x

T x f = f x.

theorem CCG.Combinators.S_apply {α β γ : Type} (f : α → β → γ) (g : α → β) (x : α) : S f g x = f x (g x)

S f g x = f x (g x).

theorem CCG.Combinators.I_apply {α : Type} (x : α) : I x = x

I x = x.

theorem CCG.Combinators.K_apply {α β : Type} (x : α) (y : β) : K x y = x

K x y = x.

theorem CCG.Combinators.I_eq_SKK {α : Type} : I = S K K

I = SKK.

theorem CCG.Combinators.B_eq_S_KS_K {α β γ : Type} (f : β → γ) (g : α → β) : B f g = S (K f) g

B f g = S (K f) g.

theorem CCG.Combinators.fcomp_is_B {m : Semantics.Montague.Model} {x y z : Cat} (f_sem : m.interpTy (catToTy (x.rslash y))) (g_sem : m.interpTy (catToTy (y.rslash z))) : (fun (arg : m.interpTy (catToTy z)) => f_sem (g_sem arg)) = B f_sem g_sem

Forward composition = B: fcomp semantics is B f g.

theorem CCG.Combinators.fcomp_type_is_B (x _y z : Cat) : catToTy (x.rslash z) = (catToTy z ⇒ catToTy x)

catToTy (X/Z) = catToTy Z => catToTy X.

theorem CCG.Combinators.bcomp_is_B {m : Semantics.Montague.Model} {x y z : Cat} (g_sem : m.interpTy (catToTy (y.lslash z))) (f_sem : m.interpTy (catToTy (x.lslash y))) : (fun (arg : m.interpTy (catToTy z)) => f_sem (g_sem arg)) = B f_sem g_sem

Backward composition = B: bcomp semantics is B f g.

theorem CCG.Combinators.type_raise_is_T {m : Semantics.Montague.Model} {x t : Cat} (a_sem : m.interpTy (catToTy x)) : (fun (f : m.interpTy (catToTy (t.lslash x))) => f a_sem) = T a_sem

Forward type-raising = T: semantics of ftr is T a.

theorem CCG.Combinators.ftr_type_is_T (x t : Cat) : catToTy (forwardTypeRaise x t) = ((catToTy x ⇒ catToTy t) ⇒ catToTy t)

catToTy (T/(T\X)) = (catToTy X => catToTy T) => catToTy T.

theorem CCG.Combinators.btr_type_is_T (x t : Cat) : catToTy (backwardTypeRaise x t) = ((catToTy x ⇒ catToTy t) ⇒ catToTy t)

Backward type-raising type = forward type-raising type.

theorem CCG.Combinators.crossed_comp_is_S {m : Semantics.Montague.Model} {x y z : Cat} (f_sem : m.interpTy (catToTy ((x.rslash y).rslash z))) (g_sem : m.interpTy (catToTy (y.rslash z))) : (fun (arg : m.interpTy (catToTy z)) => f_sem arg (g_sem arg)) = S f_sem g_sem

Crossed composition = S: (X/Y)/Z + Y/Z => X/Z with S f g x = f x (g x).

theorem CCG.Combinators.fapp_via_T {m : Semantics.Montague.Model} {x y : Cat} (f_sem : m.interpTy (catToTy (x.rslash y))) (a_sem : m.interpTy (catToTy y)) : f_sem a_sem = T a_sem f_sem

Forward application via T: f a = T a f.

def CCG.Combinators.apply' {α β : Type} (f : α → β) (a : α) : β

Direct function application.

Equations

• CCG.Combinators.apply' f a = f a

theorem CCG.Combinators.fapp_is_apply {m : Semantics.Montague.Model} {x y : Cat} (f_sem : m.interpTy (catToTy (x.rslash y))) (a_sem : m.interpTy (catToTy y)) : f_sem a_sem = apply' f_sem a_sem

theorem CCG.Combinators.subject_verb_composition {m : Semantics.Montague.Model} (subj_sem : m.interpTy (catToTy NP)) (verb_sem : m.interpTy (catToTy TV)) (obj : m.interpTy (catToTy NP)) : B (T subj_sem) verb_sem obj = verb_sem obj subj_sem

Type-raised subject composed with transitive verb gives a function from objects to truth values.

The computation is:

• subj_raised = T subj_sem = λf. f subj_sem
• result = B subj_raised verb_sem = λy. subj_raised (verb_sem y) = λy. verb_sem y subj_sem

structure CCG.Combinators.CombinatorCorrespondence : Prop

The combinator correspondence as a record

• fapp_apply {α β : Type} (f : α → β) (a : α) : f a = f a

  Forward application is function application

• fcomp_B {α β γ : Type} (f : β → γ) (g : α → β) (x : α) : (fun (z : α) => f (g z)) x = B f g x

  Forward composition is B

• ftr_T {α β : Type} (a : α) (f : α → β) : T a f = f a

  Type-raising is T

• xcomp_S {α β γ : Type} (f : α → β → γ) (g : α → β) (x : α) : (fun (z : α) => f z (g z)) x = S f g x

  Crossed composition is S

def CCG.Combinators.ccgCombinatorCorrespondence : CombinatorCorrespondence

The CCG-combinator correspondence holds

Equations

• CCG.Combinators.ccgCombinatorCorrespondence = ⋯

def CCG.Combinators.steedmanForwardApp {α β : Type} (f : α → β) (a : α) : β

Forward application: functor on left, argument on right

Equations

• CCG.Combinators.steedmanForwardApp f a = f a

def CCG.Combinators.steedmanBackwardApp {α β : Type} (a : α) (f : α → β) : β

Backward application: argument on left, functor on right

Equations

• CCG.Combinators.steedmanBackwardApp a f = f a

theorem CCG.Combinators.forward_backward_same_semantics {α β : Type} (f : α → β) (a : α) : steedmanForwardApp f a = steedmanBackwardApp a f

Both application rules have the same semantic effect: function application

theorem CCG.Combinators.steedman_B_def {α β γ : Type} (f : β → γ) (g : α → β) (x : α) : B f g x = f (g x)

Steedman's definition of B (p. 24): Bfgx ≡ f(gx)

theorem CCG.Combinators.forward_comp_semantics {α β γ : Type} (f : β → γ) (g : α → β) : B f g = fun (x : α) => f (g x)

Forward composition produces B-combined semantics

theorem CCG.Combinators.backward_comp_semantics {α β γ : Type} (g : α → β) (f : β → γ) : B f g = fun (x : α) => f (g x)

Backward composition also uses B, just with reversed linear order

def CCG.Combinators.B2 {α β γ δ : Type} (f : γ → δ) (g : α → β → γ) : α → β → δ

B² combinator: composition into a binary function

Equations

• CCG.Combinators.B2 f g x y = f (g x y)

def CCG.Combinators.B3 {α β γ δ ε : Type} (f : δ → ε) (g : α → β → γ → δ) : α → β → γ → ε

B³ combinator: composition into a ternary function

Equations

• CCG.Combinators.B3 f g x y z = f (g x y z)

theorem CCG.Combinators.B2_is_B_B {α β γ δ : Type} (f : γ → δ) (g : α → β → γ) : B2 f g = fun (x : α) => B f (g x)

B² is B composed with B

theorem CCG.Combinators.steedman_T_def {α β : Type} (x : α) (f : α → β) : T x f = f x

Steedman's definition of T (p. 33): Txf ≡ fx

theorem CCG.Combinators.type_raise_to_gq {α β : Type} (a : α) : T a = fun (f : α → β) => f a

Type-raising turns an entity into a generalized quantifier

theorem CCG.Combinators.steedman_S_def {α β γ : Type} (f : α → β → γ) (g : α → β) (x : α) : S f g x = f x (g x)

Steedman's definition of S (p. 57): Sfgx ≡ fx(gx)

theorem CCG.Combinators.S_distributes {α β γ : Type} (f : α → β → γ) (g : α → β) : S f g = fun (x : α) => f x (g x)

S distributes the argument to both functions

inductive CCG.Combinators.CCGRule : Type

The CCG combinatory rules as a sum type

• fapp : CCGRule
• bapp : CCGRule
• fcomp : CCGRule
• bcomp : CCGRule
• fcomp2 : CCGRule
• bcomp2 : CCGRule
• ftr : CCGRule
• btr : CCGRule
• bxs : CCGRule
• coord : CCGRule

instance CCG.Combinators.instDecidableEqCCGRule : DecidableEq CCGRule

Equations

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

def CCG.Combinators.instReprCCGRule.repr : CCGRule → ℕ → Std.Format

Equations

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

instance CCG.Combinators.instReprCCGRule : Repr CCGRule

Equations

• CCG.Combinators.instReprCCGRule = { reprPrec := CCG.Combinators.instReprCCGRule.repr }

def CCG.Combinators.ruleToSemantics : CCGRule → String

Each CCG rule corresponds to a specific combinator

Equations

• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.fapp = "function application: f a"
• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.bapp = "function application: f a"
• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.fcomp = "B combinator: λx.f(gx)"
• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.bcomp = "B combinator: λx.f(gx)"
• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.fcomp2 = "B² combinator: λxy.f(gxy)"
• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.bcomp2 = "B² combinator: λxy.f(gxy)"
• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.ftr = "T combinator: λf.fa"
• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.btr = "T combinator: λf.fa"
• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.bxs = "S combinator: λx.fx(gx)"
• CCG.Combinators.ruleToSemantics CCG.Combinators.CCGRule.coord = "coordination: λ...b(f...)(g...)"

theorem CCG.Combinators.catToTy_is_steedman_T (c : Cat) : ∃ (ty : Semantics.Montague.Ty), catToTy c = ty

The type mapping T from Steedman (13) - this is our catToTy

def CCG.Combinators.constituentCondition (d : DerivStep) : Prop

The Constituent Condition: derivations yield interpretable constituents. In CCG, this is automatic because categories encode semantic types.

Equations

• CCG.Combinators.constituentCondition d = ∀ (c : CCG.Cat), d.cat = some c → ∃ (ty : Semantics.Montague.Ty), CCG.catToTy c = ty

theorem CCG.Combinators.ccg_satisfies_constituent_condition (d : DerivStep) : constituentCondition d

CCG satisfies the Constituent Condition by construction

structure CCG.Combinators.VariableFreeSemantics : Prop

Combinatory grammars build meaning without bound variables. Every semantic operation is a combinator application.

• app_direct {α β : Type} (f : α → β) (x : α) : f x = f x

  All function application is direct (no variable binding)

• comp_is_B {α β γ : Type} (f : β → γ) (g : α → β) : (fun (x : α) => f (g x)) = B f g

  Composition uses B, not λ-abstraction

• raise_is_T {α β : Type} (x : α) : (fun (f : α → β) => f x) = T x

  Type-raising uses T, not λ-abstraction

def CCG.Combinators.ccgVariableFree : VariableFreeSemantics

CCG provides variable-free semantics

Equations

• CCG.Combinators.ccgVariableFree = ⋯

inductive CCG.Combinators.DependencyPattern : Type

Dependency pattern in a construction

• nesting : DependencyPattern
• intercalating : DependencyPattern

instance CCG.Combinators.instDecidableEqDependencyPattern : DecidableEq DependencyPattern

Equations

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

def CCG.Combinators.instReprDependencyPattern.repr : DependencyPattern → ℕ → Std.Format

Equations

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

instance CCG.Combinators.instReprDependencyPattern : Repr DependencyPattern

Equations

• CCG.Combinators.instReprDependencyPattern = { reprPrec := CCG.Combinators.instReprDependencyPattern.repr }

def CCG.Combinators.ccg_handles_pattern : DependencyPattern → Prop

CCG can handle both patterns (unlike pure CFGs)

Equations

• CCG.Combinators.ccg_handles_pattern CCG.Combinators.DependencyPattern.nesting = True
• CCG.Combinators.ccg_handles_pattern CCG.Combinators.DependencyPattern.intercalating = True

inductive CCG.Combinators.WordOrder : Type

Basic word order types

• SVO : WordOrder
• SOV : WordOrder
• VSO : WordOrder

instance CCG.Combinators.instDecidableEqWordOrder : DecidableEq WordOrder

Equations

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

instance CCG.Combinators.instReprWordOrder : Repr WordOrder

Equations

• CCG.Combinators.instReprWordOrder = { reprPrec := CCG.Combinators.instReprWordOrder.repr }

def CCG.Combinators.instReprWordOrder.repr : WordOrder → ℕ → Std.Format

Equations

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

inductive CCG.Combinators.GapPosition : Type

Which conjunct has the gap in gapping constructions

• left : GapPosition
• right : GapPosition

instance CCG.Combinators.instDecidableEqGapPosition : DecidableEq GapPosition

Equations

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

def CCG.Combinators.instReprGapPosition.repr : GapPosition → ℕ → Std.Format

Equations

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

instance CCG.Combinators.instReprGapPosition : Repr GapPosition

Equations

• CCG.Combinators.instReprGapPosition = { reprPrec := CCG.Combinators.instReprGapPosition.repr }

def CCG.Combinators.rossGappingUniversal (order : WordOrder) : GapPosition

Ross's Universal: Gap position correlates with word order

Equations

• CCG.Combinators.rossGappingUniversal CCG.Combinators.WordOrder.SVO = CCG.Combinators.GapPosition.right
• CCG.Combinators.rossGappingUniversal CCG.Combinators.WordOrder.VSO = CCG.Combinators.GapPosition.right
• CCG.Combinators.rossGappingUniversal CCG.Combinators.WordOrder.SOV = CCG.Combinators.GapPosition.left

def CCG.Combinators.gappingViolation (order : WordOrder) (gap : GapPosition) : Bool

The excluded patterns (from Steedman p. 17, example 22)

Equations

• CCG.Combinators.gappingViolation CCG.Combinators.WordOrder.SVO CCG.Combinators.GapPosition.left = true
• CCG.Combinators.gappingViolation CCG.Combinators.WordOrder.VSO CCG.Combinators.GapPosition.left = true
• CCG.Combinators.gappingViolation CCG.Combinators.WordOrder.SOV CCG.Combinators.GapPosition.right = true
• CCG.Combinators.gappingViolation order gap = false

def CCG.Combinators.senseUnitCondition {m : Semantics.Montague.Model} (cat : Cat) (_meaning : m.interpTy (catToTy cat)) : Prop

A fragment satisfies the Sense Unit Condition if it's semantically coherent

Equations

• CCG.Combinators.senseUnitCondition cat _meaning = True

structure CCG.Combinators.PrincipleOfAdjacency : Type

The Principle of Adjacency: rules apply only to adjacent elements

• adjacent : Bool

  Rules apply to string-adjacent entities

• finite : Bool

  Rules apply to finitely many entities

inductive CCG.Combinators.SlashDir : Type

Direction a functor seeks its argument

• forward : SlashDir
• backward : SlashDir

instance CCG.Combinators.instDecidableEqSlashDir : DecidableEq SlashDir

Equations

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

def CCG.Combinators.instReprSlashDir.repr : SlashDir → ℕ → Std.Format

Equations

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

instance CCG.Combinators.instReprSlashDir : Repr SlashDir

Equations

• CCG.Combinators.instReprSlashDir = { reprPrec := CCG.Combinators.instReprSlashDir.repr }

def CCG.Combinators.principleOfConsistency (functorDir : SlashDir) (argOnRight : Bool) : Bool

The Principle of Consistency: rules respect functor directionality

Equations

• CCG.Combinators.principleOfConsistency CCG.Combinators.SlashDir.forward true = true
• CCG.Combinators.principleOfConsistency CCG.Combinators.SlashDir.backward false = true
• CCG.Combinators.principleOfConsistency CCG.Combinators.SlashDir.forward false = false
• CCG.Combinators.principleOfConsistency CCG.Combinators.SlashDir.backward true = false

def CCG.Combinators.principleOfInheritance (inputSlash outputSlash : SlashDir) : Bool

The Principle of Inheritance: output slashes inherit from inputs

Equations

• CCG.Combinators.principleOfInheritance inputSlash outputSlash = (inputSlash == outputSlash)

inductive CCG.Combinators.RuleType : Type

Classification of combinatory rules by order-preservation

• orderPreserving : RuleType
• crossed : RuleType

instance CCG.Combinators.instDecidableEqRuleType : DecidableEq RuleType

Equations

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

def CCG.Combinators.instReprRuleType.repr : RuleType → ℕ → Std.Format

Equations

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

instance CCG.Combinators.instReprRuleType : Repr RuleType

Equations

• CCG.Combinators.instReprRuleType = { reprPrec := CCG.Combinators.instReprRuleType.repr }

inductive CCG.Combinators.CompositionRule : Type

The complete catalog of composition rules

• fcomp : CompositionRule
• fcompX : CompositionRule
• bcomp : CompositionRule
• bcompX : CompositionRule

instance CCG.Combinators.instDecidableEqCompositionRule : DecidableEq CompositionRule

Equations

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

def CCG.Combinators.instReprCompositionRule.repr : CompositionRule → ℕ → Std.Format

Equations

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

instance CCG.Combinators.instReprCompositionRule : Repr CompositionRule

Equations

• CCG.Combinators.instReprCompositionRule = { reprPrec := CCG.Combinators.instReprCompositionRule.repr }

inductive CCG.Combinators.SubstitutionRule : Type

The complete catalog of substitution rules

• fsub : SubstitutionRule
• fsubX : SubstitutionRule
• bsub : SubstitutionRule
• bsubX : SubstitutionRule

instance CCG.Combinators.instDecidableEqSubstitutionRule : DecidableEq SubstitutionRule

Equations

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

instance CCG.Combinators.instReprSubstitutionRule : Repr SubstitutionRule

Equations

• CCG.Combinators.instReprSubstitutionRule = { reprPrec := CCG.Combinators.instReprSubstitutionRule.repr }

def CCG.Combinators.instReprSubstitutionRule.repr : SubstitutionRule → ℕ → Std.Format

Equations

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

def CCG.Combinators.CompositionRule.ruleType : CompositionRule → RuleType

Classify a composition rule

Equations

• CCG.Combinators.CompositionRule.fcomp.ruleType = CCG.Combinators.RuleType.orderPreserving
• CCG.Combinators.CompositionRule.fcompX.ruleType = CCG.Combinators.RuleType.crossed
• CCG.Combinators.CompositionRule.bcomp.ruleType = CCG.Combinators.RuleType.orderPreserving
• CCG.Combinators.CompositionRule.bcompX.ruleType = CCG.Combinators.RuleType.crossed

def CCG.Combinators.SubstitutionRule.ruleType : SubstitutionRule → RuleType

Classify a substitution rule

Equations

• CCG.Combinators.SubstitutionRule.fsub.ruleType = CCG.Combinators.RuleType.orderPreserving
• CCG.Combinators.SubstitutionRule.fsubX.ruleType = CCG.Combinators.RuleType.crossed
• CCG.Combinators.SubstitutionRule.bsub.ruleType = CCG.Combinators.RuleType.orderPreserving
• CCG.Combinators.SubstitutionRule.bsubX.ruleType = CCG.Combinators.RuleType.crossed

def CCG.Combinators.isOrderPreserving (r : CompositionRule) : Bool

Order-preserving rules don't change word order

Equations

• CCG.Combinators.isOrderPreserving r = (r.ruleType == CCG.Combinators.RuleType.orderPreserving)

def CCG.Combinators.isCrossed (r : CompositionRule) : Bool

Non-order-preserving (crossed) rules can permute arguments

Equations

• CCG.Combinators.isCrossed r = (r.ruleType == CCG.Combinators.RuleType.crossed)

inductive CCG.Combinators.ExtractionType : Type

Extraction type

• subject : ExtractionType
• object : ExtractionType

instance CCG.Combinators.instDecidableEqExtractionType : DecidableEq ExtractionType

Equations

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

instance CCG.Combinators.instReprExtractionType : Repr ExtractionType

Equations

• CCG.Combinators.instReprExtractionType = { reprPrec := CCG.Combinators.instReprExtractionType.repr }

def CCG.Combinators.instReprExtractionType.repr : ExtractionType → ℕ → Std.Format

Equations

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

def CCG.Combinators.svoSubjectExtractionBlocked : Bool

In SVO languages, subject extraction from that-complements is blocked

Equations

• CCG.Combinators.svoSubjectExtractionBlocked = true

theorem CCG.Combinators.extraction_asymmetry_from_directionality : svoSubjectExtractionBlocked = true

The asymmetry follows from directionality, not from ECP

inductive CCG.Combinators.ShiftFeature : Type

Feature controlling whether an argument can shift

• plusShift : ShiftFeature
• minusShift : ShiftFeature

instance CCG.Combinators.instDecidableEqShiftFeature : DecidableEq ShiftFeature

Equations

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

instance CCG.Combinators.instReprShiftFeature : Repr ShiftFeature

Equations

• CCG.Combinators.instReprShiftFeature = { reprPrec := CCG.Combinators.instReprShiftFeature.repr }

def CCG.Combinators.instReprShiftFeature.repr : ShiftFeature → ℕ → Std.Format

Equations

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

def CCG.Combinators.canHeavyShift (f : ShiftFeature) : Bool

Heavy NP shift requires the +SHIFT feature

Equations

• CCG.Combinators.canHeavyShift CCG.Combinators.ShiftFeature.plusShift = true
• CCG.Combinators.canHeavyShift CCG.Combinators.ShiftFeature.minusShift = false

inductive CCG.Combinators.NominalType : Type

Types of nominal interpretations

• trueQuantifier : NominalType
• arbitraryObject : NominalType
• definite : NominalType

instance CCG.Combinators.instDecidableEqNominalType : DecidableEq NominalType

Equations

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

instance CCG.Combinators.instReprNominalType : Repr NominalType

Equations

• CCG.Combinators.instReprNominalType = { reprPrec := CCG.Combinators.instReprNominalType.repr }

def CCG.Combinators.instReprNominalType.repr : NominalType → ℕ → Std.Format

Equations

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

def CCG.Combinators.canScopeInvert (nt : NominalType) : Bool

True quantifiers can induce scope inversion

Equations

• CCG.Combinators.canScopeInvert CCG.Combinators.NominalType.trueQuantifier = true
• CCG.Combinators.canScopeInvert CCG.Combinators.NominalType.arbitraryObject = false
• CCG.Combinators.canScopeInvert CCG.Combinators.NominalType.definite = false

def CCG.Combinators.geachParallelScope : Prop

Geach's constraint: coordinated elements must have parallel scope

Equations

• CCG.Combinators.geachParallelScope = True

def CCG.Combinators.distributionFollowsBinding : Prop

The c-command condition on distribution parallels binding

Equations

• CCG.Combinators.distributionFollowsBinding = True

def CCG.Combinators.ccgMonotonic : Prop

CCG is monotonic: structures are never revised

Equations

• CCG.Combinators.ccgMonotonic = True

def CCG.Combinators.ccgMonostratal : Prop

CCG is monostratal: only Logical Form is a true level

Equations

• CCG.Combinators.ccgMonostratal = True

def CCG.Combinators.semanticEquivalenceClass : Prop

Different derivations can yield the same Logical Form

Equations

• CCG.Combinators.semanticEquivalenceClass = True