next up previous
Next: Proof-trees Up: Short description of the Previous: Short description of the

Formula-trees

The formula-tree ${\tt tree}(\varphi)$ of a simple type $\varphi$ is an alternative tree-like representation. For this $\varphi$ 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 $A,B, B_1,\ldots,B_n,C$ denote type-variables:


(P1): $\spreaddiagramrows{-1pc}
\spreaddiagramcolumns{-1.5pc}
\diagram
& \dline \\
& A \\
\enddiagram         $ (P2): $\spreaddiagramrows{-1pc}
\spreaddiagramcolumns{-1.5pc}
\diagram
& B\dlline \dr...
...\\
B_1 & \ldots & B_n \\
\enddiagram      (n \geq 1)         $ (P3): $\spreaddiagramrows{-1pc}
\spreaddiagramcolumns{-1.5pc}
\diagram
& C \dline \\
&    \\
\enddiagram$

Here, $A, B_1,\ldots,B_n$ are called the tail-variables of the respective primitive part, while $B$ and $C$ 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 following algorithm computes the formula-tree ${\tt tree}(\varphi)$ of a type $\varphi$. 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 $\varphi = \alpha_1 \rightarrow
\ldots \rightarrow \alpha_n \rightarrow A$, where $A$ is an atom and $n
\geq 0$. Then, its formula-tree ${\tt tree}(\varphi)$ is given by the following.


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