Next: A sample result based Up: Short description of the Previous: Proof-trees

## The relationship between proof-trees and normal inhabitants of simple types

The algorithms and below establish the following relationship between the valid proof-trees and the normal inhabitants of a simple type :

• for every (-)normal inhabitant of there exists exactly one long normal inhabitant of such that ;
• if is a normal inhabitant of , then is a valid proof-tree for ;
• if is a valid proof-tree for , then is a finite non-empty set of normal inhabitants of ;
• the two algorithms are complementary in the sense that for every normal inhabitant , there is .

Proof-tree Algorithm 3.5   Let be a long normal inhabitant of a type and let be the term obtained from by erasing abstractions in and replacing each variable with the name of the corresponding primitive part in . Then, is the graphical representation of after inserting a top level node (the root-node of ).

Terms Algorithm 3.6   Consider a type and let be the primitive parts in , where is the root-part and . Given a valid proof-tree for , the set is given by the following.
i.
First, represent as an application using for the variable name instead of . Then, for each variable-occurrence in this application, such that the primitive part has arity , insert a (possibly empty) abstraction sequence before each of its arguments. Here, the variable names in an abstraction sequence to be inserted before the th argument, , correspond to the primitive parts that descend directly from branch of .
ii.
Now, erase the variable at the top.
iii.
Finally, for term-scheme obtained in the previous step compute defined as follows.

• ;1
• ;
• ;
• .

Next: A sample result based Up: Short description of the Previous: Proof-trees
Sabine Broda