next up previous
Next: Construction of proof-trees from Up: How to use the Previous: How to use the

Constructing proof-trees and normal inhabitants

After launching the Formula Tree Lab the following window appears.

Image init

Now, choose either to work with the given type, with another one from the list or with a new type to be introduced by hand.

Pressing the "Build Formula Tree" button will visualize the formula-tree of the type, i.e. its primitive parts (here $p_0,\ldots
,p_4$) and the hierarchy defined over them:

Image ft

In order to build a proof-tree for the type press the "New Proof Tree" button and a new window with the title "Proof Tree" will be created:

The construction of a proof-tree takes place in the main part of this window and parallel to that, in the bottom of the window, the corresponding scheme for long normal inhabitants is built. Indexed boxes will mark parts (subtrees) that still have to be completed in the proof-tree and also the corresponding missing subterms in the term-scheme.

In the beginning, the first and deterministic step for the construction of a proof-tree is already done: primitive part $p_0$ is the primitive part in the top. It has a branch ending in a variable $b$, so it is not complete and has to be completed with a complete subtree, represented here by a box with index $1$. In the bottom, one has a first approach to the corresponding term-scheme, which is of the form $\lambda x_1 x_2 x_3 . \vert 1\vert$, where $\vert 1\vert$ corresponds to the missing subtree. The variables in the abstraction sequence correspond to the available primitive parts which (after using $p_0$) are parts $p_1, p_2, p_3$.

Clicking on box $\vert 1\vert$ one can choose between primitive parts $p_1$ and $p_2$, which are the available primitive parts with head-variable $b$.

After choosing $p_1$ the construction of the proof-tree and also the term-scheme proceeds:

In fact, using $p_1$ of arity $2$ in the proof-tree means using variable $x_1$ with two arguments in the term-scheme. Since primitive part $p_4$ descends from the first branch of $p_1$ in the formula-tree, there will be an abstraction introducing a new variable $x_4$ in the first argument of $x_1$.

We choose to proceed with $p_2$ in the left branch.

Now, we have to complete two branches both ending with variable $a$.

If we click on box $2$ there is only one available primitive part with head-variable $a$: part $p_3$.

On the other hand, if we click on box $1$ also part $p_4$ is available, since this box is in the left branch of an occurrence of $p_1$ (remember that $p_4$ descends from this branch in the formula-tree).

After completion of the proof-tree, the part of the window with the term-scheme turns blue and can be clicked on in order to obtain a new window with the set of normal inhabitants that correspond to this proof-tree.

The proof-tree we just constructed corresponds to just one $\beta$-normal inhabitant of the type:

As another example, consider the tree

and the corresponding set of normal terms:

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