Next: Proof-trees Up: Short description of the Previous: Short description of the

## Formula-trees

The formula-tree of a simple type is an alternative tree-like representation. For this is split into primitive parts, and the formula-tree defines some kind of hierarchy over these primitive parts.

Definition 3.1   Primitive parts are items of either one of the following forms (P1), (P2) or (P3), where denote type-variables:

(P1): (P2): (P3):

Here, are called the tail-variables of the respective primitive part, while and are head-variables. The arity of a primitive part is the number of its tail-variables.

Definition 3.2   A formula-tree is a tree-like structure with primitive parts as nodes, but such that subtrees descend from the branches (tail-variables) of primitive parts rather than from the whole primitive parts as nodes. Then, such a structure is called a formula-tree iff
• the root of the formula-tree is the only primitive part of form (P1);
• every node of form (P2) or (P3) in the formula-tree descends from a tail-variable in another primitive part.

The following algorithm computes the formula-tree of a type . We use dashed lines for the edges of the formula-tree in order to distinguish them from the edges in the primitive parts (nodes) of the tree.

Formula-tree Algorithm 3.3   Consider a type , where is an atom and . Then, its formula-tree is given by the following.
• If , i.e. , then .

• If , then

where

and for and we recursively define

Next: Proof-trees Up: Short description of the Previous: Short description of the
Sabine Broda