Tree Orders

[BP90]'s framework-agnostic notion of a syntactic tree: a set of nodes equipped with a dominance partial order. This is the carrier on which command relations (Core.Order.commandRelation) are defined.

The structure is framework-agnostic — Minimalism, HPSG, Dependency Grammar, CCG, and Construction Grammar each pick a node type with a PartialOrder instance giving dominance, then inherit the entire B&P theory of command relations as a free corollary.

The dominance order is supplied by [PartialOrder Node] — reflexivity, antisymmetry, and transitivity come from le_refl/le_antisymm/le_trans. A TreeOrder only adds what is tree-specific: a designated root, the nodes subset that participates in the tree, the Connected Ancestor Condition (CAC), and dominance closure on nodes.

The CAC is what B&P's Constituency Theorem (Theorem 7), the Embeddability Theorem (Theorem 8), and the reverse direction of the Union Theorem (Theorem 9) require; Boundedness (Theorem 4) uses only the root.

Main Definitions

• TreeOrder Node — [PartialOrder Node] plus a designated root, a nodes : Set Node subset, the CAC, and dominance closure.
• TreeOrder.properDom — strict dominance, a ≤ b ∧ a ≠ b.
• upperBounds — proper P-dominators of a node.

structure Core.Order.TreeOrder (Node : Type u_1) [PartialOrder Node] : Type u_1

Tree-shaped subset of a partially-ordered Node type ([BP90] Definitions 1 and 15 consolidated: Def 1 is the Wall-style tree — Single Root, Exclusivity, Nontangling — and Def 15 is the CAC, which B&P prove Def-1 trees entail, p. 22).

The dominance order is (· ≤ ·) from [PartialOrder Node]; this structure adds tree-specific data: a designated root, the nodes subset, and the Connected Ancestor Condition (CAC).

Reflexivity (a ≤ a), antisymmetry, and transitivity of dominance are inherited from PartialOrder and are not restipulated here.

• nodes : Set Node

  The set of nodes that belong to this tree.

• root : Node

  The designated root node.

• root_in_nodes : self.root ∈ self.nodes

  The root belongs to the tree.

• root_le_all (a : Node) : a ∈ self.nodes → self.root ≤ a

  The root dominates every node in the tree.

• ancestor_connected (x y z : Node) : x ≤ z → y ≤ z → x ≤ y ∨ y ≤ x

  Connected Ancestor Condition (CAC): if both x and y dominate z, then x ≤ y or y ≤ x. Ancestors are linearly ordered.

def Core.Order.TreeOrder.properDom {Node : Type u_1} [PartialOrder Node] (_T : TreeOrder Node) (a b : Node) : Prop

Proper dominance: a properly dominates b iff a ≤ b and a ≠ b. Definitionally equal to < on the underlying partial order via lt_iff_le_and_ne, but kept as a named And so destructuring with .1/.2 works in proofs.

Equations

• _T.properDom a b = (a ≤ b ∧ a ≠ b)

def Core.Order.upperBounds {Node : Type u_1} [PartialOrder Node] (T : TreeOrder Node) (a : Node) (P : Set Node) : Set Node

Upper bounds of a node with respect to property P ([BP90] Definition 2).

UB(a, P) = {b | b properly dominates a ∧ b ∈ P}.

Equations

• Core.Order.upperBounds T a P = {b : Node | T.properDom b a ∧ b ∈ P}

@[reducible]

def Core.Order.TreeOrder.toIsLeftLinear {Node : Type u_1} [PartialOrder Node] (T : TreeOrder Node) : IsLeftLinear Node

A TreeOrder's Connected Ancestor Condition is exactly left-linearity: the syntactic-tree CAC and the branching-time no-backward-branching axiom are one and the same. Use haveI := T.toIsLeftLinear to inherit IsLeftLinear.isChain_Iio ("ancestors are linearly ordered") on the node type.

Equations

• ⋯ = ⋯