inductive Phenomena.Ellipsis.Gapping.WordOrder : Type

Basic word order types for transitive clauses.

S = Subject, V = Verb, O = Object

• SOV : WordOrder
• SVO : WordOrder
• VSO : WordOrder
• VOS : WordOrder
• OVS : WordOrder
• OSV : WordOrder

instance Phenomena.Ellipsis.Gapping.instDecidableEqWordOrder : DecidableEq WordOrder

Equations

• Phenomena.Ellipsis.Gapping.instDecidableEqWordOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Ellipsis.Gapping.instBEqWordOrder : BEq WordOrder

Equations

• Phenomena.Ellipsis.Gapping.instBEqWordOrder = { beq := Phenomena.Ellipsis.Gapping.instBEqWordOrder.beq }

def Phenomena.Ellipsis.Gapping.instBEqWordOrder.beq : WordOrder → WordOrder → Bool

Equations

• Phenomena.Ellipsis.Gapping.instBEqWordOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Ellipsis.Gapping.instReprWordOrder : Repr WordOrder

Equations

• Phenomena.Ellipsis.Gapping.instReprWordOrder = { reprPrec := Phenomena.Ellipsis.Gapping.instReprWordOrder.repr }

def Phenomena.Ellipsis.Gapping.instReprWordOrder.repr : WordOrder → Nat → Std.Format

Equations

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

structure Phenomena.Ellipsis.Gapping.WordOrderProfile : Type

Languages can have different orders in main vs subordinate clauses

• mainClause : WordOrder
• subClause : WordOrder

def Phenomena.Ellipsis.Gapping.instReprWordOrderProfile.repr : WordOrderProfile → Nat → Std.Format

Equations

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

instance Phenomena.Ellipsis.Gapping.instReprWordOrderProfile : Repr WordOrderProfile

Equations

• Phenomena.Ellipsis.Gapping.instReprWordOrderProfile = { reprPrec := Phenomena.Ellipsis.Gapping.instReprWordOrderProfile.repr }

inductive Phenomena.Ellipsis.Gapping.GappingDirection : Type

Direction of gapping in coordinate structures.

Forward: verb in first conjunct, gap in second "Dexter ate bread, and Warren, potatoes" ↑ ↑gap

Backward: gap in first conjunct, verb in second "Ken Naomi-o, Erika Sara-o tazuneta" ↑gap ↑verb

• forward : GappingDirection
• backward : GappingDirection

instance Phenomena.Ellipsis.Gapping.instDecidableEqGappingDirection : DecidableEq GappingDirection

Equations

• Phenomena.Ellipsis.Gapping.instDecidableEqGappingDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Ellipsis.Gapping.instBEqGappingDirection : BEq GappingDirection

Equations

• Phenomena.Ellipsis.Gapping.instBEqGappingDirection = { beq := Phenomena.Ellipsis.Gapping.instBEqGappingDirection.beq }

def Phenomena.Ellipsis.Gapping.instBEqGappingDirection.beq : GappingDirection → GappingDirection → Bool

Equations

• Phenomena.Ellipsis.Gapping.instBEqGappingDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Ellipsis.Gapping.instReprGappingDirection : Repr GappingDirection

Equations

• Phenomena.Ellipsis.Gapping.instReprGappingDirection = { reprPrec := Phenomena.Ellipsis.Gapping.instReprGappingDirection.repr }

def Phenomena.Ellipsis.Gapping.instReprGappingDirection.repr : GappingDirection → Nat → Std.Format

Equations

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

structure Phenomena.Ellipsis.Gapping.GappingPattern : Type

A gapping pattern describes what a language allows.

• allowsForward : Bool
• allowsBackward : Bool

instance Phenomena.Ellipsis.Gapping.instReprGappingPattern : Repr GappingPattern

Equations

• Phenomena.Ellipsis.Gapping.instReprGappingPattern = { reprPrec := Phenomena.Ellipsis.Gapping.instReprGappingPattern.repr }

