Syntactic Graphs

@cite{adger-2025}

Graph-based representation of syntactic structure that generalizes across frameworks. Each node has a label and at most two children (1-part and 2-part), enforcing Dimensionality. In-degree is unbounded, permitting multiparthood — a single node simultaneously serving as part of multiple parents (@cite{adger-2025}).

Design

• Out-degree ≤ 2: each node has at most one 1-part (complement) and one 2-part (specifier). This is the Dimensionality axiom.
• In-degree unbounded: a node may be pointed to by multiple parents. This is multiparthood — the mechanism for movement in mereological syntax, distinct from both copies and multidominance.
• Framework predicates: isTree (in-degree ≤ 1, ≈ BPS), acyclic (required for well-formed structures). Trees are the special case.

Angular Locality

The central locality constraint (@cite{adger-2025}, definition 29):

If γ is a part, then γ can subjoin to β only if there is an α s.t.
γ is a n-part of α and α is a 1-part of β.

Crucially, "n-part" means transitive parthood within a single dimension. Transitivity does NOT cross dimensions: if x <₁ u and u <₂ e, then x is NOT a part of e in either dimension. This restriction is what makes Angular Locality derive island constraints, antilocality, and the impossibility of sideward/downward movement.

Relationship to Existing Types

• MereologicalSyntax.SynObj: tree-based, cannot express multiparthood. Embeds into SynGraph by construction.
• Minimalism.SyntacticObject: binary tree. Embeds as a SynGraph satisfying isTree.
• Core.Tree C W: n-ary tree for compositional interpretation, not a syntactic structure type.

structure SynGraph (L : Type) : Type

A syntactic graph with labeled nodes and dimensioned edges.

Nodes are indexed by Fin numNodes. Each node has a label of type L and at most two children: a 1-part (complement) and a 2-part (specifier). Multiple nodes may point to the same child — this is multiparthood.

• numNodes : Nat
• label : Fin self.numNodes → L
• onePart : Fin self.numNodes → Option (Fin self.numNodes)
• twoPart : Fin self.numNodes → Option (Fin self.numNodes)

def SynGraph.chain {L : Type} (g : SynGraph L) (f : Fin g.numNodes → Option (Fin g.numNodes)) (start : Fin g.numNodes) (fuel : Nat) : List (Fin g.numNodes)

Follow a single-dimension pointer chain from start, returning visited nodes (not including start). Fuel bounds traversal depth.

Equations

• g.chain f start 0 = []
• g.chain f start fuel.succ = match f start with | none => [] | some next => next :: g.chain f next fuel

def SynGraph.descendants {L : Type} (g : SynGraph L) (root : Fin g.numNodes) (fuel : Nat) : List (Fin g.numNodes)

All strict descendants of root reachable via 1-part and 2-part edges (cross-dimensional). May contain duplicates.

Equations

• One or more equations did not get rendered due to their size.
• g.descendants root 0 = (g.onePart root).toList ++ (g.twoPart root).toList

def SynGraph.isImm1PartOf {L : Type} (g : SynGraph L) (x y : Fin g.numNodes) : Bool

x is an immediate 1-part (complement) of y.

Equations

• g.isImm1PartOf x y = (g.onePart y == some x)

def SynGraph.isImm2PartOf {L : Type} (g : SynGraph L) (x y : Fin g.numNodes) : Bool

x is an immediate 2-part (specifier) of y.

Equations

• g.isImm2PartOf x y = (g.twoPart y == some x)

def SynGraph.isImmPartOf {L : Type} (g : SynGraph L) (x y : Fin g.numNodes) : Bool

x is an immediate part of y in either dimension.

Equations

• g.isImmPartOf x y = (g.isImm1PartOf x y || g.isImm2PartOf x y)

def SynGraph.isTrans1PartOf {L : Type} (g : SynGraph L) (x y : Fin g.numNodes) : Bool

x is a transitive 1-part of y (reachable via onePart only). Within-dimension transitivity without crossing dimensions.

Equations

• g.isTrans1PartOf x y = (g.chain g.onePart y g.numNodes).any fun (x_1 : Fin g.numNodes) => x_1 == x

def SynGraph.isTrans2PartOf {L : Type} (g : SynGraph L) (x y : Fin g.numNodes) : Bool

x is a transitive 2-part of y (reachable via twoPart only). Within-dimension transitivity without crossing dimensions.

Equations

• g.isTrans2PartOf x y = (g.chain g.twoPart y g.numNodes).any fun (x_1 : Fin g.numNodes) => x_1 == x

