Reinhart (1976) [Rei76]

The Syntactic Domain of Anaphora. PhD dissertation, MIT.

Key Contributions

1. C-command (def. 36, p. 32): replaces [Lan69]'s S-node-based "command" with a branching-node-based relation
2. C-command domain (def. 38, p. 33): the subtree dominated by the first branching node dominating A — always a constituent
3. Coreference restriction (10b, p. 14): domain-based, dispensing with "precede"
4. Claim (49) (p. 40): c-command ⊆ command (= cCommand ⊆ sCommand in B&P)
5. The irrelevance of precede (§1.4): linear order is epiphenomenal for coreference

Connection to [BP90]

Reinhart's c-command is exactly B&P's c-command (parameterized by branching nodes). [Lan69]'s command is B&P's S-command (parameterized by S-nodes). Theorem 49 follows from B&P's antitone map: since {S-nodes} ⊆ {branching nodes}, we get C_{branching} ⊆ C_{S}.

Concrete verification over the position tower

The concrete c-command facts (§5-§7) use Branching.cCommandAt — the B&P command relation over Branching.toTreeOrder of a concrete Syntax.Tree, generated by the geometric branching nodes (Branching.isBranchingAt, ≥ 2 daughters). In a binary tree every non-leaf node branches, so "the first branching node dominating A" is A's parent and A's parent dominates B iff A's sister dominates B — [Rei76]'s c-command. Membership is decide-checked via Branching.mem_commandRelation_toTreeOrder_iff, which collapses the defining universal to the finite list of A's prefixes.

Definition 1 (p. 8) — Langacker's "command"

A node A commands a node B if neither A nor B dominates the other and the S node most immediately dominating A also dominates B.

This is B&P's S-command, parameterized by S-nodes (Core.Order.commandRelation with P = S-nodes).

Definition 36 (p. 32) — C-command

Node A c(onstituent)-commands node B if neither A nor B dominates the other and the first branching node which dominates A dominates B.

This is B&P's c-command (their Definition 10), generated by branching nodes: Core.Order.cCommand abstractly, Branching.cCommandAt concretely.

Reinhart explicitly contrasts this with Langacker's command (p. 32): "The difference between the relations of command and of c-command is that while the first mentions cyclic nodes the second does not — all branching nodes can be relevant."

Definition 38 (p. 33) — C-command domain

The domain of a node A consists of A together with all and only the nodes c-commanded by A. (OR: The domain of a node A is the subtree dominated by the first branching node which dominates A.)

A key observation (p. 34): c-command domains are always constituents (subtrees), while precede-and-command domains may not be.