def Phenomena.Ellipsis.Gapping.instReprGappingPattern.repr : GappingPattern → Nat → Std.Format

Equations

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

def Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly : GappingPattern

Equations

• Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly = { allowsForward := true, allowsBackward := false }

def Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly : GappingPattern

Equations

• Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly = { allowsForward := false, allowsBackward := true }

def Phenomena.Ellipsis.Gapping.GappingPattern.both : GappingPattern

Equations

• Phenomena.Ellipsis.Gapping.GappingPattern.both = { allowsForward := true, allowsBackward := true }

def Phenomena.Ellipsis.Gapping.GappingPattern.neither : GappingPattern

Equations

• Phenomena.Ellipsis.Gapping.GappingPattern.neither = { allowsForward := false, allowsBackward := false }

def Phenomena.Ellipsis.Gapping.rossOriginal (order : WordOrder) : GappingPattern

Ross's original generalization about gapping and word order.

Equations

• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.SOV = Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.VSO = Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.SVO = Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.VOS = Phenomena.Ellipsis.Gapping.GappingPattern.forwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.OVS = Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly
• Phenomena.Ellipsis.Gapping.rossOriginal Phenomena.Ellipsis.Gapping.WordOrder.OSV = Phenomena.Ellipsis.Gapping.GappingPattern.backwardOnly

def Phenomena.Ellipsis.Gapping.hasRightwardVerbs : WordOrder → Bool

Steedman's revised generalization: gapping depends on lexical availability of verb categories, not "underlying" word order.

A language allows forward gapping iff it has rightward-combining verbs. A language allows backward gapping iff it has leftward-combining verbs.

Equations

• Phenomena.Ellipsis.Gapping.hasRightwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.VSO = true
• Phenomena.Ellipsis.Gapping.hasRightwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.SVO = true
• Phenomena.Ellipsis.Gapping.hasRightwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.VOS = true
• Phenomena.Ellipsis.Gapping.hasRightwardVerbs x✝ = false

def Phenomena.Ellipsis.Gapping.hasLeftwardVerbs : WordOrder → Bool

Equations

• Phenomena.Ellipsis.Gapping.hasLeftwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.SOV = true
• Phenomena.Ellipsis.Gapping.hasLeftwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.OVS = true
• Phenomena.Ellipsis.Gapping.hasLeftwardVerbs Phenomena.Ellipsis.Gapping.WordOrder.OSV = true
• Phenomena.Ellipsis.Gapping.hasLeftwardVerbs x✝ = false

def Phenomena.Ellipsis.Gapping.rossRevised (profile : WordOrderProfile) : GappingPattern

Equations

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

def Phenomena.Ellipsis.Gapping.japanese : WordOrderProfile

Japanese: pure SOV, backward gapping only

Equations

• Phenomena.Ellipsis.Gapping.japanese = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.SOV, subClause := Phenomena.Ellipsis.Gapping.WordOrder.SOV }

def Phenomena.Ellipsis.Gapping.irish : WordOrderProfile

Irish: pure VSO, forward gapping only

Equations

• Phenomena.Ellipsis.Gapping.irish = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.VSO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.VSO }

def Phenomena.Ellipsis.Gapping.english : WordOrderProfile

English: pure SVO, forward gapping only

Equations

• Phenomena.Ellipsis.Gapping.english = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.SVO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.SVO }

def Phenomena.Ellipsis.Gapping.dutch : WordOrderProfile

Dutch: VSO main clause, SOV subordinate clause - both directions

Equations

• Phenomena.Ellipsis.Gapping.dutch = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.SVO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.SOV }

def Phenomena.Ellipsis.Gapping.german : WordOrderProfile

German: similar to Dutch

Equations

• Phenomena.Ellipsis.Gapping.german = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.SVO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.SOV }

def Phenomena.Ellipsis.Gapping.zapotec : WordOrderProfile

Zapotec: VSO subordinate, but allows SOV main clause - both directions

Equations

