next up previous
Next: Bibliography Up: A tool for studying Previous: The relationship between proof-trees

A sample result based on the analysis of the formula-tree of a type

First note, by analysis of the algorithm $\tt Terms$ 2.6, that given a valid proof-tree $\tt PT$, one has $\vert{\tt Terms}({\tt PT})\vert > 1$ only if at least one primitive part has been used more than once in a branch of the proof-tree.


Now, consider the following definitions:

Definition 4.1   An occurrence of a subtype in a type is defined as positive or negative as follows.

Definition 4.2   A type is called negatively non-duplicated if every atom has at most one negative occurrence in it.


On the other hand, it is easy to see by inspection of the algorithm 2.3, that every negative (resp. positive) occurrence of a type-variable in a type appears as a head-variable (resp. tail-variable) of a primitive part in the formula-tree.

Thus it is easy to conclude the following result by [1].


Theorem 4.3   Every negatively non-duplicated type has at most one $\beta \eta$-normal inhabitant.

Proof $  $Consider an inhabited negatively non-duplicated type $\tau$ with formula-tree ${\tt tree}(\tau)$. Then, for every type-variable $a$ there is at most one primitive part in ${\tt tree}(\tau)$ with head-variable $a$. Thus, during the construction of a proof-tree there are no choices, which justifies the existence of a unique proof-tree. On the other hand, it also shows that there is no possibility of using a primitive part more that once in any branch, since this would lead to an infinite repetition. Thus, $\vert{\tt Terms}({\tt PT})\vert = 1$ follows from this remark and from the relationship between proof-trees and (long) normal inhabitants (cf. 2.3). $  \bullet$



next up previous
Next: Bibliography Up: A tool for studying Previous: The relationship between proof-trees
Sabine Broda