Steedman (2000): The Syntactic Process

In Steedman's combinatory categorial grammar the slash directions of lexical categories fix word order, and composition and type-raising make strings such as a subject and a transitive verb into constituents. This file derives the book's analyses of non-constituent coordination, gapping, Dutch cross-serial dependencies, scope in verb clusters and intonational phrasing over the library's CCG, and interprets the derivations over a toy English model.

Main statements

• nonConstituentCoord_eq_spelledOut: "John sees and Mary eats pizza" has the truth conditions of its spelled-out paraphrase.
• gapping_acceptable_iff: Ross's generalization over the book's gapping examples. The raised arguments of a verb-final verb compose into a rightward-looking cluster and those of a verb-initial verb into a leftward-looking one, so verb-final clauses gap backward and the others forward, SVO clauses over the verb-initial verb the revealing rule exposes.
• inverse_acceptable_iff_available: an inverse scope reading is acceptable in the book's examples exactly when some derivation lets the quantified object combine with a constituent containing the tensed verb.
• theme_rheme_clash: a theme accent and a rheme accent do not unify, so the tune forces the phrasing "(ANNA married)(MANNY)".

Implementation notes

• Type-raising and coordination are lexical in the library's CCG, so the book's raising rules appear as raised entries and its coordination rule <Φ> as a conjunction of category (X\⋆X)/⋆X. A raised name denotes the Montague lift, and coordination at S/NP is Partee and Rooth's generalized conjunction.
• The toy categories drop the book's features (subordination, case, agreement), so Dutch crossed composition is restricted to VP complements rather than the book's VP_{-SUB}.
• The revealing rule (61) is a unary decomposition outside the binary derivations, so it enters only as the condition on the categories it reveals (RevealedResidue).
• The tunes follow Pierrehumbert's decomposition of an intonation phrase into pitch accent, phrase accent and boundary tone, which Beckman and Pierrehumbert supply (ipToTune).

References

• [Ste00a]
• [Ros70]
• [Bay96]
• [Kay98]
• [HvR86]
• [Hae92]
• [Sel84]
• [PR83]
• [BP86]

Categories

inductive Steedman2000.Atom : Type

The atomic categories of the toy English fragment, without the book's features.

• S : Atom

  Sentence.

• NP : Atom

  Noun phrase.

def Steedman2000.instReprAtom.repr : Atom → ℕ → Std.Format

Equations

• Steedman2000.instReprAtom.repr Steedman2000.Atom.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Steedman2000.Atom.S")).group prec✝
• Steedman2000.instReprAtom.repr Steedman2000.Atom.NP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Steedman2000.Atom.NP")).group prec✝

@[instance_reducible]

instance Steedman2000.instReprAtom : Repr Atom

Equations

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

@[instance_reducible]

instance Steedman2000.instDecidableEqAtom : DecidableEq Atom

Equations

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

def Steedman2000.S : CCG.Cat Atom

Equations

• Steedman2000.S = CCG.Cat.atom Steedman2000.Atom.S

def Steedman2000.NP : CCG.Cat Atom

Equations

• Steedman2000.NP = CCG.Cat.atom Steedman2000.Atom.NP

def Steedman2000.IV : CCG.Cat Atom

The intransitive verb category S\NP, the book's VP.

Equations

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

def Steedman2000.TV : CCG.Cat Atom

The transitive verb category (S\NP)/NP.

Equations

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

def Steedman2000.atomTy : Atom → Montague.Ty

The semantic type of an atom, truth values for sentences and entities for noun phrases.

Equations

• Steedman2000.atomTy Steedman2000.Atom.S = Montague.Ty.t
• Steedman2000.atomTy Steedman2000.Atom.NP = Montague.Ty.e

Word order

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

def Steedman2000.john_sleeps : CCG.Derivation String CCG.RuleSystem.multimodal S

Equations

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

def Steedman2000.john_sees_mary : CCG.Derivation String CCG.RuleSystem.multimodal S

Equations

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

Non-constituent coordination

def Steedman2000.john_tr : CCG.Derivation String CCG.RuleSystem.multimodal (S.rslash CCG.Modality.dot (S.lslash CCG.Modality.dot NP))

The type-raised subject "John" is a lexical leaf of category S/(S\NP).

Equations

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

def Steedman2000.mary_tr : CCG.Derivation String CCG.RuleSystem.multimodal (S.rslash CCG.Modality.dot (S.lslash CCG.Modality.dot NP))

Equations

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

def Steedman2000.john_sees : CCG.Derivation String CCG.RuleSystem.multimodal (S.rslash CCG.Modality.dot NP)

"John sees" is the type-raised subject composed with the transitive verb, a constituent of category S/NP.

Equations

• Steedman2000.john_sees = Steedman2000.john_tr.fcomp (CCG.Derivation.lex "sees" Steedman2000.TV) Steedman2000.john_sees._proof_1