• Phenomena.Ellipsis.Gapping.zapotec = { mainClause := Phenomena.Ellipsis.Gapping.WordOrder.VSO, subClause := Phenomena.Ellipsis.Gapping.WordOrder.VSO }

structure Phenomena.Ellipsis.Gapping.GappingExample : Type

A gapping example in a specific language.

• language : String
• surface : String
• gloss : String
• translation : String
• direction : GappingDirection
• isGrammatical : Bool

def Phenomena.Ellipsis.Gapping.instReprGappingExample.repr : GappingExample → Nat → Std.Format

Equations

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

instance Phenomena.Ellipsis.Gapping.instReprGappingExample : Repr GappingExample

Equations

• Phenomena.Ellipsis.Gapping.instReprGappingExample = { reprPrec := Phenomena.Ellipsis.Gapping.instReprGappingExample.repr }

def Phenomena.Ellipsis.Gapping.japanese_backward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.japanese_forward_bad : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.irish_forward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.irish_backward_bad : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.english_forward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.english_backward_bad : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.dutch_main_forward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.dutch_sub_backward : GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.allGappingExamples : List GappingExample

Equations

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

def Phenomena.Ellipsis.Gapping.grammaticalExamples : List GappingExample

Equations

• Phenomena.Ellipsis.Gapping.grammaticalExamples = List.filter (fun (x : Phenomena.Ellipsis.Gapping.GappingExample) => x.isGrammatical) Phenomena.Ellipsis.Gapping.allGappingExamples

def Phenomena.Ellipsis.Gapping.ungrammaticalExamples : List GappingExample

Equations

• Phenomena.Ellipsis.Gapping.ungrammaticalExamples = List.filter (fun (x : Phenomena.Ellipsis.Gapping.GappingExample) => !x.isGrammatical) Phenomena.Ellipsis.Gapping.allGappingExamples

inductive Phenomena.Ellipsis.Gapping.EllipsisType : Type

