Steedman 2000: The Syntactic Process

CCG predictions from [Ste00a], one section per phenomenon:

• Word order: slash direction in lexical categories enforces English SVO.
• Non-constituent coordination: type-raising + composition make "John likes" a constituent (S/NP), and generalized conjunction delivers the conjunctive interpretation (modeled on the book's "Anna married, and I detest, Manny").
• Gapping: [Ros70]'s word-order/gapping-direction generalization, recovered from the type-raising directions a language's verb categories license.
• Cross-serial dependencies: Dutch verb clusters ([BKPZ82]) with cross-serial NP-verb bindings, via the book's leftward argument categories and forward crossed composition.
• Verb clusters and quantifier scope (§6.8): verb-raising orders are scope-ambiguous, verb-projection-raising orders surface-only; predictions are read off the derivations' structure (Derivation.HasComp) and checked against the §6.8 judgments in Linglib.Data.Examples.Steedman2000 ([Bay96], [Kay98], [HvR86], [Hae92] are credited per example in the JSON).

Word order

Slash direction encodes word order: TV = (S\NP)/NP looks right for the object NP first, then the resulting S\NP looks left for the subject, enforcing SVO.

def Steedman2000.mary_eats_pizza : CCG.Derivation CCG.Atom CCG.S

Equations

• Steedman2000.mary_eats_pizza = (CCG.Derivation.lex "Mary" CCG.NP).bapp ((CCG.Derivation.lex "eats" CCG.TV).fapp (CCG.Derivation.lex "pizza" CCG.NP))

def Steedman2000.he_sees_her : CCG.Derivation CCG.Atom CCG.S

Equations

• Steedman2000.he_sees_her = (CCG.Derivation.lex "he" CCG.NP).bapp ((CCG.Derivation.lex "sees" CCG.TV).fapp (CCG.Derivation.lex "her" CCG.NP))

def Steedman2000.the_cat_eats_pizza : CCG.Derivation CCG.Atom CCG.S

Equations

• Steedman2000.the_cat_eats_pizza = ((CCG.Derivation.lex "the" CCG.Det).fapp (CCG.Derivation.lex "cat" CCG.N)).bapp ((CCG.Derivation.lex "eats" CCG.TV).fapp (CCG.Derivation.lex "pizza" CCG.NP))

def Steedman2000.john_sleeps : CCG.Derivation CCG.Atom CCG.S

Equations

• Steedman2000.john_sleeps = (CCG.Derivation.lex "John" CCG.NP).bapp (CCG.Derivation.lex "sleeps" CCG.IV)

def Steedman2000.john_sees_mary : CCG.Derivation CCG.Atom CCG.S

Equations

• Steedman2000.john_sees_mary = (CCG.Derivation.lex "John" CCG.NP).bapp ((CCG.Derivation.lex "sees" CCG.TV).fapp (CCG.Derivation.lex "Mary" CCG.NP))

Non-constituent coordination

def Steedman2000.john_tr : CCG.Derivation CCG.Atom (CCG.S.rslash CCG.Modality.dot (CCG.S.lslash CCG.Modality.dot CCG.NP))

The type-raised subject "John", S/(S\NP) — a lexical leaf, since type-raising is morpholexical in the modern theory ([Ste19]; the book's syntactic >T yields the same category).

Equations

• Steedman2000.john_tr = CCG.Derivation.lex "John" (CCG.S.rslash CCG.Modality.dot (CCG.S.lslash CCG.Modality.dot CCG.NP))

def Steedman2000.john_likes : CCG.Derivation CCG.Atom (CCG.S.rslash CCG.Modality.dot CCG.NP)

"John likes": the type-raised subject composed with the transitive verb — a constituent of category S/NP.

Equations

• Steedman2000.john_likes = CCG.Derivation.fcomp Steedman2000.john_likes._proof_1 Steedman2000.john_tr (CCG.Derivation.lex "likes" CCG.TV)

def Steedman2000.mary_tr : CCG.Derivation CCG.Atom (CCG.S.rslash CCG.Modality.dot (CCG.S.lslash CCG.Modality.dot CCG.NP))

Equations

• Steedman2000.mary_tr = CCG.Derivation.lex "Mary" (CCG.S.rslash CCG.Modality.dot (CCG.S.lslash CCG.Modality.dot CCG.NP))

def Steedman2000.mary_hates : CCG.Derivation CCG.Atom (CCG.S.rslash CCG.Modality.dot CCG.NP)

Equations

• Steedman2000.mary_hates = CCG.Derivation.fcomp Steedman2000.john_likes._proof_1 Steedman2000.mary_tr (CCG.Derivation.lex "hates" CCG.TV)

def Steedman2000.conj (c : CCG.Cat CCG.Atom) : CCG.Cat CCG.Atom

The lexical conjunction category coordinating constituents of category c: (X \⋆ X) /⋆ X, whose star slashes confine it to application ([Ste19]).

Equations

• Steedman2000.conj c = (c.lslash CCG.Modality.star c).rslash CCG.Modality.star c

def Steedman2000.john_likes_and_mary_hates : CCG.Derivation CCG.Atom (CCG.S.rslash CCG.Modality.dot CCG.NP)

"John likes and Mary hates": coordination of two S/NP constituents via the lexical conjunction — "and" is an ordinary leaf, not a rule.

Equations

• Steedman2000.john_likes_and_mary_hates = Steedman2000.john_likes.bapp ((CCG.Derivation.lex "and" (Steedman2000.conj (CCG.S.rslash CCG.Modality.dot CCG.NP))).fapp Steedman2000.mary_hates)

def Steedman2000.john_likes_and_mary_hates_beans : CCG.Derivation CCG.Atom CCG.S

Equations

• Steedman2000.john_likes_and_mary_hates_beans = Steedman2000.john_likes_and_mary_hates.fapp (CCG.Derivation.lex "beans" CCG.NP)

theorem Steedman2000.john_likes_and_mary_hates_beans_yield : john_likes_and_mary_hates_beans.yield = ["John", "likes", "and", "Mary", "hates", "beans"]

The derivation spells out the full surface string, coordinator included.

def Steedman2000.john_sleeps_and_mary_sleeps : CCG.Derivation CCG.Atom CCG.S

Equations

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

theorem Steedman2000.opCount_standardCoord_lt_nonConstituentCoord : john_sleeps_and_mary_sleeps.opCount < john_likes_and_mary_hates_beans.opCount

Non-constituent coordination requires more combinatory operations than standard coordination. Reading operation count as processing difficulty is this formalization's linking hypothesis, not a claim of [Ste00a].

theorem Steedman2000.opCount_simple_lt_standardCoord : john_sleeps.opCount < john_sleeps_and_mary_sleeps.opCount

def Steedman2000.toySemLexicon : CCG.SemLexicon Semantics.Montague.ToyEntity Unit

Toy semantic lexicon over the toy English fragment ("likes"/"hates" reuse sees_sem as placeholder denotations).

Equations

• One or more equations did not get rendered due to their size.
• Steedman2000.toySemLexicon "John" (CCG.Cat.atom CCG.Atom.NP) = some Semantics.Montague.ToyEntity.john
• Steedman2000.toySemLexicon "Mary" (CCG.Cat.atom CCG.Atom.NP) = some Semantics.Montague.ToyEntity.mary
• Steedman2000.toySemLexicon "beans" (CCG.Cat.atom CCG.Atom.NP) = some Semantics.Montague.ToyEntity.pizza
• Steedman2000.toySemLexicon "John" ((CCG.Cat.atom CCG.Atom.S).rslash a ((CCG.Cat.atom CCG.Atom.S).lslash a_1 (CCG.Cat.atom CCG.Atom.NP))) = some (Combinator.T Semantics.Montague.ToyEntity.john)
• Steedman2000.toySemLexicon "Mary" ((CCG.Cat.atom CCG.Atom.S).rslash a ((CCG.Cat.atom CCG.Atom.S).lslash a_1 (CCG.Cat.atom CCG.Atom.NP))) = some (Combinator.T Semantics.Montague.ToyEntity.mary)
• Steedman2000.toySemLexicon "sleeps" ((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.sleeps_sem
• Steedman2000.toySemLexicon "laughs" ((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.laughs_sem
• Steedman2000.toySemLexicon "sees" (((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)).rslash a_1 (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.sees_sem
• Steedman2000.toySemLexicon "eats" (((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)).rslash a_1 (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.eats_sem
• Steedman2000.toySemLexicon "likes" (((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)).rslash a_1 (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.sees_sem
• Steedman2000.toySemLexicon "hates" (((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)).rslash a_1 (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.sees_sem
• Steedman2000.toySemLexicon word cat = none

theorem Steedman2000.interp_john_sleeps : CCG.Derivation.interp toySemLexicon john_sleeps = some True

theorem Steedman2000.interp_john_sees_mary : CCG.Derivation.interp toySemLexicon john_sees_mary = some True

def Steedman2000.john_sees_mary_via_tr : CCG.Derivation CCG.Atom CCG.S

"John sees Mary" with a type-raised subject: the raised subject john_tr : S/(S\NP) uses forward application, and the derivation produces the same truth value as the canonical one.

Equations

• Steedman2000.john_sees_mary_via_tr = Steedman2000.john_tr.fapp ((CCG.Derivation.lex "sees" CCG.TV).fapp (CCG.Derivation.lex "Mary" CCG.NP))

theorem Steedman2000.interp_john_sees_mary_via_tr : CCG.Derivation.interp toySemLexicon john_sees_mary_via_tr = some True

def Steedman2000.coordMeaningAt (e : Semantics.Montague.ToyEntity) : Option Prop

The predicate "John likes and Mary hates" (category S/NP) evaluated at an entity.

Equations

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

def Steedman2000.pointwiseConjAt (e : Semantics.Montague.ToyEntity) : Option Prop

The pointwise conjunction of "John likes" and "Mary hates" at an entity.

Equations

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

theorem Steedman2000.coordMeaningAt_eq_pointwiseConjAt (e : Semantics.Montague.ToyEntity) : coordMeaningAt e = pointwiseConjAt e

Generalized conjunction delivers the conjunctive interpretation: ⟦John likes and Mary hates⟧(e) = ⟦John likes⟧(e) ∧ ⟦Mary hates⟧(e).

theorem Steedman2000.interp_john_likes_and_mary_hates_beans : CCG.Derivation.interp toySemLexicon john_likes_and_mary_hates_beans = some (Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyEntity.pizza Semantics.Montague.ToyEntity.john ∧ Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyEntity.pizza Semantics.Montague.ToyEntity.mary)

The truth conditions of "John likes and Mary hates beans" are the conjunction of the two predications (in the toy model, likes = hates = sees).

def Steedman2000.john_likes_beans_and_mary_hates_beans : CCG.Derivation CCG.Atom CCG.S

The spelled-out paraphrase "John likes beans and Mary hates beans".

Equations

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

theorem Steedman2000.nonConstituentCoord_eq_spelledOut : CCG.Derivation.interp toySemLexicon john_likes_and_mary_hates_beans = CCG.Derivation.interp toySemLexicon john_likes_beans_and_mary_hates_beans

The non-constituent coordination and its spelled-out paraphrase receive the same truth conditions — the book's claim that the composed derivation yields the same predicate-argument structure as the canonical one.

The coordinator's role is truth-conditionally load-bearing

interp reads the coordinator's role off the .coord node — it no longer hardcodes conjunction — so which coordinator a derivation uses is part of its truth conditions. Using the actual English fragment coordinators, conjoining a true sentence p and a false sentence q with and_ (role = .j) gives p ∧ q (false), while or_ (role = .disj) gives p ∨ q (true). They differ, so the marking's role field is load-bearing — flipping English.Coordination.and_.role to .disj would break the theorem below, rather than no theorem depending on it.

theorem Steedman2000.coord_role_load_bearing : CCG.Derivation.interp Steedman2000.pqLex✝ (Steedman2000.dp✝.bapp ((CCG.Derivation.lex "and" (conj CCG.S)).fapp Steedman2000.dq✝)) ≠ CCG.Derivation.interp Steedman2000.pqLex✝ (Steedman2000.dp✝.bapp ((CCG.Derivation.lex "or" (conj CCG.S)).fapp Steedman2000.dq✝))

The coordinator's role flips the truth conditions: English and_ yields p ∧ q, or_ yields p ∨ q, and these differ at p = ⊤, q = ⊥. Flipping a fragment coordinator's role collapses the inequality, so the role marking is not decorative.

Gapping

[Ros70]'s generalization — gapping direction tracks word order — which [Ste00a] derives from the Principles of Adjacency, Consistency, and Inheritance together with the order-preserving constraint on type-raising. The constituency half is derived below — the gapped conjunct is a typechecked derivation (gappedConjunct); deriving the predictedGappingPattern table itself from per-order verb categories is TODO. (Dutch licensing both directions is mixed_allows_both.)

def Steedman2000.gappedConjunct : CCG.Derivation CCG.Atom (CCG.S.lslash CCG.Modality.dot ((CCG.S.rslash CCG.Modality.dot CCG.NP).rslash CCG.Modality.dot CCG.NP))

The gapped conjunct "Warren, potatoes" is a constituent ([Ste00a] ch. 7): backward type-raising both remnants and backward-composing them yields S\((S/NP)/NP) — a leftward-looking function over VSO-style transitive verbs, which is why forward gapping leaves the verb to the left. Deriving it is typechecking.

Equations

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

theorem Steedman2000.gappedConjunct_yield : gappedConjunct.yield = ["Warren", "potatoes"]

def Steedman2000.backwardGappedConjunct : CCG.Derivation CCG.Atom (CCG.S.rslash CCG.Modality.dot ((CCG.S.lslash CCG.Modality.dot CCG.NP).lslash CCG.Modality.dot CCG.NP))

The mirror cluster for backward gapping (Japanese "Ken-ga Naomi-o"): forward type-raising and forward composition yield S/((S\NP)\NP), a rightward-looking function over SOV transitive verbs — the verb must follow.

Equations

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

theorem Steedman2000.backwardGappedConjunct_yield : backwardGappedConjunct.yield = ["Ken-ga", "Naomi-o"]

def Steedman2000.strippedConjunct : CCG.Derivation CCG.Atom (CCG.S.lslash CCG.Modality.dot (CCG.S.rslash CCG.Modality.dot CCG.NP))

Stripping ("Dexter ran away, and Warren (too)") is the single-remnant case: one backward-raised subject, S\(S/NP).

Equations

• Steedman2000.strippedConjunct = CCG.Derivation.lex "Warren" (CCG.S.lslash CCG.Modality.dot (CCG.S.rslash CCG.Modality.dot CCG.NP))

inductive Steedman2000.WordOrder : Type

Basic word order of a transitive clause (S = subject, V = verb, O = object).

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

@[instance_reducible]

instance Steedman2000.instDecidableEqWordOrder : DecidableEq WordOrder

Equations

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

def Steedman2000.instReprWordOrder.repr : WordOrder → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Steedman2000.instReprWordOrder : Repr WordOrder

Equations

• Steedman2000.instReprWordOrder = { reprPrec := Steedman2000.instReprWordOrder.repr }

inductive Steedman2000.GappingDirection : Type

Direction of gapping in a coordinate structure: forward gapping leaves the gap in the non-initial conjunct ("Dexter ate bread, and Warren, potatoes"); backward gapping leaves it in the non-final conjunct (Japanese "Ken-ga Naomi-o, Erika-ga Sara-o tazuneta").

• forward : GappingDirection
• backward : GappingDirection

@[instance_reducible]

instance Steedman2000.instDecidableEqGappingDirection : DecidableEq GappingDirection

Equations

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

@[instance_reducible]

instance Steedman2000.instReprGappingDirection : Repr GappingDirection

Equations

• Steedman2000.instReprGappingDirection = { reprPrec := Steedman2000.instReprGappingDirection.repr }

def Steedman2000.instReprGappingDirection.repr : GappingDirection → ℕ → Std.Format

Equations

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

structure Steedman2000.GappingPattern : Type

The gapping directions a language allows.

• allowsForward : Prop
• allowsBackward : Prop
• decAllowsForward : Decidable self.allowsForward
• decAllowsBackward : Decidable self.allowsBackward

def Steedman2000.GappingPattern.forwardOnly : GappingPattern

Equations

• Steedman2000.GappingPattern.forwardOnly = { allowsForward := True, allowsBackward := False, decAllowsForward := instDecidableTrue, decAllowsBackward := instDecidableFalse }

def Steedman2000.GappingPattern.backwardOnly : GappingPattern

Equations

• Steedman2000.GappingPattern.backwardOnly = { allowsForward := False, allowsBackward := True, decAllowsForward := instDecidableFalse, decAllowsBackward := instDecidableTrue }

def Steedman2000.GappingPattern.both : GappingPattern

Equations

• Steedman2000.GappingPattern.both = { allowsForward := True, allowsBackward := True, decAllowsForward := instDecidableTrue, decAllowsBackward := instDecidableTrue }

def Steedman2000.GappingPattern.neither : GappingPattern

Equations

• Steedman2000.GappingPattern.neither = { allowsForward := False, allowsBackward := False, decAllowsForward := instDecidableFalse, decAllowsBackward := instDecidableFalse }

def Steedman2000.rossOriginal : WordOrder → GappingPattern

[Ros70]'s generalization: verb-final orders gap backward, the rest gap forward.

Equations

• Steedman2000.rossOriginal Steedman2000.WordOrder.SOV = Steedman2000.GappingPattern.backwardOnly
• Steedman2000.rossOriginal Steedman2000.WordOrder.VSO = Steedman2000.GappingPattern.forwardOnly
• Steedman2000.rossOriginal Steedman2000.WordOrder.SVO = Steedman2000.GappingPattern.forwardOnly
• Steedman2000.rossOriginal Steedman2000.WordOrder.VOS = Steedman2000.GappingPattern.forwardOnly
• Steedman2000.rossOriginal Steedman2000.WordOrder.OVS = Steedman2000.GappingPattern.backwardOnly
• Steedman2000.rossOriginal Steedman2000.WordOrder.OSV = Steedman2000.GappingPattern.backwardOnly

def Steedman2000.HasRightwardVerbs : WordOrder → Prop

The order's transitive verbs seek (at least one of) their arguments rightward.

Equations

• Steedman2000.HasRightwardVerbs Steedman2000.WordOrder.VSO = True
• Steedman2000.HasRightwardVerbs Steedman2000.WordOrder.SVO = True
• Steedman2000.HasRightwardVerbs Steedman2000.WordOrder.VOS = True
• Steedman2000.HasRightwardVerbs x✝ = False

@[instance_reducible]

instance Steedman2000.instDecidablePredWordOrderHasRightwardVerbs : DecidablePred HasRightwardVerbs

Equations

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

def Steedman2000.HasLeftwardVerbs : WordOrder → Prop

The order's transitive verbs seek their arguments leftward.

Equations

• Steedman2000.HasLeftwardVerbs Steedman2000.WordOrder.SOV = True
• Steedman2000.HasLeftwardVerbs Steedman2000.WordOrder.OVS = True
• Steedman2000.HasLeftwardVerbs Steedman2000.WordOrder.OSV = True
• Steedman2000.HasLeftwardVerbs x✝ = False

@[instance_reducible]

instance Steedman2000.instDecidablePredWordOrderHasLeftwardVerbs : DecidablePred HasLeftwardVerbs

Equations

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

def Steedman2000.predictedGappingPattern (order : WordOrder) : GappingPattern

The gapping directions CCG predicts for a word order: forward gapping needs a leftward-looking gapped conjunct, available through backward type-raising over rightward-seeking verbs (T\(T/NP)); backward gapping needs forward raising over leftward-seeking verbs (T/(T\NP)).

Equations

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

theorem Steedman2000.predictedGappingPattern_iff_rossOriginal (order : WordOrder) : ((predictedGappingPattern order).allowsForward ↔ (rossOriginal order).allowsForward) ∧ ((predictedGappingPattern order).allowsBackward ↔ (rossOriginal order).allowsBackward)

The CCG-predicted pattern coincides with Ross's generalization.

theorem Steedman2000.predictedGappingPattern_svo_iff_vso : ((predictedGappingPattern WordOrder.SVO).allowsForward ↔ (predictedGappingPattern WordOrder.VSO).allowsForward) ∧ ((predictedGappingPattern WordOrder.SVO).allowsBackward ↔ (predictedGappingPattern WordOrder.VSO).allowsBackward)

SVO patterns with VSO: both license forward but not backward gapping.

theorem Steedman2000.no_backward_gapping_in_english : ¬HasLeftwardVerbs WordOrder.SVO

English (SVO) has no leftward-looking transitive verb category, so the rightward-looking gapped conjunct a backward gap needs cannot be built: "*Warren, potatoes and Dexter ate bread" (instantiating Steedman's *SO and SVO schema; the book's attested forward counterpart is "Dexter ate bread and Warren, potatoes").

structure Steedman2000.ClauseOrderProfile : Type

Main- vs subordinate-clause word order, for languages whose two clause types diverge.

• mainClause : WordOrder
• subClause : WordOrder

@[instance_reducible]

instance Steedman2000.instReprClauseOrderProfile : Repr ClauseOrderProfile

Equations

• Steedman2000.instReprClauseOrderProfile = { reprPrec := Steedman2000.instReprClauseOrderProfile.repr }

def Steedman2000.instReprClauseOrderProfile.repr : ClauseOrderProfile → ℕ → Std.Format

Equations

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

def Steedman2000.rossRevised (profile : ClauseOrderProfile) : GappingPattern

Steedman's revision of [Ros70]: gapping availability tracks the lexical availability of verb categories, not a single "underlying" word order — forward gapping needs rightward-combining verbs, backward gapping leftward-combining verbs in either clause type.

Equations

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

def Steedman2000.dutch : ClauseOrderProfile

Dutch: SVO main clauses, SOV subordinate clauses. The mixed profile licenses both gapping directions — forward in main clauses ("Wil jij een ijsje en Marietje limonade?"), backward in subordinate clauses ("...dat Jan Syntactic Structures en Piet Aspects gelezen heeft").

Equations

• Steedman2000.dutch = { mainClause := Steedman2000.WordOrder.SVO, subClause := Steedman2000.WordOrder.SOV }

theorem Steedman2000.mixed_allows_both : (rossRevised dutch).allowsForward ∧ (rossRevised dutch).allowsBackward

A mixed-order language like Dutch licenses both gapping directions.

inductive Steedman2000.EllipsisType : Type

Steedman's taxonomy of elliptical constructions.

• gapping : EllipsisType

  "Dexter ate bread, and Warren, potatoes"

• stripping : EllipsisType

  "Dexter ran away, and Warren (too)"

• vpEllipsis : EllipsisType

  "Dexter ate bread, and Warren did too"

• sluicing : EllipsisType

  "Dexter did something, but I don't know what"

@[instance_reducible]

instance Steedman2000.instDecidableEqEllipsisType : DecidableEq EllipsisType

Equations

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

def Steedman2000.instReprEllipsisType.repr : EllipsisType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Steedman2000.instReprEllipsisType : Repr EllipsisType

Equations

• Steedman2000.instReprEllipsisType = { reprPrec := Steedman2000.instReprEllipsisType.repr }

def Steedman2000.isSyntacticallyMediated : EllipsisType → Prop

Gapping and stripping are syntactically mediated via CCG; VP ellipsis and sluicing are purely anaphoric.

Equations

• Steedman2000.isSyntacticallyMediated Steedman2000.EllipsisType.gapping = True
• Steedman2000.isSyntacticallyMediated Steedman2000.EllipsisType.stripping = True
• Steedman2000.isSyntacticallyMediated Steedman2000.EllipsisType.vpEllipsis = False
• Steedman2000.isSyntacticallyMediated Steedman2000.EllipsisType.sluicing = False

@[instance_reducible]

instance Steedman2000.instDecidablePredEllipsisTypeIsSyntacticallyMediated : DecidablePred isSyntacticallyMediated

Equations

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

def Steedman2000.HasWordOrderConstraints : EllipsisType → Prop

Only the syntactically mediated ellipsis types exhibit word-order constraints; VP ellipsis and sluicing pattern alike across languages.

Equations

• Steedman2000.HasWordOrderConstraints Steedman2000.EllipsisType.gapping = True
• Steedman2000.HasWordOrderConstraints Steedman2000.EllipsisType.stripping = True
• Steedman2000.HasWordOrderConstraints Steedman2000.EllipsisType.vpEllipsis = False
• Steedman2000.HasWordOrderConstraints Steedman2000.EllipsisType.sluicing = False

@[instance_reducible]

instance Steedman2000.instDecidablePredEllipsisTypeHasWordOrderConstraints : DecidablePred HasWordOrderConstraints

Equations

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

@[instance_reducible]

instance Steedman2000.instHasDepthEllipsisType : Anaphor.HasDepth EllipsisType

All four of Steedman's elliptical constructions are surface anaphora in Hankamer & Sag's sense ([HS76]): each deletes internal structure under identity with a linguistic antecedent. Steedman's taxonomy contains no deep anaphor (no do so-type pro-form), so the depth axis is constant .surface over it.

Equations

• Steedman2000.instHasDepthEllipsisType = { depth := fun (x : Steedman2000.EllipsisType) => Anaphor.Depth.surface }

theorem Steedman2000.surface_not_syntacticallyMediated : Anaphor.HasDepth.IsSurface EllipsisType.vpEllipsis ∧ ¬isSyntacticallyMediated EllipsisType.vpEllipsis

Cross-framework non-alignment. Steedman's CCG cut isSyntacticallyMediated (gapping/stripping derived by category composition; VP-ellipsis/sluicing handled anaphorically) is not Hankamer & Sag's deep/surface cut. VP-ellipsis is the paradigm surface anaphor ([HS76]; Landau's own surface baseline in [Lan26]) yet CCG treats it as non-mediated — so the two frameworks partition the very same constructions differently.

Cross-serial dependencies

Dutch verb clusters ([BKPZ82]) with cross-serial NP-verb bindings, over a target-restricted grammar (dutchGrammar: every rule fires at primary target S). Two constructions are given as Derives facts — the relation carries category and string at once. The verb-raising derivations (rightward /NP slots, harmonic B/B²) encode the cross-serial binding pattern at a non-Dutch string (see jan_zag_zwemmen_piet_derives); the surface-faithful derivations (leftward \NP slots, forward crossed composition, following the book's own Dutch fragment — ch. 6; appendix summary) derive the attested "Jan Piet (Marie) zag (helpen) zwemmen".

Categories for Dutch verb clusters

def Steedman2000.VP : CCG.Cat CCG.Atom

Verb phrase (infinitival).

Equations

• Steedman2000.VP = CCG.S.lslash CCG.Modality.dot CCG.NP

def Steedman2000.PercV : CCG.Cat CCG.Atom

Perception verb: (S\NP)/(S\NP) (e.g. "zag" = saw).

Equations

• Steedman2000.PercV = (CCG.S.lslash CCG.Modality.dot CCG.NP).rslash CCG.Modality.dot Steedman2000.VP

def Steedman2000.InfSubj : CCG.Cat CCG.Atom

Infinitival verb needing its (raised) subject: (S\NP)/NP. In Dutch verb-raising the infinitive's subject surfaces in an object-like position, picked up via composition.

Equations

• Steedman2000.InfSubj = (CCG.S.lslash CCG.Modality.dot CCG.NP).rslash CCG.Modality.dot CCG.NP

def Steedman2000.ControlVR : CCG.Cat CCG.Atom

Verb-raising control verb ((S\NP)/NP)/(S\NP): each restructuring verb provides an extra /NP slot for its own raised subject, in addition to its VP complement. This is what threads multiple argument slots through a 3+-verb cluster:

• zwemmen : (S\NP)/NP — base: needs subject
• helpen : ((S\NP)/NP)/(S\NP) — VR: needs complement, passes an /NP
• zag : (S\NP)/(S\NP) — matrix: standard perception verb

Equations

• Steedman2000.ControlVR = ((CCG.S.lslash CCG.Modality.dot CCG.NP).rslash CCG.Modality.dot CCG.NP).rslash CCG.Modality.dot (CCG.S.lslash CCG.Modality.dot CCG.NP)

def Steedman2000.PercVSub : CCG.Cat CCG.Atom

Subordinate-clause perception verb ((S\NP)\NP)/VP: infinitival complement to the right, object and subject NPs to the left (book: zag := ((S₊SUB\NP)\NP)/VP₋SUB; the toy Cat drops the features). Sub = subordinate-clause head — contrast InfSubj, whose /NP is a raised-subject slot.

Equations

• Steedman2000.PercVSub = ((CCG.S.lslash CCG.Modality.dot CCG.NP).lslash CCG.Modality.dot CCG.NP).rslash CCG.Modality.dot Steedman2000.VP

def Steedman2000.InfHeadSub : CCG.Cat CCG.Atom

Infinitival head with a raised object, (VP\NP)/VP (book: zien := (VP\NP)/VP₋SUB).

Equations

• Steedman2000.InfHeadSub = (Steedman2000.VP.lslash CCG.Modality.dot CCG.NP).rslash CCG.Modality.dot Steedman2000.VP

def Steedman2000.dutchGrammar : CCG.Grammar CCG.Atom

The Dutch fragment as a target-restricted grammar: the lexical entries the derivations below draw on, target and start S, degree bound 2.

Equations

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

Lexical entries, as derivability facts

theorem Steedman2000.jan_derives : dutchGrammar.Derives CCG.NP ["Jan"]

theorem Steedman2000.piet_derives : dutchGrammar.Derives CCG.NP ["Piet"]

theorem Steedman2000.marie_derives : dutchGrammar.Derives CCG.NP ["Marie"]

theorem Steedman2000.zag_vr_derives : dutchGrammar.Derives PercV ["zag"]

theorem Steedman2000.zwemmen_vr_derives : dutchGrammar.Derives InfSubj ["zwemmen"]

theorem Steedman2000.helpen_vr_derives : dutchGrammar.Derives ControlVR ["helpen"]

theorem Steedman2000.zag_sub_derives : dutchGrammar.Derives PercVSub ["zag"]

theorem Steedman2000.helpen_sub_derives : dutchGrammar.Derives InfHeadSub ["helpen"]

theorem Steedman2000.zwemmen_bare_derives : dutchGrammar.Derives VP ["zwemmen"]

Verb-raising derivations

B/B² thread the raised argument slots through the cluster — the cross-serial binding pattern — but the rightward /NP slots spell the arguments out after the cluster, so the derived strings do not match Dutch surface order.

theorem Steedman2000.verb_cluster_derives : dutchGrammar.Derives (((CCG.S.lslash CCG.Modality.dot CCG.NP).rslash CCG.Modality.dot CCG.NP).rslash CCG.Modality.dot CCG.NP) ["zag", "helpen", "zwemmen"]

zag >B² (helpen >B zwemmen): the cluster is a 3-place predicate ((S\NP)/NP)/NP wanting Jan (\NP), Piet (/NP) and Marie (/NP).

theorem Steedman2000.jan_zag_zwemmen_piet_derives : dutchGrammar.Derives CCG.S ["Jan", "zag", "zwemmen", "Piet"]

The 2-verb verb-raising derivation derives S — at the string "Jan zag zwemmen Piet", which is not Dutch ("Jan Piet zag zwemmen"): the verb-raising categories capture the binding but not the linear order. The surface-faithful derivations below get both.

Surface-faithful derivations (leftward argument categories)

[Ste00a]'s own analysis (ch. 6; appendix summary of the Dutch fragment) gives subordinate-clause cluster verbs leftward NP slots and composes the cluster by forward crossed composition, so the NPs precede the whole cluster and the derived strings are the attested "Jan Piet (Marie) zag (helpen) zwemmen".

theorem Steedman2000.crossed_cluster_derives : dutchGrammar.Derives (((CCG.S.lslash CCG.Modality.dot CCG.NP).lslash CCG.Modality.dot CCG.NP).lslash CCG.Modality.dot CCG.NP) ["zag", "helpen", "zwemmen"]

The crossed cluster zag >B× (helpen zwemmen) is a leftward-seeking 3-place predicate.

theorem Steedman2000.two_np_sub_derives : dutchGrammar.Derives CCG.S ["Jan", "Piet", "zag", "zwemmen"]

"(dat) Jan Piet zag zwemmen": zag applies to bare zwemmen and the NPs attach leftward — the 2-verb cluster needs no composition, and the string is the attested order (contrast jan_zag_zwemmen_piet_derives).

theorem Steedman2000.three_np_sub_derives : dutchGrammar.Derives CCG.S ["Jan", "Piet", "Marie", "zag", "helpen", "zwemmen"]

"(dat) Jan Piet Marie zag helpen zwemmen": the three NPs attach leftward to the crossed cluster — Marie to helpen's slot, Piet to zag's object slot, Jan as subject: the cross-serial binding falls out of the category threading, in the attested word order.

Binding annotations

structure Steedman2000.AnnotatedDerivation : Type

A derived Dutch string annotated with which NP binds to which verb; carrying the derivability fact ties the words to the grammar. TODO: compute binding from a derivation's composition structure instead of annotating it by hand.

• n : ℕ

  Number of NP-verb pairs

• words : List String

  Surface words

• binding : Features.VerbClusterBinding self.n

  The NP-verb binding permutation

• derives : dutchGrammar.Derives CCG.S self.words

  The grammar derives the words at S.

def Steedman2000.dutch_jan_piet_zag_zwemmen : AnnotatedDerivation

"Jan Piet zag zwemmen" with cross-serial bindings: Jan is the subject of "zag", Piet the argument bound into the cluster.

Equations

• Steedman2000.dutch_jan_piet_zag_zwemmen = { n := 2, words := ["Jan", "Piet", "zag", "zwemmen"], binding := Features.VerbClusterBinding.identity 2, derives := Steedman2000.two_np_sub_derives }

def Steedman2000.dutch_jan_piet_marie_zag_helpen_zwemmen : AnnotatedDerivation

"Jan Piet Marie zag helpen zwemmen", the cross-serial binding pattern in the attested word order.

Equations

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

theorem Steedman2000.dutch_jan_piet_zag_zwemmen_binding : dutch_jan_piet_zag_zwemmen.binding = BresnanEtAl1982.dutch_2np_2v.binding

The annotated binding agrees with the empirical datum.

theorem Steedman2000.dutch_jan_piet_marie_zag_helpen_zwemmen_binding : dutch_jan_piet_marie_zag_helpen_zwemmen.binding = BresnanEtAl1982.dutch_3np_3v.binding

Verb clusters and quantifier scope (§6.8)

Scope tracks word order: in the verb-raising order the cluster forms by composition, so a quantified argument combines with a function containing the tensed verb and can take scope over it; in the verb-projection-raising order it combines with the embedded verb alone. The derivations below are intrinsically typed Derivation trees: the verb-raising cluster forms by forward crossed composition (.fcompx), the verb-projection-raising order by plain application — the composed-cluster vs. applied-cluster contrast driving the account. (The toy Cat still drops the book's features, e.g. the VP₋SUB restriction on >B×.)

inductive Steedman2000.VerbOrder : Type

Word order in a West Germanic verb cluster ([Ste00a] §6.8).

• verbRaising : VerbOrder

  Object precedes the whole verb cluster: NP … V_emb V_matrix.

• verbProjectionRaising : VerbOrder

  Object follows the matrix verb: V_matrix … NP V_emb.

@[instance_reducible]

instance Steedman2000.instDecidableEqVerbOrder : DecidableEq VerbOrder

Equations

• Steedman2000.instDecidableEqVerbOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Steedman2000.instReprVerbOrder.repr : VerbOrder → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Steedman2000.instReprVerbOrder : Repr VerbOrder

Equations

• Steedman2000.instReprVerbOrder = { reprPrec := Steedman2000.instReprVerbOrder.repr }

@[instance_reducible]

instance Steedman2000.instInhabitedVerbOrder : Inhabited VerbOrder

Equations

• Steedman2000.instInhabitedVerbOrder = { default := Steedman2000.instInhabitedVerbOrder.default }

def Steedman2000.verbRaisingDeriv : CCG.Derivation CCG.Atom CCG.IV

Verb-raising order, Dutch (99a): the cluster probeert te zingen forms by crossed composition before taking the object to its left.

Equations

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

def Steedman2000.verbProjectionRaisingDeriv : CCG.Derivation CCG.Atom CCG.IV

Verb-projection-raising order, Dutch (99b): the matrix verb applies to an already-saturated embedded VP, so the quantified object never combines with a function containing the tensed verb.

Equations

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

def Steedman2000.schematicDeriv : VerbOrder → CCG.Derivation CCG.Atom CCG.IV

The CCG derivation shape each verb order forces.

Equations

• Steedman2000.schematicDeriv Steedman2000.VerbOrder.verbRaising = Steedman2000.verbRaisingDeriv
• Steedman2000.schematicDeriv Steedman2000.VerbOrder.verbProjectionRaising = Steedman2000.verbProjectionRaisingDeriv

theorem Steedman2000.verbRaisingDeriv_hasComp : verbRaisingDeriv.HasComp

theorem Steedman2000.verbProjectionRaisingDeriv_applicationOnly : ¬verbProjectionRaisingDeriv.HasComp

def Steedman2000.predictedAvailability (vo : VerbOrder) : ScopeTheory.BinaryScopeAvailability

Scope availability as CCG predicts it — the account's linking hypothesis: a cluster built with composition or type-raising is scope-ambiguous, an application-only cluster surface-only. [Ste00a] notes this overgenerates as stated (§4.4 refines it).

Equations

• Steedman2000.predictedAvailability vo = if (Steedman2000.schematicDeriv vo).HasComp then ScopeTheory.BinaryScopeAvailability.ambiguous else ScopeTheory.BinaryScopeAvailability.surfaceOnly

def Steedman2000.wordOrderOf (ex : Data.Examples.LinguisticExample) : Option VerbOrder

Read the §6.8 word-order classification off an example's paperFeatures.

Equations

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

def Steedman2000.observedAvailability (ex : Data.Examples.LinguisticExample) : Option ScopeTheory.BinaryScopeAvailability

Observed scope availability: the judgment on the example's "inverse" reading (the "surface" reading is acceptable throughout §6.8).

Equations

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

def Steedman2000.scopeData : List (VerbOrder × ScopeTheory.BinaryScopeAvailability)

The §6.8 data as (word order, observed availability) pairs.

Equations

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

theorem Steedman2000.predictedAvailability_eq_observed (d : VerbOrder × ScopeTheory.BinaryScopeAvailability) : d ∈ scopeData → predictedAvailability d.1 = d.2

The CCG prediction matches every §6.8 judgment.

Intonation and information structure

The book's ch. 5 story: alternative derivations of one string are alternative information structures, disambiguated by tune. "(ANNA married)(MANNY)" carves the composed derivation into an L+H* LH% theme and an H* LL% rheme; prosodic phrases are tune-marked constituents, so only CCG constituents can be phrases (the Sense Unit Condition, [Sel84]; [Ste00a] ch. 2).

def Steedman2000.annaMannyAccents : CCG.Intonation.AccentAssignment

Accents for "(ANNA married)(MANNY)": theme accent on "Anna", rheme accent on "Manny", "married" unaccented.

Equations

• Steedman2000.annaMannyAccents "Anna" = Features.Prosody.PitchAccent.L_plus_H_star
• Steedman2000.annaMannyAccents "Manny" = Features.Prosody.PitchAccent.H_star
• Steedman2000.annaMannyAccents w = Features.Prosody.PitchAccent.null

def Steedman2000.anna_married : CCG.Derivation CCG.Atom (CCG.S.rslash CCG.Modality.dot CCG.NP)

"ANNA married": the composed theme constituent, category S/NP.

Equations

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

theorem Steedman2000.anna_married_theme : CCG.Derivation.infoFeature annaMannyAccents anna_married = some CCG.Intonation.InfoFeature.θ

The theme constituent projects θ: the theme accent on "Anna" unifies with unaccented "married".

theorem Steedman2000.manny_rheme : CCG.Derivation.infoFeature annaMannyAccents (CCG.Derivation.lex "Manny" CCG.NP) = some CCG.Intonation.InfoFeature.ρ

The rheme "MANNY" projects ρ.

theorem Steedman2000.theme_rheme_clash : CCG.Derivation.infoFeature annaMannyAccents (anna_married.fapp (CCG.Derivation.lex "Manny" CCG.NP)) = none

Folding the rheme into the theme's constituent clashes: with these accents the whole sentence projects no coherent single marking, so the tune forces the [Anna married][Manny] phrasing — intonation disambiguates the derivational ambiguity.

def Steedman2000.annaMannyUtterance : List CCG.Intonation.ProsodicPhrase

The utterance as two tune-marked phrases.

Equations

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

theorem Steedman2000.annaMannyUtterance_infoStructure : Option.map (fun (i : CCG.Intonation.InfoStructure CCG.Intonation.ProsodicPhrase) => (Option.map (fun (x : CCG.Intonation.ProsodicPhrase) => x.cat) i.theme, i.rheme.cat)) (CCG.Intonation.extractInfoStructure annaMannyUtterance) = some (some (CCG.S.rslash CCG.Modality.dot CCG.NP), CCG.NP)

The extracted information structure: the theme is the S/NP constituent "ANNA married", the rheme is "MANNY".

Truth-conditional pipeline

The complete CCG → Montague pipeline over the toy fragment: derivations interpreted compositionally, each checked against the toy model.

def Steedman2000.ccg_mary_sleeps : CCG.Derivation CCG.Atom CCG.S

"Mary sleeps" - backward application

Equations

• Steedman2000.ccg_mary_sleeps = (CCG.Derivation.lex "Mary" CCG.NP).bapp (CCG.Derivation.lex "sleeps" CCG.IV)

def Steedman2000.ccg_john_laughs : CCG.Derivation CCG.Atom CCG.S

"John laughs" - backward application

Equations

• Steedman2000.ccg_john_laughs = (CCG.Derivation.lex "John" CCG.NP).bapp (CCG.Derivation.lex "laughs" CCG.IV)

def Steedman2000.ccg_mary_laughs : CCG.Derivation CCG.Atom CCG.S

"Mary laughs" - backward application

Equations

• Steedman2000.ccg_mary_laughs = (CCG.Derivation.lex "Mary" CCG.NP).bapp (CCG.Derivation.lex "laughs" CCG.IV)

def Steedman2000.ccg_mary_sees_john : CCG.Derivation CCG.Atom CCG.S

"Mary sees John" - forward then backward application

Equations

• Steedman2000.ccg_mary_sees_john = (CCG.Derivation.lex "Mary" CCG.NP).bapp ((CCG.Derivation.lex "sees" CCG.TV).fapp (CCG.Derivation.lex "John" CCG.NP))

def Steedman2000.ccg_john_eats_pizza : CCG.Derivation CCG.Atom CCG.S

"John eats pizza" - forward then backward application

Equations

• Steedman2000.ccg_john_eats_pizza = (CCG.Derivation.lex "John" CCG.NP).bapp ((CCG.Derivation.lex "eats" CCG.TV).fapp (CCG.Derivation.lex "pizza" CCG.NP))

def Steedman2000.extendedLexicon : CCG.SemLexicon Semantics.Montague.ToyEntity Unit

Extended lexicon with all entities and predicates

Equations

• Steedman2000.extendedLexicon "John" (CCG.Cat.atom CCG.Atom.NP) = some Semantics.Montague.ToyEntity.john
• Steedman2000.extendedLexicon "Mary" (CCG.Cat.atom CCG.Atom.NP) = some Semantics.Montague.ToyEntity.mary
• Steedman2000.extendedLexicon "pizza" (CCG.Cat.atom CCG.Atom.NP) = some Semantics.Montague.ToyEntity.pizza
• Steedman2000.extendedLexicon "book" (CCG.Cat.atom CCG.Atom.NP) = some Semantics.Montague.ToyEntity.book
• Steedman2000.extendedLexicon "sleeps" ((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.sleeps_sem
• Steedman2000.extendedLexicon "laughs" ((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.laughs_sem
• Steedman2000.extendedLexicon "sees" (((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)).rslash a_1 (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.sees_sem
• Steedman2000.extendedLexicon "eats" (((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)).rslash a_1 (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.eats_sem
• Steedman2000.extendedLexicon "reads" (((CCG.Cat.atom CCG.Atom.S).lslash a (CCG.Cat.atom CCG.Atom.NP)).rslash a_1 (CCG.Cat.atom CCG.Atom.NP)) = some Semantics.Montague.ToyLexicon.reads_sem
• Steedman2000.extendedLexicon word cat = none

def Steedman2000.ccgMeaning (d : CCG.Derivation CCG.Atom CCG.S) : Option Prop

Get meaning (as Prop) from CCG derivation

Equations

• Steedman2000.ccgMeaning d = CCG.Derivation.interp Steedman2000.extendedLexicon d

theorem Steedman2000.ccg_predicts_john_sleeps : ccgMeaning john_sleeps = some True

CCG correctly predicts "John sleeps" is true

theorem Steedman2000.ccg_predicts_mary_sleeps : ccgMeaning ccg_mary_sleeps = some False

CCG correctly predicts "Mary sleeps" is false

theorem Steedman2000.ccg_predicts_john_laughs : ccgMeaning ccg_john_laughs = some True

CCG correctly predicts "John laughs" is true

theorem Steedman2000.ccg_predicts_mary_laughs : ccgMeaning ccg_mary_laughs = some True

CCG correctly predicts "Mary laughs" is true

theorem Steedman2000.ccg_predicts_john_sees_mary : ccgMeaning john_sees_mary = some True

CCG correctly predicts "John sees Mary" is true

theorem Steedman2000.ccg_predicts_mary_sees_john : ccgMeaning ccg_mary_sees_john = some True

CCG correctly predicts "Mary sees John" is true