2
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\begingroup$ 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 hal.archives-ouvertes.fr/hal-01670363v2/document $\endgroup$
    – Bartosz Bednarczyk
    Oct 20, 2020 at 8:06
  • $\begingroup$ If you only look at closed terms, you can use de Bruijn indices, so regular tree might be enough $\endgroup$
    – xavierm02
    Oct 20, 2020 at 21:39
  • $\begingroup$ @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? $\endgroup$
    – Joey Eremondi
    Oct 20, 2020 at 22:46
  • $\begingroup$ Variables need to be encoded as string / trees in some way, for example Peano, yes $\endgroup$
    – xavierm02
    Oct 21, 2020 at 7:30

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.