def Steedman2000.mary_eats : CCG.Derivation String CCG.RuleSystem.multimodal (S.rslash CCG.Modality.dot NP)

Equations

• Steedman2000.mary_eats = Steedman2000.mary_tr.fcomp (CCG.Derivation.lex "eats" Steedman2000.TV) Steedman2000.john_sees._proof_1

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

conj c is the category (c \⋆ c) /⋆ c of a conjunction coordinating constituents of category c. Its star slashes confine it to application.

Equations

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

def Steedman2000.john_sees_and_mary_eats : CCG.Derivation String CCG.RuleSystem.multimodal (S.rslash CCG.Modality.dot NP)

"John sees and Mary eats" coordinates two S/NP constituents through the lexical conjunction, as in the book's "Anna married, and I detest".

Equations

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

def Steedman2000.john_sees_and_mary_eats_pizza : CCG.Derivation String CCG.RuleSystem.multimodal S

Equations

• Steedman2000.john_sees_and_mary_eats_pizza = Steedman2000.john_sees_and_mary_eats.fapp (CCG.Derivation.lex "pizza" Steedman2000.NP) Steedman2000.john_sees_and_mary_eats_pizza._proof_1

theorem Steedman2000.john_sees_and_mary_eats_pizza_yield : john_sees_and_mary_eats_pizza.yield = ["John", "sees", "and", "Mary", "eats", "pizza"]

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

def Steedman2000.semLexicon : CCG.SemLexicon String atomTy HeimKratzer.ToyEntity Unit

semLexicon interprets the toy English fragment. It gives meanings to names, type-raised names, verbs, and conjunctions at S and at S/NP.

Equations

• One or more equations did not get rendered due to their size.
• Steedman2000.semLexicon "John" (CCG.Cat.atom Steedman2000.Atom.NP) = some HeimKratzer.ToyEntity.john
• Steedman2000.semLexicon "Mary" (CCG.Cat.atom Steedman2000.Atom.NP) = some HeimKratzer.ToyEntity.mary
• Steedman2000.semLexicon "pizza" (CCG.Cat.atom Steedman2000.Atom.NP) = some HeimKratzer.ToyEntity.pizza
• Steedman2000.semLexicon "book" (CCG.Cat.atom Steedman2000.Atom.NP) = some HeimKratzer.ToyEntity.book
• Steedman2000.semLexicon "sleeps" ((CCG.Cat.atom Steedman2000.Atom.S).lslash a (CCG.Cat.atom Steedman2000.Atom.NP)) = some HeimKratzer.Toy.sleeps
• Steedman2000.semLexicon "laughs" ((CCG.Cat.atom Steedman2000.Atom.S).lslash a (CCG.Cat.atom Steedman2000.Atom.NP)) = some HeimKratzer.Toy.laughs
• Steedman2000.semLexicon word cat = none

def Steedman2000.john_sees_mary_via_tr : CCG.Derivation String CCG.RuleSystem.multimodal S

"John sees Mary" with a type-raised subject produces the same truth value as the canonical derivation.

Equations

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

theorem Steedman2000.interp_john_sees_mary_via_tr : CCG.Derivation.interp semLexicon john_sees_mary_via_tr = CCG.Derivation.interp semLexicon john_sees_mary

theorem Steedman2000.coord_interp_pointwise (e : HeimKratzer.ToyEntity) : Option.map (fun (x : Montague.Ty.Domain HeimKratzer.ToyEntity Unit (CCG.Cat.toTy atomTy (S.rslash CCG.Modality.dot NP))) => x e) (CCG.Derivation.interp semLexicon john_sees_and_mary_eats) = match CCG.Derivation.interp semLexicon john_sees, CCG.Derivation.interp semLexicon mary_eats with | some m₁, some m₂ => some (m₁ e ∧ m₂ e) | x, x_1 => none

At each entity the coordinated S/NP predicate is the conjunction of the two conjoined predicates.

def Steedman2000.john_sees_pizza_and_mary_eats_pizza : CCG.Derivation String CCG.RuleSystem.multimodal S

The spelled-out paraphrase is "John sees pizza and Mary eats pizza".

Equations

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

theorem Steedman2000.nonConstituentCoord_eq_spelledOut : CCG.Derivation.interp semLexicon john_sees_and_mary_eats_pizza = CCG.Derivation.interp semLexicon john_sees_pizza_and_mary_eats_pizza

The non-constituent coordination and its spelled-out paraphrase receive the same truth conditions, since the composed derivation yields the canonical predicate-argument structure.

def Steedman2000.pqLex : CCG.SemLexicon String atomTy Unit Unit

A lexicon in which sentence p is true and q false, with the English coordinators interpreted by the Boolean operation of their role.

Equations

• One or more equations did not get rendered due to their size.
• Steedman2000.pqLex "p" (CCG.Cat.atom Steedman2000.Atom.S) = some True
• Steedman2000.pqLex "q" (CCG.Cat.atom Steedman2000.Atom.S) = some False
• Steedman2000.pqLex w c = none

