Skip to content

feat(math): add greedoids domain with recognize, rank, bases, basic words, convex geometry (#1915) - #2031

Open
morluto wants to merge 2 commits into
mainfrom
agent/greedoids-antimatroids-1915
Open

feat(math): add greedoids domain with recognize, rank, bases, basic words, convex geometry (#1915)#2031
morluto wants to merge 2 commits into
mainfrom
agent/greedoids-antimatroids-1915

Conversation

@morluto

@morluto morluto commented Aug 18, 2026

Copy link
Copy Markdown
Owner

Closes #1915.

Summary

Add the greedoids domain implementing exact, bounded, deterministic greedoid/antimatroid operations over an immutable feasible-set family. This is the missing finite accessibility/exchange layer between Jacobian's existing set systems, matroids (#1707), closure systems/formal concept analysis (#1896), posets, graphs, and words.

Design and library choices

The domain uses an exact enumeration kernel over the complete feasible-set family. No caller-supplied membership oracle or heuristic exchange flag is allowed — the complete family is authoritative and omission means exact infeasibility, not unknown. Per the issue, this does not propose a greedy optimization service, arbitrary independence/closure callback, matroid/greedoid recognition from an oracle, interactive learning-space workflow, approximate knowledge-space mining, general convex optimization, or realizability/classification search.

Representation (values.py). FiniteFeasibleSetSystem carries a unique-labelled ground set and the complete duplicate-free feasible-set family (each feasible set is a sorted tuple of ground indices). The value parses only well-formed families: unique ground labels, sorted duplicate-free feasible sets, in-range indices, and a duplicate-free family. The empty-set convention is explicit.

Operations (operations.py). All functions are deterministic and complete for accepted values.

  • recognize — exhaust the accessibility and exchange axioms over the complete family. Return GREEDOID with rank and bases, or NOT_A_GREEDOID with the first exact obstruction under deterministic order (missing empty set, inaccessible feasible set, exchange violation). A sample of exchange pairs cannot return GREEDOID.
  • rankr(X) = max{|F| : F feasible and F ⊆ X}.
  • bases — the complete maximal feasible-set family with the common rank.
  • basic_word_profile — whether a distinct-element word has every prefix set feasible (BASIC_WORD), or the first infeasible prefix (NOT_A_BASIC_WORD). Repeated or foreign elements are boundary-invalid.
  • antimatroid_to_convex_geometry / convex_geometry_to_antimatroid — the complementary closed-set family C = {E\F : F in F}, an intersection-closed finite closure system satisfying anti-exchange, plus the feasible→closed complement map. The two conversions are inverse under exact ground identity.

Invariances verified by tests

  • A two-element full-support antimatroid is recognized as a greedoid with rank 2 and basis {0,1}.
  • Missing empty set, inaccessible feasible set, and exchange violation each produce the correct named obstruction.
  • basic_word_profile((0,1)) is a full basic word; (0,0) is rejected with repeated_element.
  • The complementary convex geometry of the two-element antimatroid contains both the empty set and the full ground set (top and bottom of the closed-set lattice), and the complement map reverses inclusion.

Validation

  • make check lint + typecheck clean; 24 focused domain tests; all 1110 tests/math, 67 tests/catalog/tests/math/public_api/tests/dispatch tests pass.
  • Frozen admission baselines updated (KEEP 239→244, candidates 399→404) and the greedoids schema-snapshot fragment added (5 operations).

Continue this on Linzumi

…ords, convex geometry

Add the greedoids domain implementing exact, bounded, deterministic
greedoid/antimatroid operations over an immutable feasible-set family:

- greedoid.recognize.compute: exhaust the accessibility and exchange axioms
  over the complete feasible-set family. Return GREEDOID with rank and bases,
  or NOT_A_GREEDOID with the first exact obstruction under deterministic order
  (missing empty set, inaccessible feasible set, exchange violation). A
  sample of exchange pairs cannot return GREEDOID.
- greedoid.rank.compute: r(X) = max{|F| : F feasible and F subseteq X}.
- greedoid.bases.compute: the complete maximal feasible-set family with the
  common rank.
- greedoid.basic_word.profile.compute: whether a distinct-element word has
  every prefix set feasible (BASIC_WORD), or the first infeasible prefix
  (NOT_A_BASIC_WORD). Repeated or foreign elements are boundary-invalid.
- greedoid.convex_geometry.compute: the complementary closed-set family
  C = {E\F : F in F} of a full-support antimatroid, an intersection-closed
  finite closure system satisfying anti-exchange, plus the feasible->closed
  complement map.

The FiniteFeasibleSetSystem value parses only well-formed families: unique
ground labels, sorted duplicate-free feasible sets, in-range indices, and a
duplicate-free family. The complete family is authoritative; omission means
exact infeasibility, not unknown. No caller-supplied membership oracle or
heuristic exchange flag is allowed.

Closes #1915
- Add greedoids to the root jacobian.math exports and ROOT_MATH_DOMAINS.
- Import the domain TOOLS and ADMISSIONS in catalog/builtins.py.
- Update the frozen admission baselines (KEEP 239->244, candidates
  399->404) and add the greedoids schema-snapshot fragment.
- Add 24 focused tests (recognition, rank/bases, basic-word profile,
  convex geometry, validation, native helpers).
@chatgpt-codex-connector

Copy link
Copy Markdown

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

@morluto morluto left a comment

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review verdict: blocked — several operations assume a greedoid/antimatroid that the request never establishes

FiniteFeasibleSetSystem deliberately represents an arbitrary complete set family. That is appropriate for recognize, but the other public operations accept the same unconstrained value while returning theorem-strengthened greedoid/antimatroid semantics.

1. convex_geometry.compute can return something that is not a closure system

antimatroid_to_convex_geometry() merely complements every supplied feasible set. It never checks:

  • the greedoid/accessibility axioms;
  • union closure (the antimatroid condition);
  • full support (union(F) = E).

For example, on E={0,1} with feasible family (), (0,), (1,), the operation returns closed sets (0,1), (1,), (0,). This family omits the empty set and is not intersection-closed because (0,) ∩ (1,) = (). The result is therefore not a convex geometry despite the operation ID and description.

Require and replay the full antimatroid precondition before conversion, returning a named obstruction or rejecting the request. The native inverse helper has the symmetric issue: it complements arbitrary tuples without validating a convex geometry or even index well-formedness.

2. bases() computes maximum-cardinality feasible sets, not maximal feasible sets

Those coincide for a greedoid, but only after the greedoid axioms are known. On the PR's own exchange-violating family

(), (0,), (1,), (0,1), (2,)

the inclusion-maximal feasible sets are (0,1) and (2,); this code returns only (0,1). Either bind RankRequest/BasesRequest to a validated greedoid value, or expose generic set-system semantics and stop claiming the common-rank theorem.

3. Ground-subset requests are not validated

subset accepts duplicates and foreign indices, then frozenset() silently collapses/retains them. A request such as (0,0,999) is not a subset of the ground set but receives a normal rank/bases answer. Add uniqueness and range validation.

4. Rank-zero fullness is wrong

basic_word_profile() defines is_full = len(word) == rank and rank > 0. In a rank-zero greedoid, the empty word is the full basic word and the empty set is its basis; the extra rank > 0 makes this false.

The exhaustive recognition kernel itself appears mathematically sound. The fix is to make the recognized structure an actual input invariant for operations whose semantics depend on the greedoid or antimatroid theorems.

morluto commented Aug 18, 2026

Copy link
Copy Markdown
Owner Author

Deep review summary

Verdict: REQUEST CHANGES — several operations assume a validated greedoid or antimatroid although the request accepts an arbitrary set family.

FiniteFeasibleSetSystem is appropriately generic for recognize, but the other operations return theorem-strengthened semantics without establishing their hypotheses.

1. convex_geometry.compute can return a non-closure-system

The conversion only complements supplied feasible sets. It does not require accessibility, exchange, union closure, or full support. On E={0,1} with feasible family (), (0,), (1,), it returns closed sets (0,1), (1,), (0,); the empty set is missing and (0,) ∩ (1,) = () is absent. This is not a convex geometry.

Require and replay the full antimatroid precondition before conversion. The inverse helper needs symmetric validation.

2. bases() computes maximum-cardinality sets, not inclusion-maximal sets

Those coincide only for a greedoid. On

(), (0,), (1,), (0,1), (2,)

the maximal feasible sets are (0,1) and (2,); the implementation returns only (0,1). Bind rank/bases operations to a validated greedoid value, or expose generic set-system semantics without the common-rank theorem.

3. Ground-subset requests are not validated

Values such as (0,0,999) are accepted and silently converted to a frozenset, yielding a normal answer for something that is not a ground subset. Enforce uniqueness and range.

4. Rank-zero fullness is wrong

is_full = len(word) == rank and rank > 0 marks the empty word as non-full in a rank-zero greedoid. The empty word is the full basic word there; remove the extra rank > 0 condition.

The exhaustive recognition kernel itself appears mathematically sound. The structural fix is to make recognition an input invariant wherever the downstream semantics rely on greedoid or antimatroid theorems.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[Greedoids and antimatroids] Add exact feasible-set axioms, rank profiles, minors, basic words, convex geometries, and rooted circuits

1 participant