next up previous
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 ${\tt PT}(\_)$ and ${\tt Terms}(\_)$ below establish the following relationship between the valid proof-trees and the normal inhabitants of a simple type $\varphi$:


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

Terms Algorithm 3.6   Consider a type $\varphi$ and let $p_0, \ldots,p_n$ be the primitive parts in ${\tt tree}(\varphi)$, where $p_0$ is the root-part and $n
\geq 0$. Given a valid proof-tree ${\tt PT}$ for $\varphi$, the set ${\tt Terms}({\tt PT})$ is given by the following.
i.
First, represent ${\tt PT}$ as an application using for $0 \leq i \leq n$ the variable name $x_i$ instead of $p_i$. Then, for each variable-occurrence $x_i$ in this application, such that the primitive part $p_i$ has arity $k_i \geq 0$, insert a (possibly empty) abstraction sequence before each of its $k_i$ arguments. Here, the variable names in an abstraction sequence $\lambda x_{j_1} \ldots x_{j_{l_j}}$ to be inserted before the $j$th argument, $1 \leq j \leq k_i$, correspond to the primitive parts $p_{j_1} \ldots p_{j_{l_j}}$ that descend directly from branch $j$ of $p_i$.
ii.
Now, erase the variable $x_0$ at the top.
iii.
Finally, for term-scheme $T$ obtained in the previous step compute ${\tt Terms}({\tt PT}) = T^{0\ldots 0}_{x_1\ldots x_n}$ defined as follows.

  • ${x_i}^{k_1\ldots 0 \ldots k_n}_{x_1\ldots x_i\ldots x_n}= \{
\overline{x_i} \}$;1
  • ${x_i}^{k_1\ldots k_i \ldots k_n}_{x_1\ldots x_i \ldots x_n}= \{
x_i,x'_i,x''_i,\ldots,x_i^{k_i-1} \},   {k_i \geq 1}$;
  • $(ST)^{k_1\ldots k_n}_{x_1\ldots x_n} = \{ S_i T_j   \vert   S_i
\in S^{k_1\ldots k_n}_{x_1\ldots x_n}, T_j \in T^{k_1\ldots
k_n}_{x_1\ldots x_n} \}$;
  • $(\lambda x_i.T)^{k_1\ldots k_n}_{x_1\ldots x_n} = \{ \lambda x_i^{k_i} .T_i   \vert   T_i \in
T^{k_1\ldots (k_i+1)\ldots k_n}_{x_1\ldots x_i \ldots x_n} \}$.


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