def Steedman2000.dp : CCG.Derivation String CCG.RuleSystem.multimodal S

Equations

• Steedman2000.dp = CCG.Derivation.lex "p" Steedman2000.S

def Steedman2000.dq : CCG.Derivation String CCG.RuleSystem.multimodal S

Equations

• Steedman2000.dq = CCG.Derivation.lex "q" Steedman2000.S

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

With a true and a false conjunct, coordination by and and by or receive different truth values, so the coordinator is part of a derivation's truth conditions.

Gapping

The arguments of a verb, raised order-preservingly over the functions that seek them, compose into a cluster that coordinates with other clusters and then combines with the verb. Over a verb-final verb the cluster looks rightward for it, so the verb follows the coordinated clusters (backward gapping); over a verb-initial verb it looks leftward (forward gapping); over a verb-medial verb the arguments raise in opposite directions and form no cluster.

def Steedman2000.raiseArg : CCG.Cat Atom → Option (CCG.Cat Atom)

raiseArg c raises the argument of the function category c order-preservingly over c. The argument of X\A raises to X/(X\A) and that of X/A to X\(X/A).

Equations

• Steedman2000.raiseArg (x_1.lslash a a_1) = some (a_1.forwardTypeRaise x_1)
• Steedman2000.raiseArg (x_1.rslash a a_1) = some (a_1.backwardTypeRaise x_1)
• Steedman2000.raiseArg (CCG.Cat.atom a) = none

def Steedman2000.hcomp : CCG.Cat Atom → CCG.Cat Atom → Option (CCG.Cat Atom)

hcomp is harmonic composition, the order-preserving rules >B and <B.

Equations

