Reinhart (1976): The syntactic domain of anaphora

This file formalizes the first chapter of the dissertation, which replaces precede-and-command by constituent command as the relation restricting coreference. A node commands another, after Langacker, when neither dominates the other and the S node most immediately dominating the first dominates the second; the received domain of a node consists of the nodes it precedes and commands, PrecedesAndCommands, and two noun phrases can corefer just in case, if either is in the domain of the other, the one in the domain is a pronoun, Permits. The dissertation's domain is instead the nodes a node c-commands (36), RoseTree.CCommands: neither dominates the other and the first branching node dominating the first dominates the second, so a domain is a constituent and linear order plays no part. Both domains are computed for the abstract tree (37), and the restriction under each is checked against the examples, permits_rows: the Rosa paradigm (11), Lasnik's free cases (12), preposed prepositional phrases, sentential and verbal prepositional phrases, and the Malagasy VOS pair. Precede-and-command fails exactly on the structures of types I and III of (50), where the two domains come apart, cCommands_iff_precedesAndCommands. C-command entails command whenever S nodes branch (49), and the formulation (10b) blocks whatever the pronoun-specific (10a) blocks, but not conversely.

Implementation notes

Trees are the dissertation's simplified structures, with one VP, a preposed phrase attached to the S of the subject, and a sentential adverbial attached to S; positions are Gorn addresses, and c-command is the substrate's command relation generated by the branching nodes with the clause that neither node dominates the other. The chapter 4 refinement for a preposed clause is not modelled, so the adverbial-clause examples of section 1.3 are left out, and the strict reflexive environments that (10) sets aside do not arise in the rows.

References

• T. Reinhart, The syntactic domain of anaphora (1976)
• R. W. Langacker, On pronominalization and the chain of command (1969)
• H. Lasnik, Remarks on coreference (1976)
• E. S. Klima, Negation in English (1964)
• N. Chomsky, Conditions on transformations (1973)

Command and c-command

def Reinhart1976.Commands {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) (a b : Core.Order.TreePath) : Prop

A node commands another (1) when neither dominates the other and the S node most immediately dominating the first dominates the second.

Equations

• Reinhart1976.Commands t a b = ((a, b) ∈ t.sCommand ∧ ¬a ≤ b ∧ ¬b ≤ a)

def Reinhart1976.PrecedesAndCommands {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) (a b : Core.Order.TreePath) : Prop

Precede-and-command is the domain relation of the received view (5).

Equations

• Reinhart1976.PrecedesAndCommands t a b = (a.Precedes b ∧ Reinhart1976.Commands t a b)

@[instance_reducible]

instance Reinhart1976.instDecidableRelTreePathCommands {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) : DecidableRel (Commands t)

Equations

• Reinhart1976.instDecidableRelTreePathCommands t x✝¹ x✝ = id inferInstance

@[instance_reducible]

instance Reinhart1976.instDecidableRelTreePathPrecedesAndCommands {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) : DecidableRel (PrecedesAndCommands t)

Equations

• Reinhart1976.instDecidableRelTreePathPrecedesAndCommands t x✝¹ x✝ = id inferInstance

theorem Reinhart1976.cCommands_commands {W : Type u_2} {t : PhraseStructure.Tree PhraseStructure.Cat W} {a b : Core.Order.TreePath} (hS : t.labeled {PhraseStructure.Cat.S} ⊆ {p : Core.Order.TreePath | RoseTree.IsBranchingAt t p}) (h : RoseTree.CCommands t a b) : Commands t a b

C-command entails command (49) whenever every S node branches.

theorem Reinhart1976.cCommand_eq_Ici {C : Type u_1} {W : Type u_2} {t : PhraseStructure.Tree C W} {a m : Core.Order.TreePath} (hm : m < a) (hb : RoseTree.IsBranchingAt t m) (hmax : ∀ x < a, RoseTree.IsBranchingAt t x → x ≤ m) : {b : Core.Order.TreePath | (a, b) ∈ RoseTree.cCommand t} = Set.Ici m

The c-command domain is a constituent (38). With m the first branching node dominating a, the nodes a c-commands, dominance aside, are those m dominates.

def Reinhart1976.TypeI {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) (a b : Core.Order.TreePath) : Prop

In type I of (50), a c-commands b but b precedes a.

Equations

