Repository navigation
Generalization-producing anti_unify (the produce core). Upgrade v2.lens.simulated_relationship's congruent (Bool) to RETURN the minimal form: the anti-unification generalization of a statement chain = a common template Node (with ^HOLE markers where steps differ) + the per-element substitution list. - #5599
Merged
Merged
Conversation
…ngs; derive simulated_relationship from it Upgrade v2.lens.simulated_relationship from an adjacent-pairwise congruence Bool to a derivation over the produced minimal form. New shared kernel v2.std.anti_unification (domain-agnostic over Node; the type-decl forest binder reuses it): - anti_unify(a, b): full least-general generalization -> a template Node carrying ^HOLE leaves at every divergence (always succeeds; divergence becomes a hole). - extract_fillings(template, element): the per-element substitution at each hole. - anti_unify_chain(steps): whole-chain template + per-element substitution list. - template_has_hole / fillings_all_leaves: consumer-side produced-form predicates. Additive std (flagged for review): two new generic combinators in algebra.dag (zip_map, reduce_or; FreeMonoid variant match kept inside algebra) and the new anti_unification module (sibling of exact_structural_equality_zip_fold_predicate). No existing algebra/node semantics modified. Semantics: chain_is_simulated is now whole-chain LGG (one template common to ALL steps) instead of adjacent-pairwise congruence -- stricter and more correct; all 6 prior witnesses stay green by derivation. Added 5 discriminating produced-form witnesses (exact template + substitution list; falsified by a control flip). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…y/for_all Parent §3 review: a linearity enforcer must not itself re-spell a combinator. Both were hand-rolled folds -- chain_is_redundant is a disjunction-fold (= algebra.any), body_is_linear a conjunction-fold (= algebra.for_all). Replace with the existing single authorities (not reduce_or, which is a generic binary reduce, a different shape). Behavior identical; intent_linearity 6/6 + simulated_relationship 11/11 green by execution. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Resolve conflicts in the two lens files by keeping the #5599 anti_unify refactor (simulated_relationship now derives chain_is_simulated from the produced whole-chain generalization; intent_linearity uses algebra any/for_all) over main's prior congruent logic. Strip // comments from the 5 touched .dag files to satisfy the post-#5567 parser-wall (line comments are FailClosed on ingest); no in-string // present. All 17 lens_unit witnesses (11 simulated_relationship + 6 intent_linearity) green by execution on the merged tree. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 23, 2026
…td.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) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 23, 2026
…as a row (one engine, two binders) (#5594) * WIP: Consolidate structural_similarity into the intent_linearity registry as * 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) <noreply@anthropic.com> * 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) <noreply@anthropic.com> * 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) <noreply@anthropic.com> * WIP: Consolidate structural_similarity into the intent_linearity registry as --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Upgrade
v2.lens.simulated_relationshipfrom a Bool congruence check into a derivation over the produced minimal form of a statement chain: the anti-unification (least-general) generalization = a common template Node carrying^HOLEleaves where steps differ + the per-element substitution list.The producer is a new domain-agnostic shared kernel,
v2.std.anti_unification:anti_unify(a, b)— full LGG over any twoNodes. Always succeeds: a structural divergence (leaf-vs-leaf differ, leaf-vs-internal, kind/arity/label mismatch) becomes a^HOLE, never a failure.extract_fillings(template, element)— the subtree each element placed at each hole, in template order.anti_unify_chain(steps)— whole-chain template +per_elementsubstitution list.template_has_hole/fillings_all_leaves— consumer-side produced-form predicates.The kernel is domain-agnostic over
Node: a statement chain and a type-decl forest anti-unify by the same rules; only the binder (which Nodes are the peers to generalize) differs and lives at the caller.structural_similarity(type-decl layer) and the apply-half reuse this engine.The lens is now thin:
chain_is_simulated = length>=3 AND template_has_hole AND fillings_all_leaves.Semantics change (not a silent shift)
chain_is_simulatedis now whole-chain anti-unification (one template common to all steps) instead of the prior adjacent-pairwise congruence. Whole-chain is the stricter, more correct notion. All 6 prior witnesses stay green by derivation.Load-bearing additions (flagged for review)
Both are additive, following existing patterns — no existing algebra/node semantics modified:
src/v2/std/algebra.dag: two generic combinatorszip_map(pairing sibling ofzip_eq) andreduce_or(seed-from-first reduce). FreeMonoid variantmatchkept inside algebra per the cross-module generic-variant-pattern weakness.src/v2/std/anti_unification.dag: new module, sibling ofexact_structural_equality_zip_fold_predicate.Verification (by execution)
claim_batch --source-root src/v2over the lens_unit witnesses:intent_linearitylens (consumeschain_is_simulated): 6/6 green.Design + placement signed off by the lens author (parent, #5584 author).