Crossings under random linearization

This file proves that if a sentence's word order were lost and replaced by a uniformly random one, the expected number of crossings would depend only on the arc structure: two links cross in a third of the linearizations when they share no endpoint, and in none otherwise. No tree hypothesis is needed; the identity holds for any link structure.

Main definitions

• Graph.crossingsUnder is the crossings g would show under a permutation of its positions.
• Graph.disjointLinkPairs is the number of unordered pairs of links sharing no endpoint — the pairs that can cross at all.

Main results

• Graph.crossings_relabel: the crossings of a relabelled graph are the crossings under the permutation.
• Graph.three_mul_sum_crossings_relabel: the expected-crossings identity 3 * ∑ σ, (g.relabel σ).crossings = n ! * g.disjointLinkPairs.

References

[FC17] — Random crossings in dependency trees, source of the expected-crossings identity (eq. 13) [FC13] — Hubiness, length, crossings and their relationships in syntactic dependencies, reduces the disjoint-pair count to the link count and the degree second moment

Crossings under a relabelling

def DependencyGrammar.Graph.crossingsUnder {n : ℕ} (g : Graph n) (σ : Equiv.Perm (Fin n)) : ℕ

The crossings g would show if its positions were rearranged by σ: crossing quadruples are scored in the positions σ assigns rather than in g's own.

Equations

• g.crossingsUnder σ = {x : Fin n × Fin n × Fin n × Fin n | g.Linked x.1 x.2.1 ∧ g.Linked x.2.2.1 x.2.2.2 ∧ DependencyGrammar.Alternate (σ x.1) (σ x.2.1) (σ x.2.2.1) (σ x.2.2.2)}.card

def DependencyGrammar.Graph.disjointLinkPairs {n : ℕ} (g : Graph n) : ℕ

The unordered pairs of links sharing no endpoint — the pairs that can cross at all, [FC17]'s potential crossings. Each pair is counted once, by the representative with both links least-endpoint-first and the earlier-starting link first.

Equations

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

@[simp]

theorem DependencyGrammar.Graph.crossingsUnder_one {n : ℕ} {g : Graph n} : g.crossingsUnder 1 = g.crossings

theorem DependencyGrammar.Graph.crossings_relabel {n : ℕ} {g : Graph n} (σ : Equiv.Perm (Fin n)) : (g.relabel σ).crossings = g.crossingsUnder σ

Relabelling moves the crossings to the relabelled positions.

One linearization in twenty-four alternates a distinct quadruple

Summing over linearizations, grouped by quadruple

Eight ordered witnesses per unordered disjoint pair

The expected-crossings identity

theorem DependencyGrammar.Graph.three_mul_sum_crossings_relabel {n : ℕ} {g : Graph n} : 3 * ∑ σ : Equiv.Perm (Fin n), (g.relabel σ).crossings = n.factorial * g.disjointLinkPairs

Expected crossings under random linearization ([FC17], eq. 13): summed over all n ! linearizations, three times the crossing count is n ! times the number of disjoint link pairs. So a uniformly random ordering expects a third of a crossing per pair of links sharing no endpoint, whatever the sentence's own order was.