def SynGraph.isWithinDimPartOf {L : Type} (g : SynGraph L) (x y : Fin g.numNodes) : Bool

x is a within-dimension transitive n-part of y for some n. This is the parthood relation relevant to Angular Locality: γ is reachable from α by following ONLY 1-part edges or ONLY 2-part edges, never crossing dimensions (@cite{adger-2025}, p. 95).

Equations

• g.isWithinDimPartOf x y = (g.isTrans1PartOf x y || g.isTrans2PartOf x y)

def SynGraph.isTransPartOf {L : Type} (g : SynGraph L) (x y : Fin g.numNodes) : Bool

x is a transitive part of y (reachable via any combination of 1-part and 2-part edges). Cross-dimensional — NOT the parthood relation used by Angular Locality.

Equations

• g.isTransPartOf x y = (g.descendants y g.numNodes).any fun (x_1 : Fin g.numNodes) => x_1 == x

def SynGraph.parentCount {L : Type} (g : SynGraph L) (target : Fin g.numNodes) : Nat

Number of parents of target (nodes pointing to it via either edge).

Equations

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

def SynGraph.isMultipart {L : Type} (g : SynGraph L) (i : Fin g.numNodes) : Bool

Node i is multiply dominated — more than one parent. This is multiparthood: the node occupies multiple structural positions simultaneously, not by copying but by being pointed to twice.

Equations

• g.isMultipart i = decide (g.parentCount i > 1)

def SynGraph.onePartChain {L : Type} (g : SynGraph L) (root : Fin g.numNodes) : List L

Labels along the 1-part chain from root, including root itself. Corresponds to @cite{grimshaw-2005}'s Extended Projection: the sequence N <₁ Cl <₁ Q <₁ D emerges from successive 1-parts.

Equations

• g.onePartChain root = g.label root :: List.map g.label (g.chain g.onePart root g.numNodes)

def SynGraph.containsLabel {L : Type} [BEq L] (g : SynGraph L) (l : L) (root : Fin g.numNodes) : Bool

Does the subtree rooted at root contain a node labeled l?

Equations

• g.containsLabel l root = (g.label root == l || (g.descendants root g.numNodes).any fun (i : Fin g.numNodes) => g.label i == l)

def SynGraph.satisfiesAL {L : Type} (g : SynGraph L) (γ β : Fin g.numNodes) : Bool

Angular Locality (@cite{adger-2025}, definition 29, p. 91):

If γ is a part, then γ can subjoin to β only if there is an α s.t. γ is a n-part of α and α is a 1-part of β.

"n-part" means transitive parthood within a single dimension. Transitivity does NOT cross dimensions (@cite{adger-2025}, p. 95): if x <₁ u and u <₂ e, x is neither a 1-part nor a 2-part of e.

This derives:

• Antilocality (complement-to-specifier of same head)
• No sideward movement (to a specifier/2-part)
• No downward movement
• No parallel merge (to an unattached object)
• No long-distance movement across Extended Projections — all without stipulating phases or PIC.

Equations

• g.satisfiesAL γ β = (g.chain g.onePart β g.numNodes).any fun (α : Fin g.numNodes) => g.isWithinDimPartOf γ α

def SynGraph.subjoin {L : Type} (g : SynGraph L) (x y : Fin g.numNodes) : Option (SynGraph L)

External subjoin: make x a part of y in the next available dimension. Returns none if y already has two parts (Dimensionality violation) or if x == y (irreflexivity).

Equations

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

def SynGraph.internalSubjoin {L : Type} (g : SynGraph L) (γ β : Fin g.numNodes) : Option (SynGraph L)

Internal subjoin: subjoin γ to β only if Angular Locality is satisfied. Models movement — the element already exists and is re-subjoined to a higher position, creating multiparthood.

Equations

• g.internalSubjoin γ β = if g.satisfiesAL γ β = true then g.subjoin γ β else none

def SynGraph.acyclic {L : Type} (g : SynGraph L) : Bool

No node is a descendant of itself.

Equations

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

def SynGraph.maxInDegree1 {L : Type} (g : SynGraph L) : Bool

Every node has in-degree ≤ 1 (at most one parent).

Equations

• g.maxInDegree1 = (List.range g.numNodes).all fun (i : Nat) => if h : i < g.numNodes then decide (g.parentCount ⟨i, h⟩ ≤ 1) else true

def SynGraph.isTree {L : Type} (g : SynGraph L) : Bool