Types of elliptical constructions (Steedman's taxonomy).

Gapping and Stripping are syntactically mediated via CCG. VP Ellipsis and Sluicing are purely anaphoric.

• gapping : EllipsisType
• stripping : EllipsisType
• vpEllipsis : EllipsisType
• sluicing : EllipsisType

instance Phenomena.Ellipsis.Gapping.instDecidableEqEllipsisType : DecidableEq EllipsisType

Equations

• Phenomena.Ellipsis.Gapping.instDecidableEqEllipsisType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Ellipsis.Gapping.instBEqEllipsisType.beq : EllipsisType → EllipsisType → Bool

Equations

• Phenomena.Ellipsis.Gapping.instBEqEllipsisType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Ellipsis.Gapping.instBEqEllipsisType : BEq EllipsisType

Equations

• Phenomena.Ellipsis.Gapping.instBEqEllipsisType = { beq := Phenomena.Ellipsis.Gapping.instBEqEllipsisType.beq }

def Phenomena.Ellipsis.Gapping.instReprEllipsisType.repr : EllipsisType → Nat → Std.Format

Equations

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

instance Phenomena.Ellipsis.Gapping.instReprEllipsisType : Repr EllipsisType

Equations

• Phenomena.Ellipsis.Gapping.instReprEllipsisType = { reprPrec := Phenomena.Ellipsis.Gapping.instReprEllipsisType.repr }

def Phenomena.Ellipsis.Gapping.isSyntacticallyMediated : EllipsisType → Bool

Is the ellipsis type syntactically mediated (vs purely anaphoric)?

Equations

• Phenomena.Ellipsis.Gapping.isSyntacticallyMediated Phenomena.Ellipsis.Gapping.EllipsisType.gapping = true
• Phenomena.Ellipsis.Gapping.isSyntacticallyMediated Phenomena.Ellipsis.Gapping.EllipsisType.stripping = true
• Phenomena.Ellipsis.Gapping.isSyntacticallyMediated Phenomena.Ellipsis.Gapping.EllipsisType.vpEllipsis = false
• Phenomena.Ellipsis.Gapping.isSyntacticallyMediated Phenomena.Ellipsis.Gapping.EllipsisType.sluicing = false

def Phenomena.Ellipsis.Gapping.hasWordOrderConstraints : EllipsisType → Bool

Does the ellipsis type exhibit word-order constraints?

Equations

• Phenomena.Ellipsis.Gapping.hasWordOrderConstraints Phenomena.Ellipsis.Gapping.EllipsisType.gapping = true
• Phenomena.Ellipsis.Gapping.hasWordOrderConstraints Phenomena.Ellipsis.Gapping.EllipsisType.stripping = true
• Phenomena.Ellipsis.Gapping.hasWordOrderConstraints Phenomena.Ellipsis.Gapping.EllipsisType.vpEllipsis = false
• Phenomena.Ellipsis.Gapping.hasWordOrderConstraints Phenomena.Ellipsis.Gapping.EllipsisType.sluicing = false

theorem Phenomena.Ellipsis.Gapping.sov_backward_only : (rossRevised japanese).allowsForward = false ∧ (rossRevised japanese).allowsBackward = true

Pure SOV language has backward gapping only

theorem Phenomena.Ellipsis.Gapping.vso_forward_only : (rossRevised irish).allowsForward = true ∧ (rossRevised irish).allowsBackward = false

Pure VSO language has forward gapping only

theorem Phenomena.Ellipsis.Gapping.svo_forward_only : (rossRevised english).allowsForward = true ∧ (rossRevised english).allowsBackward = false

Pure SVO language has forward gapping only

theorem Phenomena.Ellipsis.Gapping.mixed_allows_both : (rossRevised dutch).allowsForward = true ∧ (rossRevised dutch).allowsBackward = true

Mixed order language (Dutch) allows both

def Phenomena.Ellipsis.Gapping.requiresSyntacticIdentity : EllipsisType → Bool

Does this ellipsis type require syntactic identity (SIC)? @cite{anand-hardt-mccloskey-2021}: sluicing and gapping require structural matching; VP ellipsis does not.

Equations

• Phenomena.Ellipsis.Gapping.requiresSyntacticIdentity Phenomena.Ellipsis.Gapping.EllipsisType.sluicing = true
• Phenomena.Ellipsis.Gapping.requiresSyntacticIdentity Phenomena.Ellipsis.Gapping.EllipsisType.gapping = true
• Phenomena.Ellipsis.Gapping.requiresSyntacticIdentity Phenomena.Ellipsis.Gapping.EllipsisType.stripping = true
• Phenomena.Ellipsis.Gapping.requiresSyntacticIdentity Phenomena.Ellipsis.Gapping.EllipsisType.vpEllipsis = false

def Phenomena.Ellipsis.Gapping.requiresSemanticIdentity : EllipsisType → Bool

Does this ellipsis type require semantic identity (e-GIVENness)? @cite{anand-hardt-mccloskey-2021}: all ellipsis types require e-GIVENness.

Equations

• Phenomena.Ellipsis.Gapping.requiresSemanticIdentity x✝ = true

theorem Phenomena.Ellipsis.Gapping.sluicing_requires_both : requiresSemanticIdentity EllipsisType.sluicing = true ∧ requiresSyntacticIdentity EllipsisType.sluicing = true

Sluicing requires both semantic and syntactic identity.

theorem Phenomena.Ellipsis.Gapping.vpe_semantic_only : requiresSemanticIdentity EllipsisType.vpEllipsis = true ∧ requiresSyntacticIdentity EllipsisType.vpEllipsis = false

VP ellipsis requires semantic identity but not syntactic identity.

theorem Phenomena.Ellipsis.Gapping.vpe_voice_mismatch_explained : requiresSyntacticIdentity EllipsisType.vpEllipsis = false

VP ellipsis tolerates voice mismatches because it lacks the SIC. Since VPE has no syntactic identity requirement, voice flavor differences (agentive vs nonThematic) are irrelevant — only e-GIVENness (semantic identity) must hold.