Command relations generated by categories

The command relations of the syntactic literature, reconstructed as generators on a category-labelled tree: a node S-commands whatever the lowest S above it dominates (Langacker's command), and likewise NP-command, K-command from the cyclic nodes S and NP, MAX-command from the maximal projections, and c-command from the branching nodes. Each is commandRelation on Branching.toTreeOrder generated by the positions carrying the relevant categories, so the Intersection Theorem identifies K-command with S-command ∩ NP-command, and Rouveret and Vergnaud's relation, which takes the lower of the first branching node and the first maximal projection, with c-command ∩ MAX-command.

References

• [barker-pullum-1990]
• [langacker-1969]
• [lasnik-1976]
• [rouveret-vergnaud-1980]

def Syntax.Tree.labeled {W : Type u_1} (t : Tree Cat W) (L : Set Cat) : Set Core.Order.TreePath

The positions of t whose category lies in L.

Equations

• t.labeled L = {p : Core.Order.TreePath | ∃ (s : Syntax.Tree Syntax.Cat W), Core.Order.Branching.subtreeAt t p.toList = some s ∧ s.cat ∈ L}

@[instance_reducible]

instance Syntax.Tree.instDecidableMemTreePathSetLabeledOfDecidablePredCat {W : Type u_1} (t : Tree Cat W) (L : Set Cat) [DecidablePred fun (x : Cat) => x ∈ L] (p : Core.Order.TreePath) : Decidable (p ∈ t.labeled L)

Equations

• t.instDecidableMemTreePathSetLabeledOfDecidablePredCat L p = match h : Core.Order.Branching.subtreeAt t p.toList with | none => isFalse ⋯ | some s => decidable_of_iff (s.cat ∈ L) ⋯

theorem Syntax.Tree.labeled_union {W : Type u_1} (t : Tree Cat W) (L₁ L₂ : Set Cat) : t.labeled (L₁ ∪ L₂) = t.labeled L₁ ∪ t.labeled L₂

@[reducible, inline]

abbrev Syntax.Tree.sCommand {W : Type u_1} (t : Tree Cat W) : Set (Core.Order.TreePath × Core.Order.TreePath)

Langacker's command: generated by the S nodes.

Equations

• t.sCommand = Core.Order.commandRelation (Core.Order.Branching.toTreeOrder t) (t.labeled {Syntax.Cat.S})

@[reducible, inline]

abbrev Syntax.Tree.npCommand {W : Type u_1} (t : Tree Cat W) : Set (Core.Order.TreePath × Core.Order.TreePath)

Generated by the NP nodes.

Equations

• t.npCommand = Core.Order.commandRelation (Core.Order.Branching.toTreeOrder t) (t.labeled {Syntax.Cat.NP})

@[reducible, inline]

abbrev Syntax.Tree.kCommand {W : Type u_1} (t : Tree Cat W) : Set (Core.Order.TreePath × Core.Order.TreePath)

Lasnik's kommand: generated by the cyclic nodes, S and NP.

Equations

• t.kCommand = Core.Order.commandRelation (Core.Order.Branching.toTreeOrder t) (t.labeled {Syntax.Cat.S, Syntax.Cat.NP})

@[reducible, inline]

abbrev Syntax.Tree.maxCommand {W : Type u_1} (t : Tree Cat W) (max : Set Cat) : Set (Core.Order.TreePath × Core.Order.TreePath)

Generated by the maximal projections max.

Equations

• t.maxCommand max = Core.Order.commandRelation (Core.Order.Branching.toTreeOrder t) (t.labeled max)

@[reducible, inline]

abbrev Syntax.Tree.rvCommand {W : Type u_1} (t : Tree Cat W) (max : Set Cat) : Set (Core.Order.TreePath × Core.Order.TreePath)

Rouveret and Vergnaud's c-command, generated by the branching nodes together with the maximal projections.

Equations

• t.rvCommand max = Core.Order.commandRelation (Core.Order.Branching.toTreeOrder t) ({p : Core.Order.TreePath | Core.Order.Branching.isBranchingAt t p} ∪ t.labeled max)

theorem Syntax.Tree.kCommand_eq {W : Type u_1} (t : Tree Cat W) : t.kCommand = t.sCommand ∩ t.npCommand

K-command is S-command ∩ NP-command.

theorem Syntax.Tree.rvCommand_eq {W : Type u_1} (t : Tree Cat W) (max : Set Cat) : t.rvCommand max = Core.Order.Branching.cCommandAt t ∩ t.maxCommand max

Rouveret and Vergnaud's relation is c-command ∩ MAX-command.