def npCoordinationData : StringPhenomenonData

NP coordination minimal pairs

Equations

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

def vpCoordinationData : StringPhenomenonData

VP coordination minimal pairs

Equations

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

def sCoordinationData : StringPhenomenonData

S coordination minimal pairs

Equations

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

structure SemanticEquivalence : Type

Theory-Neutral Semantic Data for Non-Constituent Coordination

The core empirical observation is a semantic equivalence:

"John likes and Mary hates beans" ≡ "John likes beans and Mary hates beans"

This is theory-neutral: we don't presuppose any logical formalism, just that native speakers judge these sentences to have the same meaning (same truth conditions, same entailments, intersubstitutable in any context).

• sentence : List String

  The non-constituent coordination sentence

• equivalentTo : List String

  The semantically equivalent spelled-out version

• bothGrammatical : Bool

  Both are grammatical

def instReprSemanticEquivalence.repr : SemanticEquivalence → Nat → Std.Format

Equations

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

instance instReprSemanticEquivalence : Repr SemanticEquivalence

Equations

• instReprSemanticEquivalence = { reprPrec := instReprSemanticEquivalence.repr }

def johnLikesAndMaryHatesBeans : SemanticEquivalence

"John likes and Mary hates beans" ≡ "John likes beans and Mary hates beans"

Equations

• johnLikesAndMaryHatesBeans = { sentence := ["John", "likes", "and", "Mary", "hates", "beans"], equivalentTo := ["John", "likes", "beans", "and", "Mary", "hates", "beans"] }

def warrenCookedAndBetsyAte : SemanticEquivalence

"Warren cooked and Betsy ate the potatoes" ≡ "Warren cooked the potatoes and Betsy ate the potatoes"

Equations

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

def iMetAndYouSaw : SemanticEquivalence

"I met and you saw John" ≡ "I met John and you saw John"

Equations

• iMetAndYouSaw = { sentence := ["I", "met", "and", "you", "saw", "John"], equivalentTo := ["I", "met", "John", "and", "you", "saw", "John"] }

class CapturesNonConstituentCoord (G : Type) : Type

A theory captures non-constituent coordination if it derives equivalent meanings for both sentences in a SemanticEquivalence pair.

• bothDerive : G → SemanticEquivalence → Bool

  Both sentences derive

• meaningsEquivalent : G → SemanticEquivalence → Bool

  The derived meanings are equivalent