-
Notifications
You must be signed in to change notification settings - Fork 39
# Add alpha-unique-atom: Alpha-Equivalence Deduplication Function #150
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,59 @@ | ||
| ; Strong test suite for alpha-unique-atom | ||
|
|
||
| ; 1 Basic duplicates with different variables | ||
| !(test (=alpha (alpha-unique-atom ((link $x human) (link $y human) (link $z human))) | ||
| ((link $a human))) | ||
| True) | ||
|
|
||
| !(test (=alpha (alpha-unique-atom ((parent $a human) (parent $b human) (child $c human))) | ||
| ((parent $d human) (child $e human))) | ||
| True) | ||
|
|
||
| ; 2 Different functors (should all remain) | ||
| !(test (=alpha (alpha-unique-atom ((parent $x human) (child $y human) (friend $z human))) | ||
| ((parent $a human) (child $b human) (friend $c human))) | ||
| True) | ||
|
|
||
| !(test (=alpha (alpha-unique-atom ((likes $x) (hates $y) (knows $z))) | ||
| ((likes $a) (hates $b) (knows $c))) | ||
| True) | ||
|
|
||
| ; 3 Nested structures | ||
| !(test (=alpha (alpha-unique-atom ((link (foo $x) human) (link (foo $y) human) (link (bar $z) human))) | ||
| ((link (foo $a) human) (link (bar $b) human))) | ||
| True) | ||
|
|
||
| !(test (=alpha (alpha-unique-atom ((parent (child $x) human) (parent (child $y) human) (parent (child $x) human))) | ||
| ((parent (child $a) human))) | ||
| True) | ||
|
|
||
| ; 4 Mix of unique and duplicates | ||
| !(test (=alpha (alpha-unique-atom ((link $x human) (parent $x human) (link $y human) (parent $z human) (link $x human))) | ||
| ((parent $a human) (link $b human))) | ||
| True) | ||
|
|
||
| !(test (=alpha (alpha-unique-atom ((foo $x) (foo $y) (bar $x) (foo $x) (bar $y))) | ||
| ((foo $a) (bar $b))) | ||
| True) | ||
|
|
||
| ; 5 Numbers and atoms | ||
| !(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) | ||
|
|
||
| ; 6 Empty and single-element lists | ||
| !(test (=alpha (alpha-unique-atom ()) | ||
| ()) | ||
| True) | ||
|
|
||
| !(test (=alpha (alpha-unique-atom (1)) | ||
| (1)) | ||
| True) | ||
|
|
||
| !(test (=alpha (alpha-unique-atom ((link $x human))) | ||
| ((link $a human))) | ||
| True) | ||
| Original file line number | Diff line number | Diff line change | ||||
|---|---|---|---|---|---|---|
|
|
@@ -112,6 +112,20 @@ | |||||
| 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). | ||||||
|
||||||
| '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). |
Copilot
AI
Mar 27, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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).
Copilot
AI
Mar 27, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.