• Steedman2000.hcomp (x_2.rslash a y) (y'.rslash n z) = if y = y' then some (x_2.rslash n z) else none
• Steedman2000.hcomp (y'.lslash n z) (x_2.lslash a y) = if y = y' then some (x_2.lslash n z) else none
• Steedman2000.hcomp x✝¹ x✝ = none

def Steedman2000.cluster (v : CCG.Cat Atom) : Option (CCG.Cat Atom)

cluster v is the category of the argument cluster over the transitive verb category v. The verb's two arguments are raised over the functions that seek them and composed harmonically, in whichever order the rules allow.

Equations

• Steedman2000.cluster (x_1.lslash a a_1) = do let r₁ ← Steedman2000.raiseArg x_1 let r₂ ← Steedman2000.raiseArg (x_1.lslash a a_1) Steedman2000.hcomp r₁ r₂ <|> Steedman2000.hcomp r₂ r₁
• Steedman2000.cluster (x_1.rslash a a_1) = do let r₁ ← Steedman2000.raiseArg x_1 let r₂ ← Steedman2000.raiseArg (x_1.rslash a a_1) Steedman2000.hcomp r₁ r₂ <|> Steedman2000.hcomp r₂ r₁
• Steedman2000.cluster (CCG.Cat.atom a) = none

def Steedman2000.sovTV : CCG.Cat Atom

The verb-final transitive verb category (S\NP)\NP, the book's tazuneta (chapter 7 (2)).

Equations

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

def Steedman2000.vsoTV : CCG.Cat Atom

The verb-initial transitive verb category (S/NP)/NP, the book's chonaic (chapter 7 (17)), which Dutch main-clause verbs share and which English gapping reveals.

Equations

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

theorem Steedman2000.cluster_sov : cluster sovTV = some (S.rslash CCG.Modality.dot sovTV)

Over a verb-final verb the cluster looks rightward for the verb (chapter 7 (3b)).

theorem Steedman2000.cluster_vso : cluster vsoTV = some (S.lslash CCG.Modality.dot vsoTV)

Over a verb-initial verb the cluster looks leftward (chapter 7 (18b)).

theorem Steedman2000.cluster_svo : cluster TV = none

A verb-medial verb has no cluster, since its arguments raise in opposite directions and no harmonic rule composes them.

def Steedman2000.backwardGappedConjunct : CCG.Derivation String CCG.RuleSystem.multimodal (S.rslash CCG.Modality.dot sovTV)

The backward-gapped conjunct "Ken-ga Naomi-o" of chapter 7 (3b), by forward raising and forward composition.

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.gappedConjunct : CCG.Derivation String CCG.RuleSystem.multimodal (S.lslash CCG.Modality.dot vsoTV)

The forward-gapped English conjunct "Warren, potatoes" of chapter 7 (67), a cluster over a virtual verb-initial verb, by backward raising and backward composition.

Equations

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

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

Ross's generalization over the basic orders

def Steedman2000.transitiveCat (a : WordOrder.Arrangement WordOrder.Constituent 3) : CCG.Cat Atom

The transitive verb category of the basic order a, whose slash for each argument looks to the edge of the verb on which a puts it, the object first as in the English (S\NP)/NP. Which argument comes first matters to the category only when the two slashes look different ways.

Equations

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

theorem Steedman2000.transitiveCat_sov : transitiveCat WordOrder.Arrangement.sov = sovTV

theorem Steedman2000.transitiveCat_vso : transitiveCat WordOrder.Arrangement.vso = vsoTV

theorem Steedman2000.transitiveCat_svo : transitiveCat WordOrder.Arrangement.svo = TV

inductive Steedman2000.GappingDirection : Type

The two directions of gapping. Forward gapping keeps the verb in the first conjunct and backward gapping in the last.

• 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.

def Steedman2000.gappingDirection (v : CCG.Cat Atom) : Option GappingDirection

The direction of gapping over the verb category v, read off the cluster of its arguments, is backward when the cluster looks rightward for the verb and forward when it looks leftward.

Equations

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

theorem Steedman2000.gappingDirection_transitiveCat (a : WordOrder.Arrangement WordOrder.Constituent 3) : gappingDirection (transitiveCat a) = if a.IsFinal WordOrder.Constituent.verb then some GappingDirection.backward else if a.IsInitial WordOrder.Constituent.verb then some GappingDirection.forward else none

Ross's generalization for every basic order. As chapter 7 (77) restates it, the direction of gapping follows the direction in which the verb combines, so verb-final orders gap backward and verb-initial orders forward, while a verb-medial verb has no argument cluster.

The revealing rule

def Steedman2000.RightwardInto (t : CCG.Cat Atom) : CCG.Cat Atom → Prop

RightwardInto t c holds when c is t or a rightward function into t, a member of the book's t/$.

Equations

• Steedman2000.RightwardInto t (a.rslash a_1 a_2) = (a.rslash a_1 a_2 = t ∨ Steedman2000.RightwardInto t a)
• Steedman2000.RightwardInto t x✝ = (x✝ = t)

def Steedman2000.RightwardInto.decidable (t c : CCG.Cat Atom) : Decidable (RightwardInto t c)

RightwardInto t is decided by recursion on the category.

Equations

• Steedman2000.RightwardInto.decidable t (x_1.rslash m y) = { decide := decide (x_1.rslash m y = t) || decide (Steedman2000.RightwardInto t x_1), reflects_decide := ⋯ }
• Steedman2000.RightwardInto.decidable t (x_1.lslash m y) = Steedman2000.RightwardInto.decidable._aux_2 t x_1 m y
• Steedman2000.RightwardInto.decidable t (CCG.Cat.atom a) = Steedman2000.RightwardInto.decidable._aux_4 t a

@[instance_reducible]

instance Steedman2000.instDecidablePredCatAtomRightwardInto (t : CCG.Cat Atom) : DecidablePred (RightwardInto t)

Equations

• Steedman2000.instDecidablePredCatAtomRightwardInto t = Steedman2000.RightwardInto.decidable t

def Steedman2000.RevealedResidue : CCG.Cat Atom → Prop

The virtual conjunct-revealing rule of chapter 7 (61) decomposes a sentence into a revealed Y = S/$ and the residue S\Y. RevealedResidue c says c is such a residue.

Equations

• Steedman2000.RevealedResidue (x_1.lslash a y) = (x_1 = Steedman2000.S ∧ Steedman2000.RightwardInto Steedman2000.S y)
• Steedman2000.RevealedResidue x✝ = False

@[instance_reducible]

instance Steedman2000.instDecidablePredCatAtomRevealedResidue : DecidablePred RevealedResidue

Equations

• One or more equations did not get rendered due to their size.
• Steedman2000.instDecidablePredCatAtomRevealedResidue (x_1.rslash a a_1) = isFalse ⋯
• Steedman2000.instDecidablePredCatAtomRevealedResidue (CCG.Cat.atom a) = isFalse ⋯

theorem Steedman2000.rightwardInto_transitiveCat_iff (a : WordOrder.Arrangement WordOrder.Constituent 3) : RightwardInto S (transitiveCat a) ↔ a.IsInitial WordOrder.Constituent.verb

The revealing rule exposes exactly the verb-initial transitive verbs, since its revealed category is S/$. An SVO clause, whose own verb has no argument cluster, therefore gaps over a virtual verb-initial verb, as English does in chapter 7 (62).

def Steedman2000.predictedDirection (a : WordOrder.Arrangement WordOrder.Constituent 3) : Option GappingDirection

A clause of basic order a gaps in the direction of the cluster over its verb, or, when the verb has none, in that of the cluster over the verb-initial verb the revealing rule exposes.

Equations

• Steedman2000.predictedDirection a = (Steedman2000.gappingDirection (Steedman2000.transitiveCat a) <|> Steedman2000.gappingDirection Steedman2000.vsoTV)

def Steedman2000.gappingData : List Datum

The gapping examples of chapter 7.

Equations

• Steedman2000.gappingData = List.filter (fun (x : Datum) => decide (x.feature? "phenomenon" = some "gapping")) Steedman2000.Examples.all

theorem Steedman2000.gapping_acceptable_iff (ex : Datum) : ex ∈ gappingData → (ex.judgment = Judgment.acceptable ↔ ex.parse? "gappingDirection" [("forward", GappingDirection.forward), ("backward", GappingDirection.backward)] = ((ex.feature? "wordOrder").bind WordOrder.Arrangement.ofLabel?).bind predictedDirection)

In every gapping example of chapter 7, the construction is acceptable exactly when it gaps in the direction its clause's basic order predicts.

Other elliptical constructions

inductive Steedman2000.EllipsisType : Type

The book's elliptical constructions.

• gapping : EllipsisType

  "Dexter eats bread, and Warren, potatoes" (chapter 7 (62)).

• stripping : EllipsisType

  "Dexter ran away, and Warren (too)" (chapter 7 (78a)).

• sluicing : EllipsisType

  "Dexter did something with the beans, but I don't know what" (chapter 7 (84a)).

• vpEllipsis : EllipsisType

  "Somebody has to do the job, but I know that I won't" (chapter 7 (84b)).

@[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.elidedConjunct : EllipsisType → CCG.Cat Atom

The category of the right conjunct each construction coordinates with a full sentence, as in the gapped "Warren, potatoes" (67), the stripped "Warren" (81), and the sluiced and VP-elided conjuncts (84).

Equations

• Steedman2000.elidedConjunct Steedman2000.EllipsisType.gapping = Steedman2000.S.lslash CCG.Modality.dot Steedman2000.vsoTV
• Steedman2000.elidedConjunct Steedman2000.EllipsisType.stripping = Steedman2000.S.lslash CCG.Modality.dot (Steedman2000.S.rslash CCG.Modality.dot Steedman2000.NP)
• Steedman2000.elidedConjunct Steedman2000.EllipsisType.sluicing = Steedman2000.S.rslash CCG.Modality.dot (Steedman2000.S.rslash CCG.Modality.dot Steedman2000.NP)
• Steedman2000.elidedConjunct Steedman2000.EllipsisType.vpEllipsis = Steedman2000.S.rslash CCG.Modality.dot Steedman2000.IV

theorem Steedman2000.revealedResidue_elidedConjunct_iff (e : EllipsisType) : RevealedResidue (elidedConjunct e) ↔ e = EllipsisType.gapping ∨ e = EllipsisType.stripping

Gapping and stripping are mediated by the combinatory syntax, since the revealing rule decomposes the left conjunct into a residue of their right conjunct's category to coordinate with. Sluicing and VP ellipsis are not, since their conjuncts look rightward, and the book leaves them to an anaphoric mechanism.

Cross-serial dependencies

In the Dutch fragment of chapter 6 a subordinate-clause raising verb takes its NP arguments leftward and its infinitival complement rightward (12), and the one crossing rule, forward crossed composition restricted to VP complements (14), builds the verb cluster, so the NPs precede the whole cluster in the cross-serial order.

def Steedman2000.dutchRules : CCG.RuleSystem Atom

The rules of the Dutch fragment are application and the Dutch forward crossed composition of chapter 6 (14), X/Y (Y\Z)$ ⇒ (X\Z)$ with Y = VP.

Equations

• Steedman2000.dutchRules x✝ a β = (β = [] ∨ a.side = Edge.right ∧ a.cat = Steedman2000.IV ∧ Option.map (fun (x : CCG.Cat.Arg Steedman2000.Atom) => x.side) β.head? = some Edge.left)

@[instance_reducible]

instance Steedman2000.instDecidableDutchRules (x : CCG.Cat Atom) (a : CCG.Cat.Arg Atom) (β : List (CCG.Cat.Arg Atom)) : Decidable (dutchRules x a β)

Equations

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

def Steedman2000.dutchLexicon : List (String × CCG.Cat Atom)

The lexicon of chapter 6 (12), without the book's subordination feature. zag 'saw' and helpen 'help' take their infinitival complement rightward and their NP arguments leftward.

Equations

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

def Steedman2000.zagVoeren : CCG.Derivation String dutchRules S

In "(dat) ik Cecilia de nijlpaarden zag voeren" (chapter 6 (15)) zag crossed-composes with voeren, and the NPs combine with the cluster by backward application.

Equations

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

def Steedman2000.zagHelpenVoeren : CCG.Derivation String dutchRules S

In "(dat) ik Cecilia Henk de nijlpaarden zag helpen voeren" (chapter 6 (16)) helpen crossed-composes with voeren and zag with the result at degree 2, so each NP is the argument of the verb in the same position of the cluster, the cross-serial dependency.

Equations

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

theorem Steedman2000.crossSerial_derived : (CCG.Derivation.LexIn dutchLexicon zagVoeren ∧ zagVoeren.yield = ["ik", "Cecilia", "de nijlpaarden", "zag", "voeren"]) ∧ CCG.Derivation.LexIn dutchLexicon zagHelpenVoeren ∧ zagHelpenVoeren.yield = ["ik", "Cecilia", "Henk", "de nijlpaarden", "zag", "helpen", "voeren"]

Both cross-serial sentences are derived from the lexicon.

theorem Steedman2000.not_dutchRules_raised : ¬dutchRules (S.lslash CCG.Modality.dot NP) { side := Edge.right, modality := CCG.Modality.dot, cat := (S.lslash CCG.Modality.dot NP).lslash CCG.Modality.dot NP } [{ side := Edge.left, modality := CCG.Modality.dot, cat := NP }]

The restriction of crossed composition to VP complements keeps a raised argument from crossed-composing into a verb, as chapter 6 notes of (14).

Verb clusters and quantifier scope

A quantified argument takes scope over the tensed verb when it combines, as a functor, with a constituent containing that verb (chapter 6, on (96) and (97)). In the verb-raising order the verbs compose into such a constituent first. In the verb-projection-raising order the quantified object must combine with the embedded verb before anything combines with the tensed one, so it never takes the tensed verb in its scope, though the tensed verb can still compose.

inductive Steedman2000.VerbOrder : Type

VerbOrder is the word order of a West Germanic verb cluster.

• verbRaising : VerbOrder

  The object precedes the whole verb cluster.

• verbProjectionRaising : VerbOrder

  The object follows the matrix verb.

@[instance_reducible]

instance Steedman2000.instDecidableEqVerbOrder : DecidableEq VerbOrder

Equations

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

@[instance_reducible]

instance Steedman2000.instReprVerbOrder : Repr VerbOrder

Equations

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

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

Equations

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

@[instance_reducible]

instance Steedman2000.instInhabitedVerbOrder : Inhabited VerbOrder

Equations

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

def Steedman2000.FunctorOver {R : CCG.RuleSystem Atom} {l r c : CCG.Cat Atom} (q : List String) (v : String) : CCG.Rule R l r c → List String → List String → Prop

The node ru over daughters spelling out u and w has a primary functor spelling out q and a secondary containing v.

Equations

• Steedman2000.FunctorOver q v (CCG.Rule.forward β h) x✝¹ x✝ = (x✝¹ = q ∧ v ∈ x✝)
• Steedman2000.FunctorOver q v (CCG.Rule.backward β h) x✝¹ x✝ = (x✝ = q ∧ v ∈ x✝¹)

@[instance_reducible]

instance Steedman2000.instDecidableFunctorOver {R : CCG.RuleSystem Atom} {l r c : CCG.Cat Atom} (q : List String) (v : String) (ru : CCG.Rule R l r c) (u w : List String) : Decidable (FunctorOver q v ru u w)

Equations

• Steedman2000.instDecidableFunctorOver q v (CCG.Rule.forward β h) x✝¹ x✝ = { decide := decide (x✝¹ = q) && decide (v ∈ x✝), reflects_decide := ⋯ }
• Steedman2000.instDecidableFunctorOver q v (CCG.Rule.backward β h) x✝¹ x✝ = { decide := decide (x✝ = q) && decide (v ∈ x✝¹), reflects_decide := ⋯ }

def Steedman2000.ScopesOver {R : CCG.RuleSystem Atom} (q : List String) (v : String) {c : CCG.Cat Atom} : CCG.Derivation String R c → Prop

ScopesOver q v d holds when some node of d combines a functor spelling out q with a constituent containing v, the configuration in which q takes scope over v.

Equations

• Steedman2000.ScopesOver q v (CCG.Derivation.lex t x✝) = False
• Steedman2000.ScopesOver q v (CCG.Derivation.node ru d₁ d₂) = (Steedman2000.FunctorOver q v ru d₁.yield d₂.yield ∨ Steedman2000.ScopesOver q v d₁ ∨ Steedman2000.ScopesOver q v d₂)

@[instance_reducible]

instance Steedman2000.ScopesOver.decidable {R : CCG.RuleSystem Atom} (q : List String) (v : String) {c : CCG.Cat Atom} (d : CCG.Derivation String R c) : Decidable (ScopesOver q v d)

Equations

• One or more equations did not get rendered due to their size.
• Steedman2000.ScopesOver.decidable q v (CCG.Derivation.lex t x✝) = isFalse ⋯

theorem Steedman2000.ScopesOver.mem_yield {R : CCG.RuleSystem Atom} {q : List String} {v : String} {c : CCG.Cat Atom} {d : CCG.Derivation String R c} (h : ScopesOver q v d) : (∀ x ∈ q, x ∈ d.yield) ∧ v ∈ d.yield

ScopesOver q v d needs both q and v among the words of d.

def Steedman2000.scopeLexicon : List (String × CCG.Cat Atom)

The verbs and the quantified object of the Dutch examples (99). The tensed equi verb "probeert" 'tries' takes its infinitival complement rightward, "te zingen" 'to sing' its object leftward, and "veel liederen" 'many songs' is raised order-preservingly over the verbs that take it leftward.

Equations

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

def Steedman2000.orderString : VerbOrder → List String

The string of the example (99) in each verb order.

Equations

• Steedman2000.orderString Steedman2000.VerbOrder.verbRaising = ["veel liederen", "probeert", "te zingen"]
• Steedman2000.orderString Steedman2000.VerbOrder.verbProjectionRaising = ["probeert", "veel liederen", "te zingen"]

@[reducible, inline]

abbrev Steedman2000.ObjectOutscopesTense {R : CCG.RuleSystem Atom} {c : CCG.Cat Atom} (d : CCG.Derivation String R c) : Prop

The quantified object takes scope over the tensed verb "probeert".

Equations

• Steedman2000.ObjectOutscopesTense d = Steedman2000.ScopesOver ["veel liederen"] "probeert" d

def Steedman2000.InverseAvailable (o : VerbOrder) : Prop

The inverse reading of the order o is available when some derivation of its string over the lexicon lets the quantified object take scope over the tensed verb.

Equations

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

def Steedman2000.verbRaisingDeriv : CCG.Derivation String CCG.RuleSystem.multimodal IV

In the verb-raising order (99a) the cluster "probeert te zingen" forms by crossed composition and the raised object applies to it.

Equations

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

def Steedman2000.verbProjectionRaisingComposed : CCG.Derivation String CCG.RuleSystem.multimodal IV

In the verb-projection-raising order (99b) the tensed verb can compose with the raised object, but then the object is the tensed verb's secondary, not a functor over it.

Equations

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

theorem Steedman2000.verbProjectionRaisingComposed_hasComp_not_outscopes : CCG.Derivation.LexIn scopeLexicon verbProjectionRaisingComposed ∧ verbProjectionRaisingComposed.yield = orderString VerbOrder.verbProjectionRaising ∧ verbProjectionRaisingComposed.HasComp ∧ ¬ObjectOutscopesTense verbProjectionRaisingComposed

Composition is not what licenses wide scope: the composed verb-projection-raising derivation has a composition node, yet the object does not take scope over the tensed verb.

theorem Steedman2000.not_outscopes_of_verbProjectionRaising {R : CCG.RuleSystem Atom} {c : CCG.Cat Atom} (e : CCG.Derivation String R c) (hl : CCG.Derivation.LexIn scopeLexicon e) (hy : e.yield = orderString VerbOrder.verbProjectionRaising) : ¬ObjectOutscopesTense e

In the verb-projection-raising order no derivation, in any rule system, lets the quantified object take scope over the tensed verb: the object can be a functor only over "te zingen", since its category looks rightward.

theorem Steedman2000.inverseAvailable_iff (o : VerbOrder) : InverseAvailable o ↔ o = VerbOrder.verbRaising

The inverse reading is available in the verb-raising order and in no other.

def Steedman2000.scopeData : List (VerbOrder × Judgment)

scopeData pairs each scope example's word order with the judgment on its inverse reading, on which the quantified object outscopes the tensed verb.

Equations

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

theorem Steedman2000.inverse_acceptable_iff_available (d : VerbOrder × Judgment) : d ∈ scopeData → (d.2 = Judgment.acceptable ↔ InverseAvailable d.1)

The inverse reading is acceptable exactly where some derivation lets the quantified object combine with a constituent containing the tensed verb, in every judgment of the book's examples (96) to (100), credited in the data to [Bay96], [Kay98], [HvR86] and [Hae92].

theorem Steedman2000.exists_verbProjectionRaising_unacceptable : ∃ d ∈ scopeData, d.1 = VerbOrder.verbProjectionRaising ∧ d.2 = Judgment.unacceptable

The data hold a verb-projection-raising example whose inverse reading is rejected, so the account's restriction is tested.

Intonation and information structure

Alternative derivations of one string are alternative information structures, disambiguated by tune: "(ANNA married)(MANNY)" (chapter 5 (14)) carves the composed derivation into a theme and a rheme, and its mirror "(ANNA)(married MANNY)" (13) the applicative one. Prosodic phrases are tune-marked constituents, so only constituents of the grammar can be phrases, the Sense Unit Condition of [Sel84].

def Steedman2000.annaMannyAccents : CCG.Intonation.AccentAssignment String

The accents of "(ANNA married)(MANNY)" are a theme accent on "Anna" and a rheme accent on "Manny", with "married" unaccented.

Equations

• Steedman2000.annaMannyAccents "Anna" = some (Prosody.PitchAccent.leading Prosody.LevelTone.L Prosody.LevelTone.H)
• Steedman2000.annaMannyAccents "Manny" = some (Prosody.PitchAccent.mono Prosody.LevelTone.H)
• Steedman2000.annaMannyAccents w = none

def Steedman2000.anna_married : CCG.Derivation String CCG.RuleSystem.multimodal (S.rslash CCG.Modality.dot NP)

"ANNA married" is the composed theme constituent, of 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 θ, since the theme accent on "Anna" unifies with unaccented "married".

theorem Steedman2000.manny_rheme : CCG.Derivation.infoFeature annaMannyAccents (CCG.Derivation.lex "Manny" 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" NP) john_sees_and_mary_eats_pizza._proof_1) = none

Folding the rheme into the theme's constituent clashes. The whole sentence projects no single marking, so the tune forces the phrasing "[Anna married][Manny]".

def Steedman2000.mannyThemeAccents : CCG.Intonation.AccentAssignment String

The mirror answer "(ANNA)(married MANNY)" of chapter 5 (13) has a rheme accent on "Anna" and a theme accent on "Manny".

Equations

• Steedman2000.mannyThemeAccents "Anna" = some (Prosody.PitchAccent.mono Prosody.LevelTone.H)
• Steedman2000.mannyThemeAccents "Manny" = some (Prosody.PitchAccent.leading Prosody.LevelTone.L Prosody.LevelTone.H)
• Steedman2000.mannyThemeAccents w = none

theorem Steedman2000.married_manny_theme : CCG.Derivation.infoFeature mannyThemeAccents ((CCG.Derivation.lex "married" TV).fapp (CCG.Derivation.lex "Manny" NP) john_sees_mary._proof_1) = some CCG.Intonation.InfoFeature.θ ∧ CCG.Derivation.infoFeature mannyThemeAccents anna_married = some CCG.Intonation.InfoFeature.ρ

Under the mirror tune the theme is the applicative constituent "married MANNY", while the composed "ANNA married" of (14) carries the rheme, so the tune selects the derivation.

def Steedman2000.annaMannyUtterance : List (CCG.Intonation.ProsodicPhrase String CCG.RuleSystem.multimodal)

The utterance consists of 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 String CCG.RuleSystem.multimodal)) => (Option.map (fun (x : CCG.Intonation.ProsodicPhrase String CCG.RuleSystem.multimodal) => x.cat) i.theme, i.rheme.cat)) (CCG.Intonation.extractInfoStructure annaMannyUtterance) = some (some (S.rslash CCG.Modality.dot NP), NP)

The information structure extracted from the utterance has the S/NP constituent "ANNA married" as theme and "MANNY" as rheme.

Truth conditions

Derivations interpreted compositionally over the toy model: a true sentence and a false one.

def Steedman2000.mary_sleeps : CCG.Derivation String CCG.RuleSystem.multimodal S

Equations

• Steedman2000.mary_sleeps = (CCG.Derivation.lex "Mary" Steedman2000.NP).bapp (CCG.Derivation.lex "sleeps" Steedman2000.IV) Steedman2000.john_sleeps._proof_1

theorem Steedman2000.ccg_predicts_john_sleeps : ∃ (p : Montague.Ty.Domain HeimKratzer.ToyEntity Unit (CCG.Cat.toTy atomTy S)), CCG.Derivation.interp semLexicon john_sleeps = some p ∧ p

theorem Steedman2000.ccg_predicts_mary_sleeps : ∃ (p : Montague.Ty.Domain HeimKratzer.ToyEntity Unit (CCG.Cat.toTy atomTy S)), CCG.Derivation.interp semLexicon mary_sleeps = some p ∧ ¬p

theorem Steedman2000.ccg_predicts_john_sees_mary : ∃ (p : Montague.Ty.Domain HeimKratzer.ToyEntity Unit (CCG.Cat.toTy atomTy S)), CCG.Derivation.interp semLexicon john_sees_mary = some p ∧ p

The tune terminal as an intonation-phrase terminal

def Steedman2000.ipToTune (ip : BeckmanPierrehumbert1986.IntonationPhrase) (accent : Prosody.PitchAccent) : CCG.Intonation.Tune

ipToTune ip accent is the tune with pitch accent accent whose terminal contour is the final phrase accent and boundary tone of the intonation phrase ip.

Equations

• Steedman2000.ipToTune ip accent = { accent := accent, terminal := ip.terminalContour }

def Steedman2000.declarativeIP : BeckmanPierrehumbert1986.IntonationPhrase

A declarative intonation phrase has an L phrase accent and an L% boundary.

Equations

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

def Steedman2000.continuationIP : BeckmanPierrehumbert1986.IntonationPhrase

A continuation-rise intonation phrase has an L phrase accent and an H% boundary.

Equations

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

theorem Steedman2000.ipToTune_eq_tunes : ipToTune declarativeIP (Prosody.PitchAccent.mono Prosody.LevelTone.H) = CCG.Intonation.rhemeTune ∧ ipToTune continuationIP (Prosody.PitchAccent.leading Prosody.LevelTone.L Prosody.LevelTone.H) = CCG.Intonation.themeTune

A declarative intonation phrase with an H* accent is the rheme tune, and a continuation-rise phrase with an L+H* accent the theme tune.