Sag, Wasow & Bender (2003): Syntactic Theory: A Formal Introduction

This file formalizes two chapters of the textbook in the RSRL model theory of Syntax/HPSG. The binding theory of Chapter 7 says that an anaphor must be outranked by a coindexed argument on some argument-structure list and that a nonreflexive pronoun must not be, and the textbook's judgments on reflexives and pronouns follow from the binding grammar of Syntax/HPSG/Binding, whose outranking is local o-command (binding_rows). The long-distance dependencies of Chapter 15 rest on the list-valued feature GAP: the GAP Principle sums the daughters' gaps into the mother and the Head-Filler Rule discharges one, which is the filler-head construction of Syntax/HPSG/Construction. The Coordinate Structure Constraint and its across-the-board exception are then derived rather than stipulated: conjuncts share their SYN value, GAP included, so a gap in one conjunct whose filler lies outside is rejected while gaps in every conjunct paired with one filler pass (coordinationPrinciple, coordination_rows), and a conjunct cannot itself be a gap, since a gap is an argument unrealized in the syntax rather than an empty phrase (gap_not_conjunct).

Implementation notes

The textbook's ranking on argument-structure lists, with a prepositional object of equal rank to its PP, is the substrate's local o-command relation, given directly on a worked transitive clause; the rows record whether the pronoun's antecedent is its local o-commander. Coordination is a binary construct whose conjuncts share their category and GAP list by token identity, the SYN identity of the textbook's rule; n-ary coordination, the conjunction daughter and the semantic restriction list are not modelled. The Argument Realization Principle, the subject-extraction lexical rule and the initial symbol are not formalized.

References

• [SWB03]
• [Ros67]
• [Cho81]

def SagWasowBender2003.probing (t : String) : List Datum

The rows on a topic.

Equations

• SagWasowBender2003.probing t = List.filter (fun (x : Datum) => decide (x.feature? "topic" = some t)) SagWasowBender2003.Examples.all

Binding theory

def SagWasowBender2003.sorts : List (String × HPSG.RSRL.Binding.Srt)

Equations

• SagWasowBender2003.sorts = [("anaphor", HPSG.RSRL.Binding.Srt.ana), ("pronoun", HPSG.RSRL.Binding.Srt.ppro)]

def SagWasowBender2003.binders : List (String × HPSG.RSRL.Binding.Ent)

Equations

• SagWasowBender2003.binders = [("local", HPSG.RSRL.Binding.Ent.iSubj), ("nonlocal", HPSG.RSRL.Binding.Ent.iObj)]

theorem SagWasowBender2003.binding_rows (x : Datum) : x ∈ probing "binding" → ∀ s ∈ x.parse? "sort" sorts, ∀ i ∈ x.parse? "binder" binders, x.judgment = Judgment.acceptable ↔ (HPSG.RSRL.Binding.clause s i HPSG.RSRL.Binding.Ent.gMasc HPSG.RSRL.Binding.Ent.nSing).Models HPSG.RSRL.Binding.grammar

The rows on binding are acceptable exactly when the worked clause with a pronoun of the row's sort, coindexed with its local o-commander or not as the row records, satisfies the binding grammar: a reflexive needs a coindexed local o-commander and a nonreflexive pronoun must lack one.

Long-distance dependencies

def SagWasowBender2003.coordinationPrinciple : HPSG.RSRL.Constraint HPSG.Construction.sig

In the coordination construction the two conjuncts share their category and GAP list, and the mother carries them.

Equations

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

def SagWasowBender2003.swbGrammar : HPSG.RSRL.Grammar HPSG.Construction.sig

The filler-gap grammar with the coordination construction.

Equations

• SagWasowBender2003.swbGrammar = List.map HPSG.RSRL.Constraint.toDesc (HPSG.Construction.constraints ++ [SagWasowBender2003.coordinationPrinciple])

inductive SagWasowBender2003.CoordEnt : Type

The entities of a worked coordinate construct are the construct, its mother and two conjuncts, their category, a one-gap list with its NP gap and the gap's index, and the empty list.

• cxt : CoordEnt
• mtr : CoordEnt
• c₁ : CoordEnt
• c₂ : CoordEnt
• cat : CoordEnt
• np : CoordEnt
• g : CoordEnt
• gp : CoordEnt
• nil : CoordEnt
• ix : CoordEnt

@[instance_reducible]

instance SagWasowBender2003.instDecidableEqCoordEnt : DecidableEq CoordEnt

Equations

• SagWasowBender2003.instDecidableEqCoordEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SagWasowBender2003.instFintypeCoordEnt : Fintype CoordEnt

Equations

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

@[instance_reducible]

instance SagWasowBender2003.instReprCoordEnt : Repr CoordEnt

Equations

• SagWasowBender2003.instReprCoordEnt = { reprPrec := SagWasowBender2003.instReprCoordEnt.repr }

def SagWasowBender2003.instReprCoordEnt.repr : CoordEnt → ℕ → Std.Format

Equations

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

def SagWasowBender2003.gapList (b : Bool) : CoordEnt

The GAP list of a conjunct is the shared one-gap list when the conjunct contains a gap, and the empty list otherwise.

Equations

• SagWasowBender2003.gapList b = if b = true then SagWasowBender2003.CoordEnt.g else SagWasowBender2003.CoordEnt.nil

@[reducible]

def SagWasowBender2003.coordConstruct (gap₁ gap₂ : Bool) : HPSG.RSRL.Interpretation HPSG.Construction.sig CoordEnt

A coordinate construct of two clausal conjuncts, each containing a gap or not. The gap is one NP, shared by the conjuncts that have one, and the mother's GAP is the first conjunct's.

Equations

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

theorem SagWasowBender2003.coordConstruct_isWellTyped (g₁ g₂ : Bool) : (coordConstruct g₁ g₂).IsWellTyped

The worked coordinate constructs are well-typed.

def SagWasowBender2003.bools : List (String × Bool)

Equations

• SagWasowBender2003.bools = [("true", true), ("false", false)]

theorem SagWasowBender2003.coordination_rows (x : Datum) : x ∈ probing "coordination" → ∀ g₁ ∈ x.parse? "gapInFirst" bools, ∀ g₂ ∈ x.parse? "gapInSecond" bools, x.judgment = Judgment.acceptable ↔ (coordConstruct g₁ g₂).Models swbGrammar

The rows on coordination are acceptable exactly when the coordinate construct with a gap in the conjuncts the row records satisfies the grammar: a gap in one conjunct alone breaks the identity of the conjuncts' GAP lists, and gaps in both, paired with one filler, keep it.

theorem SagWasowBender2003.gap_not_conjunct {U : Type u_1} {I : HPSG.RSRL.Interpretation HPSG.Construction.sig U} (hI : I.IsWellTyped) {u v : U} (hv : I.A HPSG.Construction.Attr.CONJ1 u = some v) : ¬I.S v ≤ HPSG.Construction.Srt.gap

A conjunct is an overt expression and a gap a covert one, an argument unrealized in the syntax, so no well-typed interpretation has a gap for a conjunct.