From 3cb61a1859556846e0bb574eb25855224014bed5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 01:41:51 +0000 Subject: [PATCH 1/5] WIP: Consolidate structural_similarity into the intent_linearity registry as --- src/v2/lens/intent_linearity.dag | 17 +++- src/v2/lens/structural_similarity.dag | 82 +++++++++--------- .../structural_similarity/sg_claims_test.dag | 22 ----- .../lens_unit/discriminators_test.dag | 14 +++ .../lens_unit/discriminators_test.dag | 85 +++++++++++++++++++ 5 files changed, 153 insertions(+), 67 deletions(-) delete mode 100644 src/v2/lens/structural_similarity/sg_claims_test.dag create mode 100644 src/v2/test/claim/structural_similarity/lens_unit/discriminators_test.dag diff --git a/src/v2/lens/intent_linearity.dag b/src/v2/lens/intent_linearity.dag index deb469de15b..003251fd52e 100644 --- a/src/v2/lens/intent_linearity.dag +++ b/src/v2/lens/intent_linearity.dag @@ -1,6 +1,7 @@ module v2.lens.intent_linearity import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } import v2.lens.simulated_relationship { chain_is_simulated } +import v2.lens.structural_similarity { type_decls_anti_unify } import v2.std.node { Node, Symbol } import v2.std.algebra { FreeMonoid, length, fold_list } import v2.std.logic { Bool } @@ -8,7 +9,8 @@ import v2.std.logic { Bool } // Intent-linearity enforcer: a program's description should equal its irreducible information content // (minimal template + distinct data), recursively at every level -- intent 1:1 with its inputs. This is // the registry the redundancy lenses become ROWS of (so the enforcer is itself linear: one engine, N -// rows, not a fork). Row 1 = the hand-unrolled fold; complexity cost-recurrence rules join later. +// rows, not a fork). Row 1 = the hand-unrolled fold (term layer); Row 2 = duplicate type declarations +// (type-decl layer) -- one anti-unification engine, two binders; complexity cost-recurrence rules join later. // The §1 time-axis a rule's minimal form reduces (change-time = §2 maintenance; run-time = §1 cost). type CostAxis = ChangeTime | RunTime @@ -29,8 +31,19 @@ fn unroll_to_fold_rule() -> LinearityRule { } } +// Row 2 — duplicate TYPE declarations (change-time). detect reuses structural_similarity's type-decl +// binder over the same `congruent` kernel; minimal form = one generic over the leaf that varies across +// the congruent family (the §3 nickname / `Int8`..`Int128` collapse to one `Compose` axis). +fn dup_type_to_generic_rule() -> LinearityRule { + LinearityRule { + name: ^dup_type_to_generic, + axis: ChangeTime, + detect: fn(s) { type_decls_anti_unify(decls: s) } + } +} + fn linearity_registry() -> FreeMonoid { - [ unroll_to_fold_rule() ] + [ unroll_to_fold_rule(), dup_type_to_generic_rule() ] } // typed projector (avoids field access on a fold lambda element) diff --git a/src/v2/lens/structural_similarity.dag b/src/v2/lens/structural_similarity.dag index 446a5051403..d1f9e587b0a 100644 --- a/src/v2/lens/structural_similarity.dag +++ b/src/v2/lens/structural_similarity.dag @@ -1,53 +1,49 @@ module v2.lens.structural_similarity import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } -import v2.std.collection { List, Map } -import v2.std.nat { Nat, Zero } -import v2.std.node { Symbol } - -type DeclId = Symbol - -type TypeIdent = Symbol - -type VariantShape { - field_arity: Nat - field_type_idents: List -} - -type TypeShape { - variant_set: List - total_variants: Nat -} - -type FnShapeUnrealized {} - -type StructuralShape - = TypeDecl { shape: TypeShape } - | FnDecl { shape: FnShapeUnrealized } - -type StructuralSimilarityVerdict - = Unrealized - | Produced { index: Map } - -type StructuralSimilarityFact { - verdict: StructuralSimilarityVerdict -} - -data structural_similarity_empty_type_shape: TypeShape = { - variant_set: [], - total_variants: Zero -} - -fn structural_similarity_fact() -> StructuralSimilarityFact { - StructuralSimilarityFact { - verdict: Unrealized +import v2.lens.simulated_relationship { congruent } +import v2.std.node { Node } +import v2.std.algebra { FreeMonoid, length, skip, is_prefix_of } +import v2.std.logic { Bool } + +// §2-horizontal / §3-nicknaming detector at the TYPE-DECLARATION layer -- the type-decl +// twin of v2.lens.simulated_relationship (which targets statement chains inside a body). +// Same anti-unification engine -- `congruent`, the shared kernel seeded in +// simulated_relationship -- a different BINDER: the leaves that vary across a congruent +// family of type decls are not a fold's list-element hole but a TYPE PARAMETER hole. N +// near-identical type decls collapse to one generic (`Int8`..`Int128` = one +// `Compose>` axis, not 10 hand-rolled types; `CpuArchitecture` and +// `TargetArchitecture`, byte-identical enums, = one name). This is consolidated into the +// v2.lens.intent_linearity registry as a row -- one engine (`congruent`), two binders. +// +// Difference from the term binder: a fold needs VARYING data, so simulated_relationship +// excludes pure duplication; at the type layer byte-identical decls are the STRONGEST §3 +// nickname, so the type binder fires on `congruent` DIRECTLY (identical OR distinct-leaf), +// and a PAIR already suffices (threshold 2, not the fold's 3). Adjacency reuses the same +// skip / is_prefix_of machinery: congruence is one shared skeleton, transitive across the +// family, so "every adjacent pair congruent" closes the whole family. Variant-matching on +// FreeMonoid stays inside v2.std.algebra (the v2 cross-module generic-instantiation +// weakness), so the list walk goes through algebra's combinators, never a local match. + +// A type-declaration forest is STRUCTURALLY SIMILAR (redundant: collapses to one +// parameterized type) iff it holds >=2 decls that anti-unify -- share one skeleton, +// differing only at leaf positions (the type-parameter holes). +fn type_decls_anti_unify(decls: FreeMonoid) -> Bool { + if length(xs: decls) < 2 { + false + } else { + is_prefix_of( + prefix: skip(xs: decls, n: 1), + xs: decls, + eq: fn(later, earlier) { congruent(a: earlier, b: later) } + ) } } data construction_justification: ConstructionJustification = ConstructionJustification { class: WallAfterGrounding { - grounding_authority: "the parse/resolve walk producing per-decl TypeShape/VariantShape facts by construction", - dissolve_on: "per-decl structural-shape facts are produced by the substrate walk, not by a staged lens producer" + grounding_authority: "the parse/resolve walk that projects a module's type declarations into a FreeMonoid forest (shared with v2.lens.simulated_relationship's statement-chain projector)", + dissolve_on: "type_decls_anti_unify runs over live dsl/** type-declaration forests once the parse/resolve walk produces per-module type-decl facts; until then this is a lens_unit predicate over synthetic type-decl forests, consumed as a row of the v2.lens.intent_linearity registry" }, - rationale: "Per-decl structural shape is a decidable index; a scaffold producer-stage substrate (unblocking variant-parameter-clone and structural-similarity) until the parse/resolve walk lands." + rationale: "Structural congruence of type declarations is decidable (a wall): type decls that share one skeleton differing only at leaf positions collapse to one generic (the leaves becoming type parameters), and byte-identical decls are the strongest §3 nickname. The undecidable residue (whether the leaf variance is semantically one type parameter or coincidental) stays a ratchet. One engine (`congruent`), two binders (term chain / type forest)." } diff --git a/src/v2/lens/structural_similarity/sg_claims_test.dag b/src/v2/lens/structural_similarity/sg_claims_test.dag deleted file mode 100644 index e3dc518ffe0..00000000000 --- a/src/v2/lens/structural_similarity/sg_claims_test.dag +++ /dev/null @@ -1,22 +0,0 @@ -module v2.test.lens_structural_similarity.sg_claims - -import v2.lens.structural_similarity { - StructuralSimilarityVerdict, - Unrealized, - structural_similarity_fact -} -import v2.std.logic { Bool } -import v2.std.verification { BoolWitness, BoolWitnessClaim, UnifiedTestClaim } - -fn ss_verdict_is_unrealized(verdict: StructuralSimilarityVerdict) -> Bool { - match verdict { - Unrealized => true - _ => false - } -} - -test fn lens_structural_similarity_unrealized_scaffold_holds() -> Bool { - ss_verdict_is_unrealized( - verdict: structural_similarity_fact().verdict - ) -} diff --git a/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag b/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag index 913c02c923c..8f6c394f862 100644 --- a/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag +++ b/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag @@ -62,3 +62,17 @@ test fn all_minimal_body_is_linear() -> Bool { test fn single_minimal_level_is_linear() -> Bool { level_is_linear(level: linear_chain_b) } + +// ── consolidation: the type-decl row fires through the SAME engine ─────────────── +// structural_similarity is now Row 2 of the registry (one engine, two binders), so a +// congruent type-decl family is redundant by the same chain_is_redundant the term row +// uses -- proof the row is wired in, not a standalone peer. Two byte-identical enums = +// the §3 nickname (CpuArchitecture / TargetArchitecture); the term row alone (≥3, +// distinct leaves) would NOT fire on this pair, so a green here discriminates the row. +data dup_type_pair: List = [ + conj2(a: atom(id: ^x86), b: atom(id: ^arm)), + conj2(a: atom(id: ^x86), b: atom(id: ^arm)) +] +test fn dup_type_decls_redundant_through_registry() -> Bool { + chain_is_redundant(steps: dup_type_pair) +} diff --git a/src/v2/test/claim/structural_similarity/lens_unit/discriminators_test.dag b/src/v2/test/claim/structural_similarity/lens_unit/discriminators_test.dag new file mode 100644 index 00000000000..25f7852effd --- /dev/null +++ b/src/v2/test/claim/structural_similarity/lens_unit/discriminators_test.dag @@ -0,0 +1,85 @@ +module v2.test.structural_similarity.lens_unit.discriminators + +import v2.lens.structural_similarity { type_decls_anti_unify } +import v2.std.node { + Node, Edge, Positional, + TypeNode, Atom, Conj, Disj, + Symbol, node_synthetic +} +import v2.std.collection { List } +import v2.std.logic { Bool } + +// ── synthetic type-decl Node shapes (no live parse/resolve walk needed) ───────── +fn atom(id: Symbol) -> Node { + node_synthetic(kind: TypeNode { connective: Atom { identity: id } }, children: []) +} +// a 2-variant sum type (e.g. `enum Arch = X86 | Arm`) +fn disj2(a: Node, b: Node) -> Node { + node_synthetic(kind: TypeNode { connective: Disj }, children: [ + Edge { label: Positional, target: a }, Edge { label: Positional, target: b } ]) +} +// a product/compose shape (e.g. `Compose`) +fn compose2(a: Node, b: Node) -> Node { + node_synthetic(kind: TypeNode { connective: Conj }, children: [ + Edge { label: Positional, target: a }, Edge { label: Positional, target: b } ]) +} + +// ── RED: structurally-similar type decls (must flag) ──────────────────────────── + +// §3 nickname: two byte-identical enums (the CpuArchitecture / TargetArchitecture +// smell). The strongest duplication -- one concept, two names. The type binder fires +// on `congruent` directly, so identical decls (which the term binder excludes as pure +// duplication) are caught here. +data nickname_pair: List = [ + disj2(a: atom(id: ^x86), b: atom(id: ^arm)), + disj2(a: atom(id: ^x86), b: atom(id: ^arm)) +] + +// §2-horizontal: a congruent FAMILY varying at one leaf -- `Int8`/`Int16`/`Int32` = +// one `Compose>` axis, the leaf width becoming a type parameter. +data width_family: List = [ + compose2(a: atom(id: ^int), b: atom(id: ^w8)), + compose2(a: atom(id: ^int), b: atom(id: ^w16)), + compose2(a: atom(id: ^int), b: atom(id: ^w32)) +] + +// ── GREEN: genuinely-distinct type decls (must NOT flag) ──────────────────────── + +// Different skeletons: a nullary atom, a sum, a product -- no shared template, so no +// single generic collapses them. Adjacent pairs diverge in shape (atom has no children +// where disj2 does), so anti-unification finds no non-trivial common form. +data distinct_decls: List = [ + atom(id: ^unit), + disj2(a: atom(id: ^a), b: atom(id: ^b)), + compose2(a: atom(id: ^int), b: atom(id: ^w8)) +] + +// A family whose middle decl breaks the skeleton (arity 2 product vs a deeper nest): +// adjacency fails, so the family does NOT collapse to one generic. +data near_but_divergent: List = [ + compose2(a: atom(id: ^int), b: atom(id: ^w8)), + compose2(a: atom(id: ^int), b: compose2(a: atom(id: ^ptr), b: atom(id: ^w16))), + compose2(a: atom(id: ^int), b: atom(id: ^w32)) +] + +// A single type decl is not yet a similarity (< 2). +data single_decl: List = [ + disj2(a: atom(id: ^x), b: atom(id: ^y)) +] + +// ── witnesses ──────────────────────────────────────────────────────────────────── +test fn nickname_pair_is_similar() -> Bool { + type_decls_anti_unify(decls: nickname_pair) +} +test fn width_family_is_similar() -> Bool { + type_decls_anti_unify(decls: width_family) +} +test fn distinct_decls_are_not_similar() -> Bool { + !type_decls_anti_unify(decls: distinct_decls) +} +test fn divergent_family_is_not_similar() -> Bool { + !type_decls_anti_unify(decls: near_but_divergent) +} +test fn single_decl_is_not_similar() -> Bool { + !type_decls_anti_unify(decls: single_decl) +} From bb30d048c0dca355bd5db3e06e1b741b77eedc6a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 01:47:44 +0000 Subject: [PATCH 2/5] intent_linearity: make the binder first-class (Representation) so the type-decl row stays off term-chain projections Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v2/lens/intent_linearity.dag | 46 +++++++++++++++---- .../lens_unit/discriminators_test.dag | 17 ++++--- 2 files changed, 49 insertions(+), 14 deletions(-) diff --git a/src/v2/lens/intent_linearity.dag b/src/v2/lens/intent_linearity.dag index 003251fd52e..255e07902f4 100644 --- a/src/v2/lens/intent_linearity.dag +++ b/src/v2/lens/intent_linearity.dag @@ -15,29 +15,37 @@ import v2.std.logic { Bool } // The §1 time-axis a rule's minimal form reduces (change-time = §2 maintenance; run-time = §1 cost). type CostAxis = ChangeTime | RunTime +// The BINDER: which representation the engine's anti-unification kernel walks for this row. The two +// binders share one `congruent` engine but project different inputs -- a body's statement chain (the +// fold's hole is a list element) vs a module's type-declaration forest (the hole is a type parameter). +type Representation = TermChain | TypeForest + type LinearityRule { name: Symbol axis: CostAxis + representation: Representation detect: fn(FreeMonoid) -> Bool } -// Row 1 — the hand-unrolled fold (change-time). detect reuses simulated_relationship; minimal form = one -// fold over the data the chain spells out by hand. +// Row 1 — the hand-unrolled fold (term chain, change-time). detect reuses simulated_relationship; +// minimal form = one fold over the data the chain spells out by hand. fn unroll_to_fold_rule() -> LinearityRule { LinearityRule { name: ^unroll_to_fold, axis: ChangeTime, + representation: TermChain, detect: fn(s) { chain_is_simulated(steps: s) } } } -// Row 2 — duplicate TYPE declarations (change-time). detect reuses structural_similarity's type-decl -// binder over the same `congruent` kernel; minimal form = one generic over the leaf that varies across -// the congruent family (the §3 nickname / `Int8`..`Int128` collapse to one `Compose` axis). +// Row 2 — duplicate TYPE declarations (type forest, change-time). detect reuses structural_similarity's +// type-decl binder over the same `congruent` kernel; minimal form = one generic over the leaf that varies +// across the congruent family (the §3 nickname / `Int8`..`Int128` collapse to one `Compose` axis). fn dup_type_to_generic_rule() -> LinearityRule { LinearityRule { name: ^dup_type_to_generic, axis: ChangeTime, + representation: TypeForest, detect: fn(s) { type_decls_anti_unify(decls: s) } } } @@ -46,20 +54,42 @@ fn linearity_registry() -> FreeMonoid { [ unroll_to_fold_rule(), dup_type_to_generic_rule() ] } +fn representation_eq(a: Representation, b: Representation) -> Bool { + match a { + TermChain => match b { TermChain => true _ => false } + TypeForest => match b { TypeForest => true _ => false } + } +} + // typed projector (avoids field access on a fold lambda element) fn rule_fires(rule: LinearityRule, steps: FreeMonoid) -> Bool { rule.detect(steps) } -// Is this chain non-linear at this level -- does ANY registry rule fire? -fn chain_is_redundant(steps: FreeMonoid) -> Bool { +// The engine: does ANY row BOUND TO `rep` fire on this input? Filtering by representation keeps each +// binder's rows off the other binder's projection (a 2-decl congruent type pair is a nickname, but two +// adjacent congruent statements are not yet a fold), so one registry serves both without contamination. +fn input_is_redundant_for(rep: Representation, input: FreeMonoid) -> Bool { fold_list( xs: linearity_registry(), empty: false, - cons: fn(acc, rule) { acc || rule_fires(rule: rule, steps: steps) } + cons: fn(acc, rule) { + acc || (representation_eq(a: rule.representation, b: rep) && rule_fires(rule: rule, steps: input)) + } ) } +// TERM binder — is this statement chain non-linear at this level (any TermChain row fires)? +fn chain_is_redundant(steps: FreeMonoid) -> Bool { + input_is_redundant_for(rep: TermChain, input: steps) +} + +// TYPE binder — does this module's type-declaration forest collapse to one generic (any TypeForest row +// fires)? The same engine, the other binder. +fn forest_is_redundant(decls: FreeMonoid) -> Bool { + input_is_redundant_for(rep: TypeForest, input: decls) +} + // Residual redundancy: a flagged chain of N statements collapses to 1 fold over N data, so it carries // (N - 1) redundant hand-copies -- the O(n)->O(1) saving the minimal form realizes; 0 if already minimal. fn chain_residual(steps: FreeMonoid) -> Int { diff --git a/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag b/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag index 8f6c394f862..f1166e1190f 100644 --- a/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag +++ b/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag @@ -1,6 +1,6 @@ module v2.test.intent_linearity.lens_unit.discriminators -import v2.lens.intent_linearity { chain_is_redundant, chain_residual, level_is_linear, body_is_linear } +import v2.lens.intent_linearity { chain_is_redundant, forest_is_redundant, chain_residual, level_is_linear, body_is_linear } import v2.std.node { Node, Edge, EdgeLabel, Positional, NodeKind, TypeNode, Connective, Atom, Conj, @@ -65,14 +65,19 @@ test fn single_minimal_level_is_linear() -> Bool { // ── consolidation: the type-decl row fires through the SAME engine ─────────────── // structural_similarity is now Row 2 of the registry (one engine, two binders), so a -// congruent type-decl family is redundant by the same chain_is_redundant the term row -// uses -- proof the row is wired in, not a standalone peer. Two byte-identical enums = -// the §3 nickname (CpuArchitecture / TargetArchitecture); the term row alone (≥3, -// distinct leaves) would NOT fire on this pair, so a green here discriminates the row. +// congruent type-decl family is redundant through the type binder (forest_is_redundant) +// of the same registry the term binder uses -- proof the row is wired in, not a peer. +// Two byte-identical enums = the §3 nickname (CpuArchitecture / TargetArchitecture). data dup_type_pair: List = [ conj2(a: atom(id: ^x86), b: atom(id: ^arm)), conj2(a: atom(id: ^x86), b: atom(id: ^arm)) ] test fn dup_type_decls_redundant_through_registry() -> Bool { - chain_is_redundant(steps: dup_type_pair) + forest_is_redundant(decls: dup_type_pair) +} +// Binder isolation: the type pair is NOT flagged by the TERM binder (two congruent +// statements are not yet a fold; the term row needs ≥3) -- proves rows stay off the +// other binder's projection, so one registry serves both without contamination. +test fn dup_type_pair_not_flagged_by_term_binder() -> Bool { + !chain_is_redundant(steps: dup_type_pair) } From 9915d577576f460b274402d6197db9cea9bb8a92 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 02:30:36 +0000 Subject: [PATCH 3/5] Integrate main (#5579 .dag comment-wall): strip // comments from the consolidation files, fold key prose into construction_justification carriers Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v2/lens/intent_linearity.dag | 39 +------------------ src/v2/lens/structural_similarity.dag | 26 +------------ .../lens_unit/discriminators_test.dag | 8 ---- .../lens_unit/discriminators_test.dag | 20 ---------- 4 files changed, 4 insertions(+), 89 deletions(-) diff --git a/src/v2/lens/intent_linearity.dag b/src/v2/lens/intent_linearity.dag index 9ae804a204b..6933edcfbe8 100644 --- a/src/v2/lens/intent_linearity.dag +++ b/src/v2/lens/intent_linearity.dag @@ -6,20 +6,8 @@ import v2.std.node { Node, Symbol } import v2.std.algebra { FreeMonoid, length, fold_list } import v2.std.logic { Bool } -<<<<<<< HEAD -// Intent-linearity enforcer: a program's description should equal its irreducible information content -// (minimal template + distinct data), recursively at every level -- intent 1:1 with its inputs. This is -// the registry the redundancy lenses become ROWS of (so the enforcer is itself linear: one engine, N -// rows, not a fork). Row 1 = the hand-unrolled fold (term layer); Row 2 = duplicate type declarations -// (type-decl layer) -- one anti-unification engine, two binders; complexity cost-recurrence rules join later. -======= ->>>>>>> origin/main - type CostAxis = ChangeTime | RunTime -// The BINDER: which representation the engine's anti-unification kernel walks for this row. The two -// binders share one `congruent` engine but project different inputs -- a body's statement chain (the -// fold's hole is a list element) vs a module's type-declaration forest (the hole is a type parameter). type Representation = TermChain | TypeForest type LinearityRule { @@ -29,11 +17,6 @@ type LinearityRule { detect: fn(FreeMonoid) -> Bool } -<<<<<<< HEAD -// Row 1 — the hand-unrolled fold (term chain, change-time). detect reuses simulated_relationship; -// minimal form = one fold over the data the chain spells out by hand. -======= ->>>>>>> origin/main fn unroll_to_fold_rule() -> LinearityRule { LinearityRule { name: ^unroll_to_fold, @@ -43,9 +26,6 @@ fn unroll_to_fold_rule() -> LinearityRule { } } -// Row 2 — duplicate TYPE declarations (type forest, change-time). detect reuses structural_similarity's -// type-decl binder over the same `congruent` kernel; minimal form = one generic over the leaf that varies -// across the congruent family (the §3 nickname / `Int8`..`Int128` collapse to one `Compose` axis). fn dup_type_to_generic_rule() -> LinearityRule { LinearityRule { name: ^dup_type_to_generic, @@ -70,14 +50,7 @@ fn rule_fires(rule: LinearityRule, steps: FreeMonoid) -> Bool { rule.detect(steps) } -<<<<<<< HEAD -// The engine: does ANY row BOUND TO `rep` fire on this input? Filtering by representation keeps each -// binder's rows off the other binder's projection (a 2-decl congruent type pair is a nickname, but two -// adjacent congruent statements are not yet a fold), so one registry serves both without contamination. fn input_is_redundant_for(rep: Representation, input: FreeMonoid) -> Bool { -======= -fn chain_is_redundant(steps: FreeMonoid) -> Bool { ->>>>>>> origin/main fold_list( xs: linearity_registry(), empty: false, @@ -87,22 +60,14 @@ fn chain_is_redundant(steps: FreeMonoid) -> Bool { ) } -<<<<<<< HEAD -// TERM binder — is this statement chain non-linear at this level (any TermChain row fires)? fn chain_is_redundant(steps: FreeMonoid) -> Bool { input_is_redundant_for(rep: TermChain, input: steps) } -// TYPE binder — does this module's type-declaration forest collapse to one generic (any TypeForest row -// fires)? The same engine, the other binder. fn forest_is_redundant(decls: FreeMonoid) -> Bool { input_is_redundant_for(rep: TypeForest, input: decls) } -// Residual redundancy: a flagged chain of N statements collapses to 1 fold over N data, so it carries -// (N - 1) redundant hand-copies -- the O(n)->O(1) saving the minimal form realizes; 0 if already minimal. -======= ->>>>>>> origin/main fn chain_residual(steps: FreeMonoid) -> Int { if chain_is_redundant(steps: steps) { length(xs: steps) - 1 @@ -126,7 +91,7 @@ fn body_is_linear(levels: FreeMonoid>) -> Bool { data construction_justification: ConstructionJustification = ConstructionJustification { class: WallAfterGrounding { grounding_authority: "the parse/resolve walk + chain projector decomposing a body into its per-level statement-chains (shared with v2.lens.simulated_relationship / v2.lens.structural_similarity)", - dissolve_on: "body_is_linear runs over live dsl/** bodies once the walk projects per-level chains; the registry grows by rows (complexity cost-recurrence rules join the change-time rows); until then this is a lens_unit over projected synthetic chains" + dissolve_on: "body_is_linear runs over live dsl bodies once the walk projects per-level chains; the registry grows by rows (complexity cost-recurrence rules join the change-time rows); Row 1 is the term-chain hand-unrolled fold, Row 2 the type-decl duplicate-to-generic, one anti-unification engine and two binders; until then this is a lens_unit over projected synthetic chains" }, - rationale: "Intent-linearity is a wall up to the substrate's expressible abstraction (anti-unification computes the structural minimum) and a ratchet beyond it (global minimal description is Kolmogorov-uncomputable). The registry is the decidable wall-half; complexity.dag keeps the RatchetForever optimality residue. One engine, N rows (§2-horizontal)." + rationale: "Intent-linearity is a wall up to the substrate's expressible abstraction (anti-unification computes the structural minimum) and a ratchet beyond it (global minimal description is Kolmogorov-uncomputable). The registry is the decidable wall-half; complexity.dag keeps the RatchetForever optimality residue. One engine, N rows; the Representation field tags each row's binder so the term and type rows stay off each other's projection." } diff --git a/src/v2/lens/structural_similarity.dag b/src/v2/lens/structural_similarity.dag index d1f9e587b0a..d43cb166ae5 100644 --- a/src/v2/lens/structural_similarity.dag +++ b/src/v2/lens/structural_similarity.dag @@ -6,28 +6,6 @@ import v2.std.node { Node } import v2.std.algebra { FreeMonoid, length, skip, is_prefix_of } import v2.std.logic { Bool } -// §2-horizontal / §3-nicknaming detector at the TYPE-DECLARATION layer -- the type-decl -// twin of v2.lens.simulated_relationship (which targets statement chains inside a body). -// Same anti-unification engine -- `congruent`, the shared kernel seeded in -// simulated_relationship -- a different BINDER: the leaves that vary across a congruent -// family of type decls are not a fold's list-element hole but a TYPE PARAMETER hole. N -// near-identical type decls collapse to one generic (`Int8`..`Int128` = one -// `Compose>` axis, not 10 hand-rolled types; `CpuArchitecture` and -// `TargetArchitecture`, byte-identical enums, = one name). This is consolidated into the -// v2.lens.intent_linearity registry as a row -- one engine (`congruent`), two binders. -// -// Difference from the term binder: a fold needs VARYING data, so simulated_relationship -// excludes pure duplication; at the type layer byte-identical decls are the STRONGEST §3 -// nickname, so the type binder fires on `congruent` DIRECTLY (identical OR distinct-leaf), -// and a PAIR already suffices (threshold 2, not the fold's 3). Adjacency reuses the same -// skip / is_prefix_of machinery: congruence is one shared skeleton, transitive across the -// family, so "every adjacent pair congruent" closes the whole family. Variant-matching on -// FreeMonoid stays inside v2.std.algebra (the v2 cross-module generic-instantiation -// weakness), so the list walk goes through algebra's combinators, never a local match. - -// A type-declaration forest is STRUCTURALLY SIMILAR (redundant: collapses to one -// parameterized type) iff it holds >=2 decls that anti-unify -- share one skeleton, -// differing only at leaf positions (the type-parameter holes). fn type_decls_anti_unify(decls: FreeMonoid) -> Bool { if length(xs: decls) < 2 { false @@ -43,7 +21,7 @@ fn type_decls_anti_unify(decls: FreeMonoid) -> Bool { data construction_justification: ConstructionJustification = ConstructionJustification { class: WallAfterGrounding { grounding_authority: "the parse/resolve walk that projects a module's type declarations into a FreeMonoid forest (shared with v2.lens.simulated_relationship's statement-chain projector)", - dissolve_on: "type_decls_anti_unify runs over live dsl/** type-declaration forests once the parse/resolve walk produces per-module type-decl facts; until then this is a lens_unit predicate over synthetic type-decl forests, consumed as a row of the v2.lens.intent_linearity registry" + dissolve_on: "type_decls_anti_unify runs over live dsl type-declaration forests once the parse/resolve walk produces per-module type-decl facts; until then this is a lens_unit predicate over synthetic type-decl forests, consumed as a row of the v2.lens.intent_linearity registry. This is the type-decl twin of v2.lens.simulated_relationship: the same congruent kernel, a different binder (the leaves that vary across a congruent family of type decls are a type-parameter hole, not a fold's list-element hole), so N near-identical type decls collapse to one generic (Int8..Int128 = one Compose axis). Unlike the term binder a pair suffices (threshold 2, not the fold's 3) and it fires on congruent directly so byte-identical decls (the strongest section-3 nickname) are caught; adjacency reuses skip/is_prefix_of since congruence is one shared skeleton transitive across the family." }, - rationale: "Structural congruence of type declarations is decidable (a wall): type decls that share one skeleton differing only at leaf positions collapse to one generic (the leaves becoming type parameters), and byte-identical decls are the strongest §3 nickname. The undecidable residue (whether the leaf variance is semantically one type parameter or coincidental) stays a ratchet. One engine (`congruent`), two binders (term chain / type forest)." + rationale: "Structural congruence of type declarations is decidable (a wall): type decls that share one skeleton differing only at leaf positions collapse to one generic (the leaves becoming type parameters), and byte-identical decls are the strongest section-3 nickname. The undecidable residue (whether the leaf variance is semantically one type parameter or coincidental) stays a ratchet. One engine (congruent), two binders (term chain / type forest)." } diff --git a/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag b/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag index 8ca50015ef8..f64e1458c50 100644 --- a/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag +++ b/src/v2/test/claim/intent_linearity/lens_unit/discriminators_test.dag @@ -56,11 +56,6 @@ test fn single_minimal_level_is_linear() -> Bool { level_is_linear(level: linear_chain_b) } -// ── consolidation: the type-decl row fires through the SAME engine ─────────────── -// structural_similarity is now Row 2 of the registry (one engine, two binders), so a -// congruent type-decl family is redundant through the type binder (forest_is_redundant) -// of the same registry the term binder uses -- proof the row is wired in, not a peer. -// Two byte-identical enums = the §3 nickname (CpuArchitecture / TargetArchitecture). data dup_type_pair: List = [ conj2(a: atom(id: ^x86), b: atom(id: ^arm)), conj2(a: atom(id: ^x86), b: atom(id: ^arm)) @@ -68,9 +63,6 @@ data dup_type_pair: List = [ test fn dup_type_decls_redundant_through_registry() -> Bool { forest_is_redundant(decls: dup_type_pair) } -// Binder isolation: the type pair is NOT flagged by the TERM binder (two congruent -// statements are not yet a fold; the term row needs ≥3) -- proves rows stay off the -// other binder's projection, so one registry serves both without contamination. test fn dup_type_pair_not_flagged_by_term_binder() -> Bool { !chain_is_redundant(steps: dup_type_pair) } diff --git a/src/v2/test/claim/structural_similarity/lens_unit/discriminators_test.dag b/src/v2/test/claim/structural_similarity/lens_unit/discriminators_test.dag index 25f7852effd..b2771c5cc55 100644 --- a/src/v2/test/claim/structural_similarity/lens_unit/discriminators_test.dag +++ b/src/v2/test/claim/structural_similarity/lens_unit/discriminators_test.dag @@ -9,65 +9,45 @@ import v2.std.node { import v2.std.collection { List } import v2.std.logic { Bool } -// ── synthetic type-decl Node shapes (no live parse/resolve walk needed) ───────── fn atom(id: Symbol) -> Node { node_synthetic(kind: TypeNode { connective: Atom { identity: id } }, children: []) } -// a 2-variant sum type (e.g. `enum Arch = X86 | Arm`) fn disj2(a: Node, b: Node) -> Node { node_synthetic(kind: TypeNode { connective: Disj }, children: [ Edge { label: Positional, target: a }, Edge { label: Positional, target: b } ]) } -// a product/compose shape (e.g. `Compose`) fn compose2(a: Node, b: Node) -> Node { node_synthetic(kind: TypeNode { connective: Conj }, children: [ Edge { label: Positional, target: a }, Edge { label: Positional, target: b } ]) } -// ── RED: structurally-similar type decls (must flag) ──────────────────────────── - -// §3 nickname: two byte-identical enums (the CpuArchitecture / TargetArchitecture -// smell). The strongest duplication -- one concept, two names. The type binder fires -// on `congruent` directly, so identical decls (which the term binder excludes as pure -// duplication) are caught here. data nickname_pair: List = [ disj2(a: atom(id: ^x86), b: atom(id: ^arm)), disj2(a: atom(id: ^x86), b: atom(id: ^arm)) ] -// §2-horizontal: a congruent FAMILY varying at one leaf -- `Int8`/`Int16`/`Int32` = -// one `Compose>` axis, the leaf width becoming a type parameter. data width_family: List = [ compose2(a: atom(id: ^int), b: atom(id: ^w8)), compose2(a: atom(id: ^int), b: atom(id: ^w16)), compose2(a: atom(id: ^int), b: atom(id: ^w32)) ] -// ── GREEN: genuinely-distinct type decls (must NOT flag) ──────────────────────── - -// Different skeletons: a nullary atom, a sum, a product -- no shared template, so no -// single generic collapses them. Adjacent pairs diverge in shape (atom has no children -// where disj2 does), so anti-unification finds no non-trivial common form. data distinct_decls: List = [ atom(id: ^unit), disj2(a: atom(id: ^a), b: atom(id: ^b)), compose2(a: atom(id: ^int), b: atom(id: ^w8)) ] -// A family whose middle decl breaks the skeleton (arity 2 product vs a deeper nest): -// adjacency fails, so the family does NOT collapse to one generic. data near_but_divergent: List = [ compose2(a: atom(id: ^int), b: atom(id: ^w8)), compose2(a: atom(id: ^int), b: compose2(a: atom(id: ^ptr), b: atom(id: ^w16))), compose2(a: atom(id: ^int), b: atom(id: ^w32)) ] -// A single type decl is not yet a similarity (< 2). data single_decl: List = [ disj2(a: atom(id: ^x), b: atom(id: ^y)) ] -// ── witnesses ──────────────────────────────────────────────────────────────────── test fn nickname_pair_is_similar() -> Bool { type_decls_anti_unify(decls: nickname_pair) } From 43b5237ad66d515b80218dec1414daad51c45dc0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 03:15:40 +0000 Subject: [PATCH 4/5] Integrate main (#5599): rebuild structural_similarity on the new v2.std.anti_unification kernel #5599 extracted anti-unification into v2.std.anti_unification (anti_unify_chain -> ChainGeneralization, fillings_all_leaves, template_has_hole) and removed simulated_relationship's congruent. Rebuild the type-decl binder on the shared kernel: a forest collapses to one generic iff fillings_all_leaves (all variance at leaf positions that become type parameters). Unlike the term binder, template_has_hole is NOT required, so byte-identical decls (the hole-free section-3 nickname) are still flagged. Reconcile intent_linearity with main's any/for_all refactor while keeping the Representation-tagged two-binder registry. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v2/lens/intent_linearity.dag | 14 ++++---------- src/v2/lens/structural_similarity.dag | 20 ++++++++++---------- 2 files changed, 14 insertions(+), 20 deletions(-) diff --git a/src/v2/lens/intent_linearity.dag b/src/v2/lens/intent_linearity.dag index 10a6c1a04b6..aa7d7a98850 100644 --- a/src/v2/lens/intent_linearity.dag +++ b/src/v2/lens/intent_linearity.dag @@ -50,19 +50,13 @@ fn rule_fires(rule: LinearityRule, steps: FreeMonoid) -> Bool { rule.detect(steps) } -<<<<<<< HEAD fn input_is_redundant_for(rep: Representation, input: FreeMonoid) -> Bool { - fold_list( + any( xs: linearity_registry(), - empty: false, - cons: fn(acc, rule) { - acc || (representation_eq(a: rule.representation, b: rep) && rule_fires(rule: rule, steps: input)) + predicate: fn(rule) { + representation_eq(a: rule.representation, b: rep) && rule_fires(rule: rule, steps: input) } ) -======= -fn chain_is_redundant(steps: FreeMonoid) -> Bool { - any(xs: linearity_registry(), predicate: fn(rule) { rule_fires(rule: rule, steps: steps) }) ->>>>>>> origin/main } fn chain_is_redundant(steps: FreeMonoid) -> Bool { @@ -91,7 +85,7 @@ fn body_is_linear(levels: FreeMonoid>) -> Bool { data construction_justification: ConstructionJustification = ConstructionJustification { class: WallAfterGrounding { - grounding_authority: "the parse/resolve walk + chain projector decomposing a body into its per-level statement-chains (shared with v2.lens.simulated_relationship / v2.lens.structural_similarity)", + grounding_authority: "the parse/resolve walk + chain projector decomposing a body into its per-level statement-chains (shared with v2.lens.simulated_relationship / v2.lens.structural_similarity, all over the v2.std.anti_unification kernel)", dissolve_on: "body_is_linear runs over live dsl bodies once the walk projects per-level chains; the registry grows by rows (complexity cost-recurrence rules join the change-time rows); Row 1 is the term-chain hand-unrolled fold, Row 2 the type-decl duplicate-to-generic, one anti-unification engine and two binders; until then this is a lens_unit over projected synthetic chains" }, rationale: "Intent-linearity is a wall up to the substrate's expressible abstraction (anti-unification computes the structural minimum) and a ratchet beyond it (global minimal description is Kolmogorov-uncomputable). The registry is the decidable wall-half; complexity.dag keeps the RatchetForever optimality residue. One engine, N rows; the Representation field tags each row's binder so the term and type rows stay off each other's projection." diff --git a/src/v2/lens/structural_similarity.dag b/src/v2/lens/structural_similarity.dag index d43cb166ae5..29a5767249e 100644 --- a/src/v2/lens/structural_similarity.dag +++ b/src/v2/lens/structural_similarity.dag @@ -1,27 +1,27 @@ module v2.lens.structural_similarity import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } -import v2.lens.simulated_relationship { congruent } import v2.std.node { Node } -import v2.std.algebra { FreeMonoid, length, skip, is_prefix_of } +import v2.std.algebra { FreeMonoid, length } +import v2.std.anti_unification { ChainGeneralization, anti_unify_chain, fillings_all_leaves } import v2.std.logic { Bool } +fn forest_collapses_to_generic(g: ChainGeneralization) -> Bool { + fillings_all_leaves(per_element: g.per_element) +} + fn type_decls_anti_unify(decls: FreeMonoid) -> Bool { if length(xs: decls) < 2 { false } else { - is_prefix_of( - prefix: skip(xs: decls, n: 1), - xs: decls, - eq: fn(later, earlier) { congruent(a: earlier, b: later) } - ) + forest_collapses_to_generic(g: anti_unify_chain(steps: decls)) } } data construction_justification: ConstructionJustification = ConstructionJustification { class: WallAfterGrounding { - grounding_authority: "the parse/resolve walk that projects a module's type declarations into a FreeMonoid forest (shared with v2.lens.simulated_relationship's statement-chain projector)", - dissolve_on: "type_decls_anti_unify runs over live dsl type-declaration forests once the parse/resolve walk produces per-module type-decl facts; until then this is a lens_unit predicate over synthetic type-decl forests, consumed as a row of the v2.lens.intent_linearity registry. This is the type-decl twin of v2.lens.simulated_relationship: the same congruent kernel, a different binder (the leaves that vary across a congruent family of type decls are a type-parameter hole, not a fold's list-element hole), so N near-identical type decls collapse to one generic (Int8..Int128 = one Compose axis). Unlike the term binder a pair suffices (threshold 2, not the fold's 3) and it fires on congruent directly so byte-identical decls (the strongest section-3 nickname) are caught; adjacency reuses skip/is_prefix_of since congruence is one shared skeleton transitive across the family." + grounding_authority: "the parse/resolve walk that projects a module's type declarations into a FreeMonoid forest (anti-unified by the shared v2.std.anti_unification kernel, also used by v2.lens.simulated_relationship's statement-chain binder)", + dissolve_on: "type_decls_anti_unify runs over live dsl type-declaration forests once the parse/resolve walk produces per-module type-decl facts; until then this is a lens_unit predicate over synthetic type-decl forests, consumed as a row of the v2.lens.intent_linearity registry. This is the type-decl twin of v2.lens.simulated_relationship: the same anti_unify_chain engine, a different binder (the leaves that vary across a congruent family of type decls are a type-parameter hole, not a fold's list-element hole), so N near-identical type decls collapse to one generic (Int8..Int128 = one Compose axis). Unlike the term binder a pair suffices (threshold 2, not the fold's 3) and template_has_hole is NOT required, so byte-identical decls (the strongest section-3 nickname, a hole-free template) are also caught: the wall is fillings_all_leaves, i.e. all variance sits at leaf positions that become type parameters." }, - rationale: "Structural congruence of type declarations is decidable (a wall): type decls that share one skeleton differing only at leaf positions collapse to one generic (the leaves becoming type parameters), and byte-identical decls are the strongest section-3 nickname. The undecidable residue (whether the leaf variance is semantically one type parameter or coincidental) stays a ratchet. One engine (congruent), two binders (term chain / type forest)." + rationale: "Structural anti-unification of type declarations is decidable (a wall): type decls whose only variance is at leaf positions collapse to one generic (the leaves becoming type parameters), and byte-identical decls are the strongest section-3 nickname. The undecidable residue (whether the leaf variance is semantically one type parameter or coincidental) stays a ratchet. One engine (v2.std.anti_unification), two binders (term chain / type forest)." } From 2b3597ee266b77e6a304bcd76c91b9a580f99bce Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 23 Jun 2026 04:47:53 +0000 Subject: [PATCH 5/5] WIP: Consolidate structural_similarity into the intent_linearity registry as --- src/v2/lens/intent_linearity.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/v2/lens/intent_linearity.dag b/src/v2/lens/intent_linearity.dag index aa7d7a98850..cbb5365625f 100644 --- a/src/v2/lens/intent_linearity.dag +++ b/src/v2/lens/intent_linearity.dag @@ -41,8 +41,8 @@ fn linearity_registry() -> FreeMonoid { fn representation_eq(a: Representation, b: Representation) -> Bool { match a { - TermChain => match b { TermChain => true _ => false } - TypeForest => match b { TypeForest => true _ => false } + TermChain => match b { TermChain => true TypeForest => false } + TypeForest => match b { TermChain => false TypeForest => true } } }