The graph is a tree: acyclic with in-degree ≤ 1 everywhere. Minimalism.SyntacticObject and MereologicalSyntax.SynObj both satisfy this. Mereological structures with multiparthood do NOT.

Equations

• g.isTree = (g.acyclic && g.maxInDegree1)

def SynGraph.isMereological {L : Type} (g : SynGraph L) : Bool

Well-formed mereological structure: acyclic, but multiparthood (in-degree > 1) is permitted.

Equations

• g.isMereological = g.acyclic

The five key results derived from Angular Locality in @cite{adger-2025}, Chapter 4, list (35), p. 93. Each is demonstrated on a concrete SynGraph and verified by native_decide.

We construct small graphs with specific edge configurations and verify that satisfiesAL returns the expected result.

@[reducible, inline]

abbrev N : Type

Equations

• N = Nat

def mkGraph (n : Nat) (ones twos : List (Fin n × Fin n)) : SynGraph N

Helper: build a SynGraph from edge lists.

Equations

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

Structure (28), @cite{adger-2025} p. 90: a (0) ──1──▶ b (1)

b trying to subjoin to a. AL requires an α that is a 1-part of a
such that b is a within-dim n-part of α. The only 1-part of a is b
itself, and b is not a part of itself. AL fails. 

theorem al_blocks_superlocal : g_superlocal✝.satisfiesAL ⟨1, ⋯⟩ ⟨0, ⋯⟩ = false

Structure (31a), @cite{adger-2025} p. 92: c (0) ──1──▶ b (1), c (0) ──2──▶ a (2)

a trying to subjoin to b (sibling). b has no 1-parts, so the
candidate α set is empty. AL fails. 

theorem al_blocks_sideward : g_sideward✝.satisfiesAL ⟨2, ⋯⟩ ⟨1, ⋯⟩ = false

@cite{adger-2025} p. 91 (30): subjunction to an unattached object. a (0) ──1──▶ b (1); c (2) disconnected.

c trying to subjoin to a. a's 1-part chain = [b]. c is not a
within-dim part of b. AL fails. 

theorem al_blocks_parallel : g_parallel✝.satisfiesAL ⟨2, ⋯⟩ ⟨0, ⋯⟩ = false

Structure (38), @cite{adger-2025} p. 95: y (0) ──1──▶ e (1) ──1──▶ w (3) e (1) ──2──▶ u (2) ──2──▶ z (4) u (2) ──1──▶ x (5)

The paper states: "u is a 2-part of e", "z is a 2-part of u",
"x is a 1-part of u."

z CAN subjoin to y: α = e is a 1-part of y. z <₂ u <₂ e
(transitive 2-part of e, within dimension 2). AL satisfied.

x CANNOT subjoin to y: x <₁ u, u <₂ e. "Since transitivity does
not cross dimensions, x is neither a 2-part nor a 1-part of e"
(p. 95). The corrected `satisfiesAL` using within-dimension chains
correctly rejects this; the old version using `descendants` would
have incorrectly allowed it. 

theorem al_allows_within_dim : g_crossdim✝.satisfiesAL ⟨4, ⋯⟩ ⟨0, ⋯⟩ = true

z (transitive 2-part of e) CAN subjoin to y.

theorem al_blocks_cross_dim : g_crossdim✝.satisfiesAL ⟨5, ⋯⟩ ⟨0, ⋯⟩ = false

x (cross-dimensional from e) CANNOT subjoin to y. This is the critical test that distinguishes the corrected AL from the buggy version: x <₁ u <₂ e crosses dimensions, so x is not a within-dimension part of e.

Structure (32), @cite{adger-2025} p. 92: e (0) ──1──▶ a (1) ──1──▶ d (3) e (0) ──2──▶ f (2) a (1) ──2──▶ b (4) ──1──▶ c (5) ──1──▶ g (6)

d trying to subjoin to c (lowering). c's 1-part chain = [g].
d is not a within-dim part of g. AL fails. 

theorem al_blocks_lowering : g_lowering✝.satisfiesAL ⟨3, ⋯⟩ ⟨5, ⋯⟩ = false

Structure (24a), @cite{adger-2025} p. 89: e (0) ──1──▶ d (1) ──1──▶ a (2) ──1──▶ c (3) ──2──▶ b (4)

b subjoins to e: a is in e's 1-part chain, b <₂ a. AL satisfied.
c subjoins to e: a is in e's 1-part chain, c <₁ a. AL satisfied. 

