I'm wondering if there has been any research done into automata that accept languages of trees that can bind arbitrary variables, and are considered equal under alpha equivalence.
I've found so far:
- Dependency Tree Automata which seems to only support a finite set of bound variables, given beforehand
- Nominal Regular Languages which supports an unbounded number of variables, but only on words, not on trees. So it can't support i.e. sets of $\lambda$-calculus terms, just sequences of commands.
- Higher-order model checking which seems to only support checking of there is 0 or 1 trees in a given language, but doesn't do i.e. intersection, union, or other set operations.
I'm basically looking for a way to categorize languages of $\lambda$-calculus terms, but only considering structure i.e. I don't need to reason about $\beta$-reductions. I need a class of languages that is closed under union and intersection, with decidable emptiness checking.
Does anything like this exist?