Editing Tree automaton (section)

== Examples ==

===Bottom-up automaton accepting boolean lists===
Employing coloring to distinguish members of ''F'' and ''Q'', and using the ranked alphabet ''F''={ {{color|#800000|''false''}},{{color|#800000|''true''}},{{color|#800000|''nil''}},{{color|#800000|''cons''}}(.,.) }, with {{color|#800000|''cons''}} having arity 2 and all other symbols having arity 0, a bottom-up tree automaton accepting the set of all finite lists of boolean values can be defined as (''Q'', ''F'', ''Q''<sub>''f''</sub>, Δ) with {{math|1=''Q'' = { {{color|#008000|''Bool''}},{{color|#008000|''BList''}} }, ''Q''<sub>''f''</sub> = { {{color|#008000|''BList''}} },}} and Δ consisting of the rules

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
:{|
|-
| {{color|#800000|''false''}} || → || {{color|#008000|''Bool''}}({{color|#800000|''false''}}) || (1),
|-
| {{color|#800000|''true''}} || → || {{color|#008000|''Bool''}}({{color|#800000|''true''}}) || (2),
|-
| {{color|#800000|''nil''}} || → || {{color|#008000|''BList''}}({{color|#800000|''nil''}}) || (3), and
|-
| {{color|#800000|''cons''}}({{color|#008000|''Bool''}}(x<sub>1</sub>),{{color|#008000|''BList''}}(x<sub>2</sub>)) || → || {{color|#008000|''BList''}}({{color|#800000|''cons''}}(x<sub>1</sub>,x<sub>2</sub>)) &nbsp; &nbsp; &nbsp; || (4).
|}

In this example, the rules can be understood intuitively as assigning to each term its type in a bottom-up manner; e.g. rule (4) can be read as "A term {{color|#800000|''cons''}}(''x''<sub>1</sub>,''x''<sub>2</sub>) has type {{color|#008000|''BList''}}, provided ''x''<sub>1</sub> and ''x''<sub>2</sub> has type {{color|#008000|''Bool''}} and {{color|#008000|''BList''}}, respectively".
An accepting example run is

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
:{|
|-
|
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#800000|''nil''}}
| ))
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''nil''}})
| ))
| by (3)
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''true''}}),
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''nil''}})
| ))
| by (2)
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#800000|''nil''}}
| )))
| by (4)
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''false''}}),
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#800000|''nil''}}
| )))
| by (1)
|-
| ⇒
| ALIGN=RIGHT | {{color|#008000|''BList''}}({{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''true''}},
| ALIGN=RIGHT | {{color|#800000|''nil''}}
| ))) &nbsp; &nbsp; &nbsp;
| by (4), accepted.
|}

