|
| 1 | +(* SPDX-License-Identifier: MPL-2.0 *) |
| 2 | +(* braid_equiv.ml — decide braid-GROUP equivalence of braid words via Dehornoy |
| 3 | + * handle reduction. |
| 4 | + * |
| 5 | + * TG-7, NON-SEMANTIC rung. The language's `==` on braids (eval.ml `VBraid` |
| 6 | + * equality and the Lean `Step.eqBraids` rule) is LIST equality and is left |
| 7 | + * UNCHANGED by this module — `braid_equiv` is an out-of-band decision procedure |
| 8 | + * for callers who want true braid-group equivalence (e.g. tooling, future |
| 9 | + * `compute`-style checks). Changing `==` itself to use this is a separate |
| 10 | + * language-design decision (see PROOF-NEEDS.md TG-7). |
| 11 | + * |
| 12 | + * Algorithm (Dehornoy 1997, "A fast method for comparing braids"). A braid |
| 13 | + * word on σ₁,σ₂,… A σᵢ-handle is a factor |
| 14 | + * σᵢ^e · w₀ · σ_{i+1}^d · w₁ · σ_{i+1}^d · ⋯ · σ_{i+1}^d · w_m · σᵢ^{-e} |
| 15 | + * with e,d ∈ {±1}, where every wₖ uses only generators σⱼ with j ≥ i+2 (so the |
| 16 | + * interior contains no σᵢ, no σ_{<i}, and the σ_{i+1} all share the sign d). It |
| 17 | + * reduces to |
| 18 | + * w₀ · (σ_{i+1}^{-e} σᵢ^d σ_{i+1}^e) · w₁ · ⋯ · (σ_{i+1}^{-e} σᵢ^d σ_{i+1}^e) · w_m |
| 19 | + * (the m = 0 case is plain free cancellation σᵢ^e wₐ σᵢ^{-e} → wₐ). Handle |
| 20 | + * reduction terminates and a reduced word is empty iff the braid is trivial, so |
| 21 | + * equiv u v ⇔ reduce (u · v⁻¹) = ε. |
| 22 | + * |
| 23 | + * Correctness here is established BY TESTING (compiler/test/tg7): the defining |
| 24 | + * relations, randomly-constructed equivalent pairs (ground truth from the group |
| 25 | + * relations), and the writhe/permutation invariants. A mechanised Garside/ |
| 26 | + * Dehornoy correctness proof in Lean is the research-grade rung and is NOT |
| 27 | + * claimed. A safety step-bound guards against any non-termination surprise. |
| 28 | + *) |
| 29 | + |
| 30 | +(* A braid word as a list of UNIT letters (index ≥ 1, sign ±1). *) |
| 31 | +type letter = { idx : int; sgn : int } |
| 32 | + |
| 33 | +let units_of (gs : Ast.generator list) : letter list = |
| 34 | + List.concat_map (fun (g : Ast.generator) -> |
| 35 | + let s = if g.gen_exponent >= 0 then 1 else -1 in |
| 36 | + List.init (abs g.gen_exponent) (fun _ -> { idx = g.gen_index; sgn = s })) gs |
| 37 | + |
| 38 | +(* inverse braid: reverse order, negate each sign. (ab)⁻¹ = b⁻¹a⁻¹. *) |
| 39 | +let inverse (w : letter list) : letter list = |
| 40 | + List.rev_map (fun l -> { l with sgn = - l.sgn }) w |
| 41 | + |
| 42 | +(* free reduction: cancel adjacent σ·σ⁻¹. Sound (group inverses); keeps words |
| 43 | + short. (Adjacent cancellation is itself the empty-interior handle case, but |
| 44 | + doing it eagerly speeds convergence.) *) |
| 45 | +let free_reduce (w : letter list) : letter list = |
| 46 | + List.fold_right (fun x acc -> |
| 47 | + match acc with |
| 48 | + | y :: rest when x.idx = y.idx && x.sgn = - y.sgn -> rest |
| 49 | + | _ -> x :: acc) w [] |
| 50 | + |
| 51 | +(* Find and reduce the leftmost handle. Returns None if the word is handle-free. *) |
| 52 | +let reduce_one (w : letter list) : letter list option = |
| 53 | + let arr = Array.of_list w in |
| 54 | + let n = Array.length arr in |
| 55 | + (* Does position [a] open a handle? If so return its closing index [b]. *) |
| 56 | + let handle_at a = |
| 57 | + let i = arr.(a).idx and e = arr.(a).sgn in |
| 58 | + let rec scan k d_opt = |
| 59 | + if k >= n then None (* no close → not a handle *) |
| 60 | + else |
| 61 | + let j = arr.(k).idx and s = arr.(k).sgn in |
| 62 | + if j = i then (if s = -e then Some k else None) (* close, or same-sign σᵢ → blocked *) |
| 63 | + else if j < i then None (* σ_{<i} inside → blocked *) |
| 64 | + else if j = i + 1 then |
| 65 | + (match d_opt with |
| 66 | + | None -> scan (k + 1) (Some s) |
| 67 | + | Some d -> if d = s then scan (k + 1) d_opt else None) (* mixed σ_{i+1} signs *) |
| 68 | + else scan (k + 1) d_opt (* j ≥ i+2 → interior wₖ, ok *) |
| 69 | + in |
| 70 | + scan (a + 1) None |
| 71 | + in |
| 72 | + let rec find a = |
| 73 | + if a >= n then None |
| 74 | + else match handle_at a with Some b -> Some (a, b) | None -> find (a + 1) |
| 75 | + in |
| 76 | + match find 0 with |
| 77 | + | None -> None |
| 78 | + | Some (a, b) -> |
| 79 | + let i = arr.(a).idx and e = arr.(a).sgn in |
| 80 | + let interior = Array.to_list (Array.sub arr (a + 1) (b - a - 1)) in |
| 81 | + let rewritten = |
| 82 | + List.concat_map (fun l -> |
| 83 | + if l.idx = i + 1 then |
| 84 | + (* σ_{i+1}^d → σ_{i+1}^{-e} σᵢ^d σ_{i+1}^e *) |
| 85 | + [ { idx = i + 1; sgn = -e }; { idx = i; sgn = l.sgn }; { idx = i + 1; sgn = e } ] |
| 86 | + else [ l ]) interior |
| 87 | + in |
| 88 | + let prefix = Array.to_list (Array.sub arr 0 a) in |
| 89 | + let suffix = Array.to_list (Array.sub arr (b + 1) (n - b - 1)) in |
| 90 | + Some (prefix @ rewritten @ suffix) |
| 91 | + |
| 92 | +let default_max_steps = 1_000_000 |
| 93 | + |
| 94 | +(* Reduce to a handle-free (and freely-reduced) word. *) |
| 95 | +let reduce ?(max_steps = default_max_steps) (w0 : letter list) : letter list = |
| 96 | + let rec loop steps w = |
| 97 | + if steps <= 0 then w (* safety net; never hit in tests *) |
| 98 | + else match reduce_one w with |
| 99 | + | None -> w |
| 100 | + | Some w' -> loop (steps - 1) (free_reduce w') |
| 101 | + in |
| 102 | + loop max_steps (free_reduce w0) |
| 103 | + |
| 104 | +(* A braid word is trivial (= identity) iff it reduces to the empty word. *) |
| 105 | +let is_trivial_word (w : letter list) : bool = reduce w = [] |
| 106 | + |
| 107 | +let is_trivial (gs : Ast.generator list) : bool = is_trivial_word (units_of gs) |
| 108 | + |
| 109 | +(* u ≡ v in the braid group ⇔ u·v⁻¹ is trivial. *) |
| 110 | +let equiv (u : Ast.generator list) (v : Ast.generator list) : bool = |
| 111 | + is_trivial_word (units_of u @ inverse (units_of v)) |
| 112 | + |
| 113 | +(* ---- invariants (necessary conditions; exposed for callers/tests) ---- *) |
| 114 | + |
| 115 | +(* writhe = exponent sum (abelianisation); invariant under braid relations. *) |
| 116 | +let writhe (gs : Ast.generator list) : int = |
| 117 | + List.fold_left (fun a (g : Ast.generator) -> a + g.gen_exponent) 0 gs |
| 118 | + |
| 119 | +(* underlying permutation on 1..n as an array p where p.(k-1) = image of strand k; |
| 120 | + each σᵢ (any sign) transposes strands i,i+1. *) |
| 121 | +let permutation ~(strands : int) (gs : Ast.generator list) : int array = |
| 122 | + let p = Array.init strands (fun k -> k + 1) in |
| 123 | + List.iter (fun (g : Ast.generator) -> |
| 124 | + let i = g.gen_index in |
| 125 | + if i >= 1 && i < strands then begin |
| 126 | + let t = p.(i - 1) in p.(i - 1) <- p.(i); p.(i) <- t |
| 127 | + end) gs; |
| 128 | + p |
0 commit comments