<p>I think section 3.1 (titled &quot;Nominal tree automata&quot;) of this paper: <a href="https://drops.dagstuhl.de/opus/volltexte/2019/11434/" rel="nofollow noreferrer">https://drops.dagstuhl.de/opus/volltexte/2019/11434/</a> may be what you're looking for, they use λ-terms as their example.</p>
<p>In addition to this, here are two naive ideas for defining &quot;regular languages of λ-terms up to α-equivalence&quot;. I have no idea whether they give well-behaved notions; in both cases intersections and unions work, but I don't know about emptiness checking.</p>
<ul>
<li><p>The first solution is to represent your λ-terms as relational structures: a binary tree + a relation between variables and their binders. On such structures you can consider the predicates definable in Monadic Second-Order logic; in fact there is a huge literature on MSO over graphs, and in the case of words and trees (without binders) it coincides with recognition by finite automata.</p>
</li>
<li><p>The second is a bit more complicated and unconventional. First, note that untyped closed λ-terms modulo α-equivalence are in canonical bijection with the simply typed inhabitants of LAM = (o → o → o) → ((o → o) → o) → o modulo βη-conversion, where o is a base type (let's say that our grammar of simple types is A,B ::= o | A → B). This is kind of a generalized Church encoding, the o → o → o part corresponds to application (compare with the encoding of binary trees (o → o → o) → o → o) while the (o → o) → o corresponds to abstraction (this is reminiscent of higher-order abstract syntax). For instance (λx.xx)(λx.xx) would be encoded as λa.λl.a(l(λx.axx))(l(λx.axx)). Then there is a notion of &quot;recognizable language of closed inhabitants of a simple type modulo βη&quot; due to Salvati: <a href="https://link.springer.com/chapter/10.1007/978-3-642-02261-6_5" rel="nofollow noreferrer">https://link.springer.com/chapter/10.1007/978-3-642-02261-6_5</a> which you could apply to the type LAM.</p>
</li>
</ul>

CC BY-SA 4.0
2022-11-03T00:19:54.657Z
2022-11-03T00:19:54.657Z
Lê Thành Dũng 'Tito' Nguyễn
<p>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.</p>
<p>I've found so far:</p>
<ul>
<li><a href="http://homepages.inf.ed.ac.uk/cps/fossacs09.pdf" rel="nofollow noreferrer">Dependency Tree Automata</a> which seems to only support a finite set of bound variables, given beforehand</li>
<li><a href="https://www.cs.le.ac.uk/people/et52/LAVORI/fossacs12_ext.pdf" rel="nofollow noreferrer">Nominal Regular Languages</a> which supports an unbounded number of variables, but only on words, not on trees. So it can't support i.e. sets of <span class="math-container">$\lambda$</span>-calculus terms, just sequences of commands.</li>
<li><a href="http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/LICS15.pdf" rel="nofollow noreferrer">Higher-order model checking</a> 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.</li>
</ul>
<p>I'm basically looking for a way to categorize languages of <span class="math-container">$\lambda$</span>-calculus terms, but only considering structure i.e. I don't need to reason about <span class="math-container">$\beta$</span>-reductions. I need a class of languages that is closed under union and intersection, with decidable emptiness checking.</p>
<p>Does anything like this exist?</p>

CC BY-SA 4.0
2020-10-20T08:06:43.683Z
I'm not sure about lambda calculus but what about automata working on data-trees? Are they similar? The examples are Alternating Tree 1-Register Automata (ATRA), Class Automata on data trees, Bottom-up 1-register alternating Data Automata (known as BUDA) etc. Check the survey of Diego Figueira on XPath on trees with data https://hal.archives-ouvertes.fr/hal-01670363v2/document
Bartosz Bednarczyk
CC BY-SA 4.0
2020-10-20T21:39:57.390Z
If you only look at closed terms, you can use de Bruijn indices, so regular tree might be enough
xavierm02
CC BY-SA 4.0
2020-10-20T22:46:48.663Z
@xavierm02 But that still requires an infinite alphabet of names (i.e. a Nominal Set) to represent, right? Or do you just Peano-encode the indices?
Joey Eremondi
CC BY-SA 4.0
2020-10-21T07:30:29.037Z
Variables need to be encoded as string / trees in some way, for example Peano, yes
xavierm02
<reference-request><automata-theory><pl.programming-languages><lambda-calculus><program-verification>
Nominal Tree Languages i.e. with Binders and Infinite Symbols?
Joey Eremondi
# Nominal Tree Languages i.e. with Binders and Infinite Symbols?

(Asked by: username_0 on 2020-10-19)

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](http://homepages.inf.ed.ac.uk/cps/fossacs09.pdf) which seems to only support a finite set of bound variables, given beforehand
* [Nominal Regular Languages](https://www.cs.le.ac.uk/people/et52/LAVORI/fossacs12_ext.pdf) 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](http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/LICS15.pdf) 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?

**Tags:** reference-request, automata-theory, pl.programming-languages, lambda-calculus, program-verification
> **Comments:**
> **username_1**: I'm not sure about lambda calculus but what about automata working on data-trees? Are they similar? The examples are Alternating Tree 1-Register Automata (ATRA), Class Automata on data trees, Bottom-up 1-register alternating Data Automata (known as BUDA) etc. Check the survey of Diego Figueira on XPath on trees with data https://hal.archives-ouvertes.fr/hal-01670363v2/document  
> **username_2**: If you only look at closed terms, you can use de Bruijn indices, so regular tree might be enough  
> **username_0**: @xavierm02 But that still requires an infinite alphabet of names (i.e. a Nominal Set) to represent, right? Or do you just Peano-encode the indices?  
> **username_2**: Variables need to be encoded as string / trees in some way, for example Peano, yes  

---

## 1 answers

### Answer by username_3 on 2022-11-03. Score: 4

I think section 3.1 (titled "Nominal tree automata") of this paper: <https://drops.dagstuhl.de/opus/volltexte/2019/11434/> may be what you're looking for, they use λ-terms as their example.

In addition to this, here are two naive ideas for defining "regular languages of λ-terms up to α-equivalence". I have no idea whether they give well-behaved notions; in both cases intersections and unions work, but I don't know about emptiness checking.

* The first solution is to represent your λ-terms as relational structures: a binary tree + a relation between variables and their binders. On such structures you can consider the predicates definable in Monadic Second-Order logic; in fact there is a huge literature on MSO over graphs, and in the case of words and trees (without binders) it coincides with recognition by finite automata.
* The second is a bit more complicated and unconventional. First, note that untyped closed λ-terms modulo α-equivalence are in canonical bijection with the simply typed inhabitants of LAM = (o → o → o) → ((o → o) → o) → o modulo βη-conversion, where o is a base type (let's say that our grammar of simple types is A,B ::= o | A → B). This is kind of a generalized Church encoding, the o → o → o part corresponds to application (compare with the encoding of binary trees (o → o → o) → o → o) while the (o → o) → o corresponds to abstraction (this is reminiscent of higher-order abstract syntax). For instance (λx.xx)(λx.xx) would be encoded as λa.λl.a(l(λx.axx))(l(λx.axx)). Then there is a notion of "recognizable language of closed inhabitants of a simple type modulo βη" due to Salvati: <https://link.springer.com/chapter/10.1007/978-3-642-02261-6_5> which you could apply to the type LAM.


---