def Reinhart1976.cCommandDomain {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (a : Node) : Set Node

The c-command domain of a node a: the set of nodes that a c-commands, plus a itself.

In B&P terms: {b | (a, b) ∈ cCommand T} ∪ {a}.

Equations

• Reinhart1976.cCommandDomain T a = {b : Node | (a, b) ∈ Core.Order.cCommand T} ∪ {a}

Claim (49) (p. 40)

A c-commands B ⟶ A commands B A does not command B ⟶ A does not c-command B

In B&P terms: cCommand T ⊆ sCommand T, provided every S-node is also a branching node — a universally accepted structural assumption (S-nodes always dominate both a subject and a predicate).

theorem Reinhart1976.cCommand_implies_command {Node : Type} [PartialOrder Node] (T : BarkerPullum1990.LabeledTree Node) (h_S_branch : BarkerPullum1990.sNodes T ⊆ Core.Order.branchingNodes T.toTreeOrder) : Core.Order.cCommand T.toTreeOrder ⊆ BarkerPullum1990.sCommand T

Claim (49): C-command implies command.

Every S-node is a branching node (S-nodes dominate ≥2 children), so {S-nodes} ⊆ {branching nodes}, and by B&P's antitone map (command_antitone), C_{branching} ⊆ C_{S}.

Restriction 10b (p. 14)

Two NP's in a non strict reflexive environment can be coreferential just in case if either is in the domain of the other, the one in the domain is a pronoun.

Reinhart argues (§1.4) that the earlier formulation using precede-and-command is both empirically wrong (fails for preposed PPs) and theoretically unnatural (c-command domains are constituents; precede-and-command domains are not).

@[reducible, inline]

abbrev Reinhart1976.IsPronoun (Node : Type) : Type

Whether node a is a pronoun.

Equations

• Reinhart1976.IsPronoun Node = (Node → Prop)

def Reinhart1976.corefPermitted {Node : Type} [PartialOrder Node] (isPron : IsPronoun Node) (T : Core.Order.TreeOrder Node) (a b : Node) : Prop

Reinhart's Coreference Restriction (10b).

Two nodes can corefer unless one is in the c-command domain of the other and is not a pronoun.

corefPermitted isPron T a b holds iff:

• neither is in the other's domain, OR
• whichever is in the other's domain is a pronoun.

Equations

• Reinhart1976.corefPermitted isPron T a b = ((b ∈ Reinhart1976.cCommandDomain T a → isPron b) ∧ (a ∈ Reinhart1976.cCommandDomain T b → isPron a))

The irrelevance of precede (§1.4, §1.5)

Reinhart's central argumentative contribution: the relation precede plays no role in determining anaphora options. Two key observations:

1. Preposed PPs (§1.5.2): In "Near him, Dan saw a snake" (45), the pronoun precedes the antecedent yet coreference is fine — because "him" (PP-internal) does not c-command "Dan" (the subject). Meanwhile, "*Near Dan, he saw a snake" (43a) is correctly blocked: "Dan" is in the c-command domain of "he" and is not a pronoun.

2. VOS languages (p. 41): In Malagasy, the pronoun precedes and commands the antecedent (by the precede-and-command definition) yet coreference is permitted — because the pronoun does not c-command the antecedent.

Both facts follow automatically from the c-command restriction (10b) without mentioning linear order.

theorem Reinhart1976.command_ignores_precedence {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (P : Set Node) (a b : Node) : (a, b) ∈ Core.Order.commandRelation T P ↔ ∀ x ∈ Core.Order.upperBounds T a P, x ≤ b

Precede is irrelevant: c-command domains are symmetric with respect to linear order.

In B&P terms: the command relation C_P is defined purely in terms of dominance (upperBounds, dom), with no reference to precedence.

This is a structural fact about how commandRelation is defined — it uses only vertical (dominance) relations, never horizontal (precedence) relations.

C-command as cCommandAt over concrete trees

The concrete tests use the [BP90] tower: [Rei76]'s c-command is cCommandAt t — the B&P command relation over the dominance order Branching.toTreeOrder t of a concrete Syntax.Tree, generated by the geometric branching nodes (isBranchingAt, ≥ 2 daughters). Positions are TreePaths (Gorn addresses, 0 = left, 1 = right); membership is decide-checked via Branching.mem_commandRelation_toTreeOrder_iff. This replaces the earlier bespoke address/cCommand stack with the project-canonical position machinery, making the c-command facts theorems about the same command relation the rest of the library attributes to [Rei76] ([Rei76]'s c-command = B&P c-command).

def Reinhart1976.johnSawMary : Syntax.Tree Unit String

"John saw Mary": [S [NP John] [VP [V saw] [NP Mary]]]. Subject at ⟨[0]⟩, V at ⟨[1,0]⟩, object at ⟨[1,1]⟩.

Equations

• Reinhart1976.johnSawMary = (Syntax.Tree.leaf "John").bin ((Syntax.Tree.leaf "saw").bin (Syntax.Tree.leaf "Mary"))

theorem Reinhart1976.johnSawMary_yield : Core.Order.Branching.yield johnSawMary = ["John", "saw", "Mary"]

The yield is the surface string, left to right. With the per-instance simp lemmas (branching_yield_terminal/_node/...), the generic Branching.yield reduces on concrete Tree data by simp.

theorem Reinhart1976.subject_ccommands_object : ({ toList := [0] }, { toList := [1, 1] }) ∈ Core.Order.Branching.cCommandAt johnSawMary

The subject ⟨[0]⟩ k-commands the object ⟨[1,1]⟩: the only branching node dominating the subject is the root, which dominates everything.

theorem Reinhart1976.object_not_ccommands_subject : ({ toList := [1, 1] }, { toList := [0] }) ∉ Core.Order.Branching.cCommandAt johnSawMary

The converse fails: the object ⟨[1,1]⟩ does not k-command the subject ⟨[0]⟩ — the VP node ⟨[1]⟩ dominates the object but not the subject. This is the subject–object asymmetry.

theorem Reinhart1976.subject_ccommands_into_vp : ({ toList := [0] }, { toList := [1, 0] }) ∈ Core.Order.Branching.cCommandAt johnSawMary

The subject c-commands into the VP (here, the verb ⟨[1,0]⟩).

theorem Reinhart1976.object_verb_mutual_ccommand : ({ toList := [1, 1] }, { toList := [1, 0] }) ∈ Core.Order.Branching.cCommandAt johnSawMary ∧ ({ toList := [1, 0] }, { toList := [1, 1] }) ∈ Core.Order.Branching.cCommandAt johnSawMary

Object and verb mutually k-command (co-arguments inside the VP).

theorem Reinhart1976.ccommand_asymmetric_example : ({ toList := [0] }, { toList := [1, 1] }) ∈ Core.Order.Branching.cCommandAt johnSawMary ∧ ({ toList := [1, 1] }, { toList := [0] }) ∉ Core.Order.Branching.cCommandAt johnSawMary

C-command is not symmetric: subject k-commands object, not conversely.

Preposed PP example (§1.5.2)

[Rei76]'s structures (41)/(42) are ternary branching (S → PP NP₁ VP), but the key half of the argument is tree-shape-independent: the PP-internal NP ("Dan" inside "near Dan") does NOT c-command the subject region, because the first branching node dominating it is PP, which does not dominate the subject. The precede-and-command approach wrongly blocks backward pronominalization in "Near him, Dan saw a snake" (45); the c-command restriction correctly permits it.

def Reinhart1976.nearDanHeSaw : Syntax.Tree Unit String

Preposed PP, binary encoding [S [PP near Dan] [VP' [NP he] …]]: NP_Dan at ⟨[0,1]⟩, NP_he at ⟨[1,0]⟩. Dan does not k-command the subject-region NP_he: the only branching node above Dan that also sits above the subject is the root, but PP ⟨[0]⟩ dominates Dan and not the subject, blocking the universal.

Equations

• Reinhart1976.nearDanHeSaw = ((Syntax.Tree.leaf "near").bin (Syntax.Tree.leaf "Dan")).bin ((Syntax.Tree.leaf "he").bin ((Syntax.Tree.leaf "saw").bin (Syntax.Tree.leaf "snake")))

theorem Reinhart1976.preposed_pp_no_ccommand : ({ toList := [0, 1] }, { toList := [1, 0] }) ∉ Core.Order.Branching.cCommandAt nearDanHeSaw

Subject–object asymmetry with a complex subject

"The man who traveled with her denied that Rosa met the Shah": her deep inside the subject does NOT c-command the embedded subject Rosa, so coreference is permitted; whereas a bare matrix subject does c-command the embedded subject.

def Reinhart1976.complexSubject : Syntax.Tree Unit String

Complex-subject clause [S [NP the man with x her] [VP denied [S' Rosa metShah]]]: matrix subject ⟨[0]⟩, embedded subject ⟨[1,1,0]⟩, deep "her" ⟨[0,1,1,1,1]⟩.

Equations

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

theorem Reinhart1976.matrix_subject_ccommands_embedded : ({ toList := [0] }, { toList := [1, 1, 0] }) ∈ Core.Order.Branching.cCommandAt complexSubject

The matrix subject k-commands the embedded subject.

theorem Reinhart1976.deep_pronoun_not_ccommands_embedded : ({ toList := [0, 1, 1, 1, 1] }, { toList := [1, 1, 0] }) ∉ Core.Order.Branching.cCommandAt complexSubject

"her" deep inside the subject does not k-command the embedded subject: every branching node dominating it stays inside the subject.

Coreference permission over the tower (decidable)

A decidable, Prop-valued form of corefPermitted (10b) for concrete trees: coreference is permitted unless one NP k-commands the other and the k-commanded NP is not a pronoun.

def Reinhart1976.corefPermittedAt (t : Syntax.Tree Unit String) (isPronA isPronB : Prop) [Decidable isPronA] [Decidable isPronB] (a b : Core.Order.TreePath) : Prop

Coreference permission (restriction 10b) over a concrete tree.

a, b may corefer iff: if a k-commands b then b is a pronoun, and if b k-commands a then a is a pronoun. Omits the "non strict reflexive environment" qualification (non-reflexive coreference only), matching the abstract corefPermitted.

Equations

• Reinhart1976.corefPermittedAt t isPronA isPronB a b = (((a, b) ∈ Core.Order.Branching.cCommandAt t → isPronB) ∧ ((b, a) ∈ Core.Order.Branching.cCommandAt t → isPronA))

@[implicit_reducible]

instance Reinhart1976.instDecidableCorefPermittedAt (t : Syntax.Tree Unit String) (isPronA isPronB : Prop) [Decidable isPronA] [Decidable isPronB] (a b : Core.Order.TreePath) : Decidable (corefPermittedAt t isPronA isPronB a b)

Equations

• Reinhart1976.instDecidableCorefPermittedAt t isPronA isPronB a b = id inferInstance

The (11) paradigm (pp. 14-15)

Structure [S NP₁ [VP denied [S' NP₂ [VP' has met the Shah]]]], NP₁ at ⟨[0]⟩, NP₂ at ⟨[1,1,0]⟩. The matrix subject NP₁ k-commands NP₂ (not vice versa), so (10b) requires NP₂ to be a pronoun for coreference:

• (11a) Rosa denied that Rosa met the Shah. — blocked
• (11b) She denied that Rosa met the Shah. — blocked
• (11c) Rosa denied that she met the Shah. — permitted
• (11d) She denied that she met the Shah. — permitted

def Reinhart1976.deniedParadigm : Syntax.Tree Unit String

"NP₁ denied that NP₂ met the Shah": NP₁ at ⟨[0]⟩, NP₂ at ⟨[1,1,0]⟩.

Equations

• Reinhart1976.deniedParadigm = (Syntax.Tree.leaf "NP1").bin ((Syntax.Tree.leaf "denied").bin ((Syntax.Tree.leaf "NP2").bin (Syntax.Tree.leaf "metShah")))

theorem Reinhart1976.paradigm_11a_blocked : ¬corefPermittedAt deniedParadigm False False { toList := [0] } { toList := [1, 1, 0] }

(11a) Rosa₁ denied that Rosa₂ met the Shah: coref blocked. Rosa₂ is in the domain of Rosa₁ and is not a pronoun.

theorem Reinhart1976.paradigm_11b_blocked : ¬corefPermittedAt deniedParadigm True False { toList := [0] } { toList := [1, 1, 0] }

(11b) She₁ denied that Rosa₂ met the Shah: coref blocked. Rosa₂ is in the domain of She₁ and is not a pronoun.

theorem Reinhart1976.paradigm_11c_permitted : corefPermittedAt deniedParadigm False True { toList := [0] } { toList := [1, 1, 0] }

(11c) Rosa₁ denied that she₂ met the Shah: coref permitted. she₂ is in the domain of Rosa₁ but IS a pronoun.

theorem Reinhart1976.paradigm_11d_permitted : corefPermittedAt deniedParadigm True True { toList := [0] } { toList := [1, 1, 0] }

(11d) She₁ denied that she₂ met the Shah: coref permitted. she₂ is in the domain of She₁ but IS a pronoun.

Restriction (10a) — the pronoun-specific formulation (p. 14)

Two NP's in a non strict reflexive environment can be coreferential just in case one is a pronoun, the other is not and the non-pronoun is not in the domain of the pronoun.

(10a) applies only to pronoun–full NP pairs; [Rei76] argues (pp. 14-17) that (10b) is strictly superior — (10a) fails to block coreference between two full NPs when one is in the domain of the other (the (11a) case).

def Reinhart1976.corefPermittedAt_10a (t : Syntax.Tree Unit String) (isPronA isPronB : Prop) [Decidable isPronA] [Decidable isPronB] (a b : Core.Order.TreePath) : Prop

Restriction (10a): applies only to pronoun–full NP pairs. When exactly one NP is a pronoun, the non-pronoun must not be in the c-command domain of the pronoun; otherwise (10a) does not apply.

Equations

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

@[implicit_reducible]

instance Reinhart1976.instDecidableCorefPermittedAt_10a (t : Syntax.Tree Unit String) (isPronA isPronB : Prop) [Decidable isPronA] [Decidable isPronB] (a b : Core.Order.TreePath) : Decidable (corefPermittedAt_10a t isPronA isPronB a b)

Equations

• Reinhart1976.instDecidableCorefPermittedAt_10a t isPronA isPronB a b = id inferInstance

theorem Reinhart1976.restriction_10a_vs_10b : corefPermittedAt_10a deniedParadigm False False { toList := [0] } { toList := [1, 1, 0] } ∧ ¬corefPermittedAt deniedParadigm False False { toList := [0] } { toList := [1, 1, 0] }

Non-equivalence of (10a) and (10b): (10a) fails on the (11a) case. (10a) cannot block coreference between two full NPs (Rosa₁ … Rosa₂), because it only applies to pronoun–full NP pairs; (10b) correctly blocks it because Rosa₂ is in the domain of Rosa₁ and is not a pronoun.

theorem Reinhart1976.restriction_10b_subsumes_10a (t : Syntax.Tree Unit String) (isPronA isPronB : Prop) [Decidable isPronA] [Decidable isPronB] (a b : Core.Order.TreePath) (h : ¬corefPermittedAt_10a t isPronA isPronB a b) : ¬corefPermittedAt t isPronA isPronB a b

(10b) subsumes (10a): whenever (10a) blocks coreference, (10b) does too. The converse fails (restriction_10a_vs_10b), so (10b) is strictly more restrictive.