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.