theorem al_allows_rollup_2part : g_rollup✝.satisfiesAL ⟨4, ⋯⟩ ⟨0, ⋯⟩ = true

Roll-up: b (2-part of a) CAN subjoin to e.

theorem al_allows_rollup_1part : g_rollup✝.satisfiesAL ⟨3, ⋯⟩ ⟨0, ⋯⟩ = true

Roll-up: c (1-part of a) CAN subjoin to e.

@cite{adger-2025}, Chapter 4.3: Angular Locality forces successive- cyclic movement across clause boundaries. Within a single Extended Projection (EP), movement is unrestricted — the 1-part chain connects everything. But when movement crosses from an embedded EP to a matrix EP (connected via a 2-part edge), AL blocks direct movement.

Cross-clausal structure: Matrix: C₁(0) ──1──▶ T₁(1) ──1──▶ v₁(2) ──1──▶ V₁(3) T₁(1) ──2──▶ subj(4) Embedded: C₂(5) ──1──▶ T₂(6) ──1──▶ v₂(7) ──1──▶ V₂(8) Link: v₁(2) ──2──▶ C₂(5) ← embedded CP is 2-part of matrix v wh(9) is a 2-part of v₂(7).

wh CANNOT reach C₁ directly: C₁'s 1-part chain = [T₁, v₁, V₁].
wh is in the embedded EP, connected to v₁ only via C₂ which is a
2-part of v₁ — cross-dimensional, so invisible to AL.