• Reinhart1976.TypeI t a b = (RoseTree.CCommands t a b ∧ b.Precedes a)

def Reinhart1976.TypeIII {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) (a b : Core.Order.TreePath) : Prop

In type III of (50), a precedes and commands b but does not c-command it.

Equations

• Reinhart1976.TypeIII t a b = (Reinhart1976.PrecedesAndCommands t a b ∧ ¬RoseTree.CCommands t a b)

@[instance_reducible]

instance Reinhart1976.instDecidableRelTreePathTypeI {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) : DecidableRel (TypeI t)

Equations

• Reinhart1976.instDecidableRelTreePathTypeI t x✝¹ x✝ = id inferInstance

@[instance_reducible]

instance Reinhart1976.instDecidableRelTreePathTypeIII {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) : DecidableRel (TypeIII t)

Equations

• Reinhart1976.instDecidableRelTreePathTypeIII t x✝¹ x✝ = id inferInstance

theorem Reinhart1976.cCommands_iff_precedesAndCommands {W : Type u_2} {t : PhraseStructure.Tree PhraseStructure.Cat W} {a b : Core.Order.TreePath} (hS : t.labeled {PhraseStructure.Cat.S} ⊆ {p : Core.Order.TreePath | RoseTree.IsBranchingAt t p}) (h₁ : ¬TypeI t a b) (h₃ : ¬TypeIII t a b) : RoseTree.CCommands t a b ↔ PrecedesAndCommands t a b

The two domains agree except on types I and III (50).

The coreference restriction

def Reinhart1976.Permits (R : Core.Order.TreePath → Core.Order.TreePath → Prop) (pron : List Core.Order.TreePath) (a b : Core.Order.TreePath) : Prop

Under the restriction (10b), read with the domain relation R, two noun phrases can corefer just in case, if either is in the domain of the other, the one in the domain is a pronoun.

Equations

• Reinhart1976.Permits R pron a b = ((R a b → b ∈ pron) ∧ (R b a → a ∈ pron))

def Reinhart1976.Permits10a (R : Core.Order.TreePath → Core.Order.TreePath → Prop) (pron : List Core.Order.TreePath) (a b : Core.Order.TreePath) : Prop

Under the restriction (10a), two noun phrases can corefer just in case one is a pronoun, the other is not, and the non-pronoun is not in the domain of the pronoun; two names or two pronouns are not covered.

Equations

• Reinhart1976.Permits10a R pron a b = ((a ∈ pron ∧ b ∉ pron → ¬R a b) ∧ (b ∈ pron ∧ a ∉ pron → ¬R b a))

@[instance_reducible]

instance Reinhart1976.instDecidablePermitsOfDecidableRelTreePath (R : Core.Order.TreePath → Core.Order.TreePath → Prop) [DecidableRel R] (pron : List Core.Order.TreePath) (a b : Core.Order.TreePath) : Decidable (Permits R pron a b)

Equations

• Reinhart1976.instDecidablePermitsOfDecidableRelTreePath R pron a b = id inferInstance

@[instance_reducible]

instance Reinhart1976.instDecidablePermits10aOfDecidableRelTreePath (R : Core.Order.TreePath → Core.Order.TreePath → Prop) [DecidableRel R] (pron : List Core.Order.TreePath) (a b : Core.Order.TreePath) : Decidable (Permits10a R pron a b)

Equations

• Reinhart1976.instDecidablePermits10aOfDecidableRelTreePath R pron a b = id inferInstance

theorem Reinhart1976.permits10a_of_permits {R : Core.Order.TreePath → Core.Order.TreePath → Prop} {pron : List Core.Order.TreePath} {a b : Core.Order.TreePath} (h : Permits R pron a b) : Permits10a R pron a b

Whatever (10a) blocks, (10b) blocks.

The trees

def Reinhart1976.np : PhraseStructure.Tree PhraseStructure.Cat Unit

A noun phrase.

Equations

• Reinhart1976.np = PhraseStructure.Tree.node PhraseStructure.Cat.N [PhraseStructure.Tree.terminal PhraseStructure.Cat.N ()]

def Reinhart1976.tree37 : PhraseStructure.Tree PhraseStructure.Cat Unit

The abstract tree (37) is a cyclic node with daughters A, B and C, of which B branches into D and a cyclic node with daughters E and F.

Equations

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