Cf. the derivation of the same term from a regular tree grammar corresponding to the automaton, shown at [[Regular tree grammar#Examples]].

A rejecting example run is

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
:{|
|-
|
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#800000|''true''}}
| )
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#800000|''false''}},
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''true''}})
| )
| by (1)
|-
| ⇒
| ALIGN=RIGHT | {{color|#800000|''cons''}}(
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''false''}}),
| ALIGN=RIGHT | {{color|#008000|''Bool''}}({{color|#800000|''true''}})
| ) &nbsp; &nbsp; &nbsp;
| by (2), no further rule applicable.
|}
Intuitively, this corresponds to the term {{color|#800000|''cons''}}({{color|#800000|''false''}},{{color|#800000|''true''}}) not being well-typed.

===Top-down automaton accepting multiples of 3 in binary notation===

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
{| class=wikitable style="float:right;"
|-
!
! ALIGN=center | '''(A)'''
! ALIGN=center | '''(B)'''
! ALIGN=center | '''(C)'''
! ALIGN=center | '''(D)'''
|-
!
! ALIGN=center | [[Regular grammar#Strictly regular grammars|'''String'''<BR>'''grammar''']]<BR>'''rules'''
! ALIGN=center | [[Deterministic finite automaton#Formal definition|'''String'''<BR>'''automaton''']]<BR>'''transitions'''
! ALIGN=center | '''Tree'''<BR>'''automaton'''<BR>'''transitions'''
! ALIGN=center | [[Regular tree grammar#Definition|'''Tree'''<BR>'''grammar''']]<BR>'''rules'''
|-
| <!---line numbers--->
{|
|-
! 0
|-
! 1
|-
! 2
|-
! 3
|-
! 4
|-
! 5
|-
! 6
|}
| <!---string grammar--->
{| 
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || ε
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|0}} {{color|#008000|''S''<sub>0</sub>}}
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|1}} {{color|#008000|''S''<sub>1</sub>}}
|- 
| {{color|#008000|''S''<sub>1</sub>}} || → || {{color|#800000|0}} {{color|#008000|''S''<sub>2</sub>}}
|- 
| {{color|#008000|''S''<sub>1</sub>}} || → || {{color|#800000|1}} {{color|#008000|''S''<sub>0</sub>}}
|- 
| {{color|#008000|''S''<sub>2</sub>}} || → || {{color|#800000|0}} {{color|#008000|''S''<sub>1</sub>}}
|- 
| {{color|#008000|''S''<sub>2</sub>}} || → || {{color|#800000|1}} {{color|#008000|''S''<sub>2</sub>}}
|}
| <!---string automaton--->
{| 
|- 
| &nbsp;
|- 
| δ({{color|#008000|''S''<sub>0</sub>}},{{color|#800000|0}}) || = {{color|#008000|''S''<sub>0</sub>}}
|- 
| δ({{color|#008000|''S''<sub>0</sub>}},{{color|#800000|1}}) || = {{color|#008000|''S''<sub>1</sub>}}
|- 
| δ({{color|#008000|''S''<sub>1</sub>}},{{color|#800000|0}}) || = {{color|#008000|''S''<sub>2</sub>}}
|- 
| δ({{color|#008000|''S''<sub>1</sub>}},{{color|#800000|1}}) || = {{color|#008000|''S''<sub>0</sub>}}
|- 
| δ({{color|#008000|''S''<sub>2</sub>}},{{color|#800000|0}}) || = {{color|#008000|''S''<sub>1</sub>}}
|- 
| δ({{color|#008000|''S''<sub>2</sub>}},{{color|#800000|1}}) || = {{color|#008000|''S''<sub>2</sub>}}
|}
| <!--- tree automaton--->
{|
|- 
| {{color|#008000|''S''<sub>0</sub>}}({{color|#800000|''nil''}}) || → || {{color|#800000|''nil''}}
|- 
| {{color|#008000|''S''<sub>0</sub>}}({{color|#800000|0}}(x)) || → || {{color|#800000|0}}({{color|#008000|''S''<sub>0</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>0</sub>}}({{color|#800000|1}}(x)) || → || {{color|#800000|1}}({{color|#008000|''S''<sub>1</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>1</sub>}}({{color|#800000|0}}(x)) || → || {{color|#800000|0}}({{color|#008000|''S''<sub>2</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>1</sub>}}({{color|#800000|1}}(x)) || → || {{color|#800000|1}}({{color|#008000|''S''<sub>0</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>2</sub>}}({{color|#800000|0}}(x)) || → || {{color|#800000|0}}({{color|#008000|''S''<sub>1</sub>}}(x))
|- 
| {{color|#008000|''S''<sub>2</sub>}}({{color|#800000|1}}(x)) || → || {{color|#800000|1}}({{color|#008000|''S''<sub>2</sub>}}(x))
|}
| <!--- tree grammar--->
{|
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|''nil''}}
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|0}}({{color|#008000|''S''<sub>0</sub>}})
|- 
| {{color|#008000|''S''<sub>0</sub>}} || → || {{color|#800000|1}}({{color|#008000|''S''<sub>1</sub>}})
|- 
| {{color|#008000|''S''<sub>1</sub>}} || → || {{color|#800000|0}}({{color|#008000|''S''<sub>2</sub>}})
|- 
| {{color|#008000|''S''<sub>1</sub>}} || → || {{color|#800000|1}}({{color|#008000|''S''<sub>0</sub>}})
|- 
| {{color|#008000|''S''<sub>2</sub>}} || → || {{color|#800000|0}}({{color|#008000|''S''<sub>1</sub>}})
|- 
| {{color|#008000|''S''<sub>2</sub>}} || → || {{color|#800000|1}}({{color|#008000|''S''<sub>2</sub>}})
|}
|}

{| style="float:right;"
| [[File:DFA example multiplies of 3.svg|thumb|[[Deterministic finite automaton|Deterministic finite (string) automaton]] accepting multiples of 3 in binary notation]]
|}

Using the same colorization as above, this example shows how tree automata generalize ordinary string automata.
The finite deterministic string automaton shown in the picture accepts all strings of binary digits that denote a multiple of 3.
Using the notions from [[Deterministic finite automaton#Formal definition]], it is defined by:
* the set ''Q'' of states being { {{color|#008000|''S''<sub>0</sub>}}, {{color|#008000|''S''<sub>1</sub>}}, {{color|#008000|''S''<sub>2</sub>}} },
* the input alphabet being { {{color|#800000|0}}, {{color|#800000|1}} },
* the initial state being {{color|#008000|''S''<sub>0</sub>}},
* the set of final states being { {{color|#008000|''S''<sub>0</sub>}} }, and
* the transitions being as shown in column (B) of the table.

In the tree automaton setting, the input alphabet is changed such that the symbols {{color|#800000|0}} and {{color|#800000|1}} are both unary, and a nullary symbol, say {{color|#800000|''nil''}} is used for tree leaves.
For example, the binary string "{{color|#800000|110}}" in the string automaton setting corresponds to the term "{{color|#800000|1}}({{color|#800000|1}}({{color|#800000|0}}({{color|#800000|''nil''}})))" in the tree automaton setting; this way, strings can be generalized to trees, or terms.
The top-down finite tree automaton accepting the set of all terms corresponding to multiples of 3 in binary string notation is then defined by:
* the set ''Q'' of states being still { {{color|#008000|''S''<sub>0</sub>}}, {{color|#008000|''S''<sub>1</sub>}}, {{color|#008000|''S''<sub>2</sub>}} },
* the ranked input alphabet being { {{color|#800000|0}}, {{color|#800000|1}}, {{color|#800000|''nil''}} }, with ''Arity''({{color|#800000|0}})=''Arity''({{color|#800000|1}})=1 and ''Arity''({{color|#800000|''nil''}})=0, as explained,
* the set of initial states being { {{color|#008000|''S''<sub>0</sub>}} }, and
* the transitions being as shown in column (C) of the table.
For example, the tree "{{color|#800000|1}}({{color|#800000|1}}({{color|#800000|0}}({{color|#800000|''nil''}})))" is accepted by the following tree automaton run:

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
{|
|-
|    || {{color|#008000|''S''<sub>0</sub>}}( || {{color|#800000|1}}( ||  || {{color|#800000|1}}( || ||  {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || ))))
|- 
| ⇒  || || {{color|#800000|1}}( || {{color|#008000|''S''<sub>1</sub>}}( || {{color|#800000|1}}( ||  || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || )))) || by 2
|- 
| ⇒  || || {{color|#800000|1}}( ||  || {{color|#800000|1}}( || {{color|#008000|''S''<sub>0</sub>}}( || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || )))) || by 4
|- 
| ⇒  || || {{color|#800000|1}}( ||  || {{color|#800000|1}}( ||  || {{color|#800000|0}}( || {{color|#008000|''S''<sub>0</sub>}}( || {{color|#800000|''nil''}} || )))) || by 1
|- 
| ⇒  || || {{color|#800000|1}}( ||  || {{color|#800000|1}}(  ||  || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || ))) &nbsp; &nbsp; &nbsp; || by 0
|}

In contrast, the term "{{color|#800000|1}}({{color|#800000|0}}({{color|#800000|''nil''}}))" leads to following non-accepting automaton run:

<!-- -tabular alignment chosen intentionally - please don't change without understanding the example or without proper reason- -->
{|
|- 
| ⇒  {{color|#008000|''S''<sub>0</sub>}}( || {{color|#800000|1}}( ||  || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || )))
|- 
| ⇒  || {{color|#800000|1}}( || {{color|#008000|''S''<sub>1</sub>}}( || {{color|#800000|0}}( ||  || {{color|#800000|''nil''}} || )))) || by 2
|- 
| ⇒   || {{color|#800000|1}}( ||  || {{color|#800000|0}}( || {{color|#008000|''S''<sub>2</sub>}}( || {{color|#800000|''nil''}} || )))) &nbsp; &nbsp; &nbsp; || by 3, no further rule applicable
|}

Since there are no other initial states than {{color|#008000|''S''<sub>0</sub>}} to start an automaton run with, the term "{{color|#800000|1}}({{color|#800000|0}}({{color|#800000|''nil''}}))" is not accepted by the tree automaton.

For comparison purposes, the table gives in column (A) and (D) a [[regular grammar#Strictly regular grammars|(right) regular (string) grammar]], and a [[regular tree grammar#Definition|regular tree grammar]], respectively, each accepting the same language as its automaton counterpart.