Binding configurations of phrase-structure trees

On a phrase-structure tree a position commands another when it c-commands it in Reinhart's sense, neither dominating the other and every branching node above the first dominating the second. The binding domain of a position is bounded by a set of nodes: it holds the positions that every bounding node properly dominating the position dominates, the cone of the lowest such node. Theories of binding differ in the bounding nodes, which may depend on the position. With the clause nodes the domain is the minimal clause, the governing category of Government and Binding approximated; with the spell-out domains of phases it is the domain of Charnavel and Sportiche. More bounding nodes give smaller domains.

Main definitions

• PhraseStructure.Tree.configuration: c-command with the domain of each position bounded by a set of nodes.
• PhraseStructure.Tree.clauseConfiguration: the configuration bounded by the clause nodes.

Main statements

• PhraseStructure.Tree.configuration_anti: the configuration is antitone in the bounding nodes.

References

• [Rei76]
• [Cho81]
• [BP90]
• [CS16a]

def PhraseStructure.Tree.configuration {C : Type u_1} {W : Type u_2} (t : Tree C W) (P : Core.Order.TreePath → Set Core.Order.TreePath) : Binding.Configuration Core.Order.TreePath

The binding configuration of t bounded by P takes c-command as its command relation and gives a position b the domain that every node of P b properly dominating it dominates.

Equations

• t.configuration P = { commands := RoseTree.CCommands t, domain := fun (b : Core.Order.TreePath) => {a : Core.Order.TreePath | (b, a) ∈ PhraseStructure.commandRelation (P b)} }

@[instance_reducible]

instance PhraseStructure.Tree.instDecidableRelTreePathCommandsConfiguration {C : Type u_1} {W : Type u_2} (t : Tree C W) {P : Core.Order.TreePath → Set Core.Order.TreePath} : DecidableRel (t.configuration P).commands

Equations

• t.instDecidableRelTreePathCommandsConfiguration = PhraseStructure.Tree.instDecidableRelTreePathCommandsConfiguration._aux_1 t

@[instance_reducible]

instance PhraseStructure.Tree.instDecidablePredTreePathMemSetDomainConfiguration {C : Type u_1} {W : Type u_2} (t : Tree C W) {P : Core.Order.TreePath → Set Core.Order.TreePath} [(b : Core.Order.TreePath) → DecidablePred fun (x : Core.Order.TreePath) => x ∈ P b] (b : Core.Order.TreePath) : DecidablePred fun (x : Core.Order.TreePath) => x ∈ (t.configuration P).domain b

Equations

• t.instDecidablePredTreePathMemSetDomainConfiguration b a = { decide := decide (∀ x ∈ List.map Core.Order.TreePath.mk b.toList.inits, x ≠ b → x ∈ P b → x ≤ a), reflects_decide := ⋯ }

theorem PhraseStructure.Tree.configuration_anti {C : Type u_1} {W : Type u_2} (t : Tree C W) {P Q : Core.Order.TreePath → Set Core.Order.TreePath} (h : ∀ (b : Core.Order.TreePath), P b ⊆ Q b) : t.configuration Q ≤ t.configuration P

More bounding nodes give smaller domains and the same command.

@[reducible, inline]

abbrev PhraseStructure.Tree.clauseConfiguration {W : Type u_3} (t : Tree Cat W) : Binding.Configuration Core.Order.TreePath

The clause configuration of t is bounded by the clause nodes, so the binding domain of a position is the minimal clause containing it.

Equations

• t.clauseConfiguration = t.configuration fun (x : Core.Order.TreePath) => t.labeled {PhraseStructure.Cat.S}