next up previous
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 $\eta$-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:

So, if one chooses to use part $p_1$

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

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

Then, when completing the right branch with $p_3$

the same happens to the occurrences of $a$ in $p_3$ and in $p_1$:

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 $\eta$-reduction are not always principal inhabitants.


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