def Reinhart1976.nodes37 : List Core.Order.TreePath

The nodes of (37) other than the root are A, B, C, D, the lower cyclic node, E and F.

Equations

• Reinhart1976.nodes37 = [{ toList := [0] }, { toList := [1] }, { toList := [2] }, { toList := [1, 0] }, { toList := [1, 1] }, { toList := [1, 1, 0] }, { toList := [1, 1, 1] }]

def Reinhart1976.domain (R : Core.Order.TreePath → Core.Order.TreePath → Prop) [DecidableRel R] (nodes : List Core.Order.TreePath) (a : Core.Order.TreePath) : List Core.Order.TreePath

The nodes among nodes in the relation R to a form the domain of a under R, without a itself.

Equations

• Reinhart1976.domain R nodes a = List.filter (fun (b : Core.Order.TreePath) => decide (R a b)) nodes

theorem Reinhart1976.domain_precedesAndCommands_tree37 : domain (PrecedesAndCommands tree37) nodes37 { toList := [0] } = [{ toList := [1] }, { toList := [2] }, { toList := [1, 0] }, { toList := [1, 1] }, { toList := [1, 1, 0] }, { toList := [1, 1, 1] }] ∧ domain (PrecedesAndCommands tree37) nodes37 { toList := [1] } = [{ toList := [2] }] ∧ domain (PrecedesAndCommands tree37) nodes37 { toList := [2] } = [] ∧ domain (PrecedesAndCommands tree37) nodes37 { toList := [1, 0] } = [{ toList := [2] }, { toList := [1, 1] }, { toList := [1, 1, 0] }, { toList := [1, 1, 1] }] ∧ domain (PrecedesAndCommands tree37) nodes37 { toList := [1, 1] } = [{ toList := [2] }] ∧ domain (PrecedesAndCommands tree37) nodes37 { toList := [1, 1, 0] } = [{ toList := [1, 1, 1] }] ∧ domain (PrecedesAndCommands tree37) nodes37 { toList := [1, 1, 1] } = []

In the precede-and-command domains of (37), table (39a), C has nothing in its domain, and D, which precedes and commands C, has C in its domain.

theorem Reinhart1976.domain_cCommands_tree37 : domain (RoseTree.CCommands tree37) nodes37 { toList := [0] } = [{ toList := [1] }, { toList := [2] }, { toList := [1, 0] }, { toList := [1, 1] }, { toList := [1, 1, 0] }, { toList := [1, 1, 1] }] ∧ domain (RoseTree.CCommands tree37) nodes37 { toList := [1] } = [{ toList := [0] }, { toList := [2] }] ∧ domain (RoseTree.CCommands tree37) nodes37 { toList := [2] } = [{ toList := [0] }, { toList := [1] }, { toList := [1, 0] }, { toList := [1, 1] }, { toList := [1, 1, 0] }, { toList := [1, 1, 1] }] ∧ domain (RoseTree.CCommands tree37) nodes37 { toList := [1, 0] } = [{ toList := [1, 1] }, { toList := [1, 1, 0] }, { toList := [1, 1, 1] }] ∧ domain (RoseTree.CCommands tree37) nodes37 { toList := [1, 1] } = [{ toList := [1, 0] }] ∧ domain (RoseTree.CCommands tree37) nodes37 { toList := [1, 1, 0] } = [{ toList := [1, 1, 1] }] ∧ domain (RoseTree.CCommands tree37) nodes37 { toList := [1, 1, 1] } = [{ toList := [1, 1, 0] }]

In the c-command domains of (37), table (39b), every domain is a constituent, C's is the whole sentence, and D's is B without C.

def Reinhart1976.tree9a : PhraseStructure.Tree PhraseStructure.Cat Unit

Example (9a) has a subject and an embedded subject, NP₁ denied that NP₂ has met the Shah, at 0 and 110.

Equations

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

def Reinhart1976.tree9b : PhraseStructure.Tree PhraseStructure.Cat Unit

Example (9b) has a noun phrase inside a relative clause of the subject, the man who traveled with NP₅, at 02111, and an embedded subject at 110.

Equations

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

def Reinhart1976.tree12 : PhraseStructure.Tree PhraseStructure.Cat Unit

Example (12) has an object inside a relative clause of the subject, people who know NP, at 0111, and the matrix object at 11.

Equations

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

