Editing Tree automaton (section)

===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.