# Add alpha-unique-atom: Alpha-Equivalence Deduplication Function

[aprilyab]

Summary

This PR introduces a new built-in function, alpha-unique-atom, to the PeTTa language. Unlike the existing unique-atom, which only removes syntactically identical atoms, alpha-unique-atom deduplicates 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-atom function 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:

!(alpha-unique-atom ((link $x human) (link $y human) (link $z human)))

Observed (incorrect) output with unique-atom:

((link $x human) (link $y human) (link $z human))

Expected output with alpha-unique-atom:

((link $a human))

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

• Added alpha-unique-atom as a new built-in, implemented in Prolog and registered in the PeTTa core.
• The function uses structural equality (=@=) to compare atoms, ensuring alpha-equivalent atoms are deduplicated.
• All other behavior remains unchanged; only the equality notion for deduplication is altered.

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:

• Basic duplicates with different variables
• Different functors and nested structures
• Mixed unique and duplicate elements
• Numbers, atoms, empty and single-element lists

Example test:

!(test (=alpha (alpha-unique-atom ((link $x human) (link $y human) (link $z human)))
               ((link $a human)))
       True)

Impact

• Enables correct deduplication for symbolic reasoning and pattern mining.
• Does not change the behavior of the existing unique-atom function, preserving backward compatibility for projects relying on its current semantics.

Related issues

Fixes unique-atom does not remove alpha-equivalent atoms#149

[patham9]

Well-done and well-tested! Thank you so much!!

[rTreutlein]

While i agree that this is an important function. I would generally prefer such things to be implemented in MeTTa directly.