In my quest to understand the theory of recursive types in more detail, the notion of regular tree languages and [[Tree automaton|Tree Automata]] has cropped up. These have been used, amongst other things, for describing [[XML schema|XML schemas]]. They are also useful for describing recursive types as well!
A nice example of a regular tree language is one for minimising boolean expressions. The constructors of the language are
Or/2. The regular tree language looks thus:
Expr -> True | False | Not(Expr) | And(Expr,Expr)
This should look pretty familiar to anyone who’s studied context-free and/or regular languages before. A simple (deterministic) bottom-up tree automata can then be defined using the following state transitions:
True --> q1 Not(q0) --> q1 False --> q0 Not(q1) --> q0 And(q0,q0) --> q0 And(q1,q0) --> q0 And(q0,q1) --> q0 And(q1,q1) --> q1
I guess the interesting question is how this differs from general regular languages. They appear to be very similar — for example, they support minimisation, intersection and union (amongst other things). Likewise, the relationship with context-free grammar is interesting … although I haven’t got to the bottom of that yet.
Anyway, a good reference on this subject is the book Tree Automata Techniques and Applications.