# Add alpha-unique-atom: Alpha-Equivalence Deduplication Function#150
# Add alpha-unique-atom: Alpha-Equivalence Deduplication Function#150aprilyab wants to merge 2 commits into
Conversation
- Added extensive tests for alpha-unique-atom using =alpha for alpha-equivalence - Covers: - Basic duplicates with distinct variables - Different functors and nested structures - Mixed unique and duplicate elements - Numbers, atoms, empty, and single-element lists
- Implemented alpha-unique-atom/2 predicate in metta.pl to remove duplicates from a list using structural (alpha) equivalence (=@=/2), rather than syntactic equality. - Added helper predicates alpha_list_to_set/2 and alpha_member_eq/2 to support alpha-equivalent deduplication. - Registered alpha-unique-atom as a MeTTa function for use in user code.
There was a problem hiding this comment.
Pull request overview
This PR adds a new PeTTa built-in, alpha-unique-atom, intended to deduplicate atoms by alpha-equivalence (variant/structural equality under variable renaming) to address issue #149.
Changes:
- Added
alpha-unique-atomto the Prolog built-ins and registered it in the core function table. - Implemented alpha-equivalence-based list deduplication via helper predicates using
=@=comparison. - Added an examples-based test suite covering common alpha-dedup cases and edge cases.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 4 comments.
| File | Description |
|---|---|
| src/metta.pl | Implements and registers alpha-unique-atom using a custom alpha-equivalence set conversion. |
| examples/test_alpha_unique_atom.metta | Adds test cases validating alpha-equivalence dedup behavior across structures and primitives. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| first([A, _], A). | ||
| 'second-from-pair'([_, A], A). | ||
| 'unique-atom'(A, B) :- list_to_set(A, B). | ||
| 'alpha-unique-atom'(A, B) :- alpha_list_to_set(A, B). |
There was a problem hiding this comment.
Unlike unique-atom/2 (list_to_set/2), alpha-unique-atom/2 will simply fail if A is not a proper list (because alpha_list_to_set/2 only matches []/[H|T]) rather than raising a type error. If callers rely on the existing error behavior for invalid inputs, consider adding explicit list validation (e.g., must_be(list, A)) so alpha-unique-atom behaves consistently with unique-atom.
| 'alpha-unique-atom'(A, B) :- alpha_list_to_set(A, B). | |
| 'alpha-unique-atom'(A, B) :- must_be(list, A), alpha_list_to_set(A, B). |
| alpha_list_to_set([], []). | ||
| alpha_list_to_set([H|T], R) :- | ||
| ( alpha_member_eq(H, T) -> | ||
| alpha_list_to_set(T, R) | ||
| ; | ||
| alpha_list_to_set(T, RT), | ||
| R = [H|RT] | ||
| ). |
There was a problem hiding this comment.
alpha_list_to_set/2 performs an O(n^2) pairwise scan (alpha_member_eq/2 for each element). If alpha-unique-atom is expected to run on large atom lists (e.g., reasoning outputs), this could become a hot spot compared to the built-in list_to_set/2. Consider using a canonicalized representation for alpha-equivalence (e.g., copy_term + numbervars) and tracking seen keys in an assoc/dict to get closer to O(n).
| !(test (=alpha (alpha-unique-atom (1 2 2 3 1 4 4 5)) | ||
| (2 3 1 4 5)) | ||
| True) | ||
|
|
||
| !(test (=alpha (alpha-unique-atom (a b a c b d e a)) | ||
| (c b d e a)) | ||
| True) |
There was a problem hiding this comment.
The expected results here (e.g., (1 2 2 3 1 4 4 5) -> (2 3 1 4 5) and (a b a c b d e a) -> (c b d e a)) encode “keep last occurrence” semantics. If alpha-unique-atom is meant to mirror unique-atom and only change the equality notion (as described in the PR), these expectations should be updated to match first-occurrence preservation instead.
| alpha_list_to_set([H|T], R) :- | ||
| ( alpha_member_eq(H, T) -> | ||
| alpha_list_to_set(T, R) | ||
| ; | ||
| alpha_list_to_set(T, RT), |
There was a problem hiding this comment.
alpha_list_to_set/2 currently removes an element if an alpha-equivalent one exists later in the list, which means it keeps the last occurrence of each equivalence class. This differs from unique-atom (list_to_set/2), which keeps the first occurrence, and it contradicts the PR description that “only the equality notion” changes. Consider rewriting alpha_list_to_set/2 to scan left-to-right while tracking already-seen alpha-variants so the first representative is preserved (or update the docs/tests if last-occurrence semantics are intended).
Summary
This PR introduces a new built-in function,
alpha-unique-atom, to the PeTTa language. Unlike the existingunique-atom, which only removes syntactically identical atoms,alpha-unique-atomdeduplicates atoms using alpha-equivalence (structural equality with variable renaming). This ensures that atoms differing only by variable names are treated as duplicates and only one representative is kept.Problem and reproduction
The current
unique-atomfunction in PeTTa does not consider alpha-equivalence, leading to unexpected duplicates when atoms differ only by variable names. This causes issues in symbolic reasoning and pattern mining tasks, where structurally identical atoms should be considered equal.Example:
Input:
Observed (incorrect) output with unique-atom:
Expected output with alpha-unique-atom:
Root cause
unique-atom only checks for syntactic equality, not structural (alpha) equivalence. As a result, atoms that are structurally identical but use different variable names are not deduplicated.
What I changed
alpha-unique-atomas a new built-in, implemented in Prolog and registered in the PeTTa core.=@=) to compare atoms, ensuring alpha-equivalent atoms are deduplicated.Why this fix
Alpha-equivalence is the correct equality notion for deduplication in symbolic reasoning: two atoms that only differ by the names of their variables are treated as the same pattern, while distinct syntactic patterns are preserved.
Testing & validation
A comprehensive test suite is included, covering:
Example test:
Impact
unique-atomfunction, preserving backward compatibility for projects relying on its current semantics.Related issues
Fixes unique-atom does not remove alpha-equivalent atoms#149