wh CAN reach C₂ (same EP — within-dim 2-part of v₂, v₂ <₁ T₂ <₁ C₂).
After wh subjoins to C₂ (becoming C₂'s 2-part), wh <₂ C₂ <₂ v₁,
making wh a transitive 2-part of v₁. Since v₁ is in C₁'s 1-part
chain, wh can NOW reach C₁. This is successive cyclicity: the
intermediate stop at C₂ is forced by AL. 

theorem succ_cyc_blocked_cross_clause : g_succ_cyc_0✝.satisfiesAL ⟨9, ⋯⟩ ⟨0, ⋯⟩ = false

wh CANNOT reach matrix C₁ directly — cross-clausal boundary.

theorem succ_cyc_wh_reaches_embedded_C : g_succ_cyc_0✝.satisfiesAL ⟨9, ⋯⟩ ⟨5, ⋯⟩ = true

wh CAN reach embedded C₂ — within the same EP.

theorem succ_cyc_wh_reaches_C1_after_stop : g_succ_cyc_1✝.satisfiesAL ⟨9, ⋯⟩ ⟨0, ⋯⟩ = true

After stopping at C₂, wh CAN now reach matrix C₁. This is successive cyclicity: the C₂ intermediate landing site is forced by AL, just as phase edges force cyclic movement in Minimalism.

@cite{adger-2025}, Chapter 6: When D has a 2-part (because Det/Dem subjoins to it), its 2-part slot is "used up." The mechanism has two parts:

1. wh CAN satisfy AL for D (wh <₂ P, P is D's 1-part), so AL alone does not block movement. But D already has both parts filled (Dimensionality blocks subjoin).
2. wh CANNOT satisfy AL for any node above D (C, T), because D is connected to the matrix clause via a 2-part edge, and the path from wh through D to v crosses dimensions.

This derives the Specificity Condition: definite nominals (whose D has a 2-part) are islands, indefinite ones (free 2-part) are transparent.

Structure: C (0) ──1──▶ T (1) ──1──▶ v (2) ──1──▶ V (3) T (1) ──2──▶ subj (4) v (2) ──2──▶ D (5) ──1──▶ P (6) ──1──▶ N (7) D (5) ──2──▶ Det (8) P (6) ──2──▶ wh (9)

theorem nominal_island_definite_blocks : g_definite_island✝.satisfiesAL ⟨9, ⋯⟩ ⟨0, ⋯⟩ = false

wh CANNOT reach matrix C when D has a 2-part (definite = island). The path wh <₂ P <₁ D <₂ v crosses dimensions, so wh is not a within-dimension part of any node in C's 1-part chain.

theorem nominal_island_d_full : g_definite_island✝.internalSubjoin ⟨9, ⋯⟩ ⟨5, ⋯⟩ = none

wh satisfies AL for D (wh <₂ P, P <₁ D), but D is full — internalSubjoin returns none because Dimensionality blocks it.

Indefinite structure: D has no 2-part (Det does not subjoin). wh can subjoin to D, filling its free 2-part slot.

theorem nominal_island_indefinite_allows : g_indefinite_transparent✝.satisfiesAL ⟨9, ⋯⟩ ⟨5, ⋯⟩ = true

wh CAN reach D when D has a free 2-part (indefinite = transparent).

theorem nominal_island_indefinite_reaches_C : g_indefinite_after✝.satisfiesAL ⟨9, ⋯⟩ ⟨0, ⋯⟩ = true

@cite{adger-2025}, Chapter 6: Extraction from within a subject DP is blocked because the path from the extracted element to the matrix clause crosses dimensions.

Structure: C (0) ──1──▶ T (1) ──1──▶ v (2) ──1──▶ V (3) T (1) ──2──▶ DP_subj (4) ──1──▶ NP (5) ──1──▶ N_friend (6) NP (5) ──2──▶ PP (7) ──1──▶ N_who (8)

"*Who did [a friend of t] arrive?" — extraction of N_who from within the subject DP.

The path N_who(8) <₁ PP(7) <₂ NP(5) <₁ DP(4) <₂ T(1) crosses dimensions twice. N_who is not a within-dimension transitive part of any node in C's 1-part chain [T, v, V].

Crucially, the SUBJECT DP ITSELF can extract (it is T's 2-part): this correctly predicts "Who [t arrived]?" is grammatical.

theorem subject_island_blocks : g_subject_island✝.satisfiesAL ⟨8, ⋯⟩ ⟨0, ⋯⟩ = false

Extraction from within a subject is blocked: N_who CANNOT reach C. The cross-dimensional path N_who <₁ PP <₂ NP <₁ DP <₂ T prevents N_who from being a within-dimension transitive part of any α in C's 1-part chain.

theorem subject_itself_can_extract : g_subject_island✝.satisfiesAL ⟨4, ⋯⟩ ⟨0, ⋯⟩ = true

The subject DP itself CAN reach C (it is T's 2-part, and T is in C's 1-part chain). Subjects can extract, just not their subparts.

@cite{adger-2025}, Chapter 6: Extraction from within an adjunct is blocked by the same cross-dimensional mechanism as subject islands.

Structure: C (0) ──1──▶ T (1) ──1──▶ v (2) ──1──▶ V (3) T (1) ──2──▶ subj (4) v (2) ──2──▶ AdvP (5) ──1──▶ PP (6) ──1──▶ NP_wh (7)

"*What did John arrive [after fixing t]?" — extraction of NP_wh from the adjunct AdvP.

The path NP_wh(7) <₁ PP(6) <₁ AdvP(5) <₂ v(2) crosses dimensions at the AdvP-to-v boundary. Within v's 2-part chain: AdvP is there, but NP_wh is not (NP_wh is in AdvP's 1-part chain, not its 2-part chain).

theorem adjunct_island_blocks : g_adjunct_island✝.satisfiesAL ⟨7, ⋯⟩ ⟨0, ⋯⟩ = false

Extraction from within an adjunct is blocked: NP_wh CANNOT reach C.

theorem adjunct_itself_can_extract : g_adjunct_island✝.satisfiesAL ⟨5, ⋯⟩ ⟨0, ⋯⟩ = true

The adjunct AdvP itself CAN reach C (it is v's 2-part, and v is in C's 1-part chain). Adjuncts can be fronted, just not extracted from.

Antilocality: complement-to-specifier movement within the same head is always blocked. This is (35a) stated as a general test: for any 2-node structure where β has exactly one 1-part γ and no further substructure, γ cannot re-subjoin to β. The only candidate α (γ itself) fails because γ is not a part of itself.

We verify this for minimal structures of each shape: sub₁ and sub₁₂.

theorem antilocality_sub1 : let g := mkGraph 2 [(⟨0, ⋯⟩, ⟨1, ⋯⟩)] []; g.satisfiesAL ⟨1, ⋯⟩ ⟨0, ⋯⟩ = false

Antilocality for a bare sub₁: the sole complement cannot re-subjoin.

theorem antilocality_sub12 : let g := mkGraph 3 [(⟨0, ⋯⟩, ⟨1, ⋯⟩)] [(⟨0, ⋯⟩, ⟨2, ⋯⟩)]; g.satisfiesAL ⟨1, ⋯⟩ ⟨0, ⋯⟩ = false ∧ g.satisfiesAL ⟨2, ⋯⟩ ⟨0, ⋯⟩ = false

Antilocality for sub₁₂: neither the complement nor the specifier can re-subjoin to the head.