q_{init} (є) | q_{1} (a (X)) :- q_{init} (X) | |
q_{1} (b (X)) :- q_{1} (X) | q_{init} (X) :- q_{1} (X) |
To define the semantics of tree automata, the simplest is just to describe their translation to Horn clauses. Each transition again gives rise to exactly one clause:
q_{even} (O) | q_{even} (S (X)) :- q_{odd} (X) | q_{odd} (S (X)) :- q_{even} (X) |
q_{list−even} (cons (X, Y)) :- q_{even} (X), q_{list−even} (Y) | q_{list−even} (nil) |