def Reinhart1976.tree41 : PhraseStructure.Tree PhraseStructure.Cat Unit

Example (41) has a preposed prepositional phrase whose noun phrase, at 01, may contain a possessor at 010, with the subject at 1 and the object at 21.

Equations

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

def Reinhart1976.tree42 : PhraseStructure.Tree PhraseStructure.Cat Unit

Example (42) has a sentential prepositional phrase whose clause has a subject with a possessor at 2100, with the matrix subject at 0 and object at 11.

Equations

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

def Reinhart1976.tree48b : PhraseStructure.Tree PhraseStructure.Cat Unit

Example (48b) has a verb-phrasal prepositional phrase with a possessor at 11310, and the object at 111.

Equations

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

def Reinhart1976.tree51 : PhraseStructure.Tree PhraseStructure.Cat Unit

Example (51) is a VOS clause with a VP, the object at 01 with a possessor at 011, and the subject at 1 with a possessor at 11.

Equations

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

theorem Reinhart1976.typeI_tree41 : TypeI tree41 { toList := [1] } { toList := [0, 1] }

In (41) the subject c-commands the noun phrase of the preposed phrase, which precedes it, a pair of type I.

theorem Reinhart1976.typeIII_tree42 : TypeIII tree42 { toList := [1, 1] } { toList := [2, 1, 0, 0] }

In (42) the object precedes and commands the possessor in the sentential phrase without c-commanding it, a pair of type III.

theorem Reinhart1976.permits10a_not_permits : Permits10a (RoseTree.CCommands tree9a) [] { toList := [0] } { toList := [1, 1, 0] } ∧ ¬Permits (RoseTree.CCommands tree9a) [] { toList := [0] } { toList := [1, 1, 0] }

(10a) does not cover two names, so it fails to block (11a) where (10b) blocks it.

The dissertation's examples

def Reinhart1976.trees : List (String × PhraseStructure.Tree PhraseStructure.Cat Unit)

The trees by their paperFeatures labels.

Equations

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

def Reinhart1976.path (s : String) : Core.Order.TreePath

A position from its digits.

Equations

• Reinhart1976.path s = { toList := List.map (fun (c : Char) => c.toNat - '0'.toNat) s.toList }

structure Reinhart1976.Row : Type

An example records its tree, the two noun phrases, the pronouns among them, and the judgment of coreference: its coreference reading's where the prose gives one, else the mark.

• tree : PhraseStructure.Tree PhraseStructure.Cat Unit
• np₁ : Core.Order.TreePath
• np₂ : Core.Order.TreePath
• pron : List Core.Order.TreePath
• judgment : Judgment

def Reinhart1976.Row.ofDatum (e : Datum) : Option Row

A datum read into its row.

Equations

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

theorem Reinhart1976.isSome_ofDatum (e : Datum) : e ∈ Examples.all → (Row.ofDatum e).isSome = true

Every example is read.

def Reinhart1976.data : List Row

The dissertation's examples.

Equations

• Reinhart1976.data = List.filterMap Reinhart1976.Row.ofDatum Reinhart1976.Examples.all

theorem Reinhart1976.permits_rows (d : Row) : d ∈ data → (d.judgment = Judgment.acceptable ↔ Permits (RoseTree.CCommands d.tree) d.pron d.np₁ d.np₂)

Coreference is possible exactly when the restriction (10b) read with c-command permits it.

theorem Reinhart1976.exists_not_permits_precedesAndCommands : ∃ d ∈ data, ¬(d.judgment = Judgment.acceptable ↔ Permits (PrecedesAndCommands d.tree) d.pron d.np₁ d.np₂)

Read with precede-and-command, the restriction fails on Near him, Dan saw a snake and the Malagasy pair among others.

theorem Reinhart1976.typeI_or_typeIII_of_not_permits_precedesAndCommands (d : Row) : d ∈ data → ¬(d.judgment = Judgment.acceptable ↔ Permits (PrecedesAndCommands d.tree) d.pron d.np₁ d.np₂) → TypeI d.tree d.np₁ d.np₂ ∨ TypeI d.tree d.np₂ d.np₁ ∨ TypeIII d.tree d.np₁ d.np₂ ∨ TypeIII d.tree d.np₂ d.np₁

Precede-and-command fails only where the two domains come apart, on a pair of type I or type III in one order or the other.