Next: Formula Tree Lab Applet Up: How to use the Previous: Construction of proof-trees from

## Principal Inhabitants

Another option allows searching for principal normal inhabitants. When pressing the "New Proof Tree" with the "Show Principality Cues" option, some edges and type-variables in the formula-tree appear colored.

This coloring might change during the construction of the proof-tree.

In order to construct principal normal inhabitants, after completion of the proof-tree all edges and type-variables in the formula-tree should be black. Then, all long terms in the corresponding set of normal terms are principal (terms obtained by -reduction may possibly be not principal). Conversely, if not all edges and type-variables in the formula-tree are black after completion of a proof-tree, then none of the corresponding terms is principal.

For changing colors the following rules apply:

• using a primitive part in the proof-tree turns all edges in this primitive part in the formula-tree black;
• overlapping occurrences of type-variables in the proof-tree receive the same color in the formula-tree (due to implementation, if all occurrences of a type-variable are have the same color, then they are all black).

So, if one chooses to use part

then the tail-variable in and the head-variable in receive the same color both in the proof-tree

as well as in the formula-tree and the edges in turn black.

Then, when completing the right branch with

the same happens to the occurrences of in and in :

Proceeding, one might construct the following proof-tree.

For this proof-tree all edges and type-variables in the formula-tree turned black:

This means that all long terms in the corresponding set of normal terms are principal inhabitants.

Note, that terms in this set obtained by -reduction are not always principal inhabitants.

Next: Formula Tree Lab Applet Up: How to use the Previous: Construction of proof-trees from
Sabine Broda