IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

### Sequents with Restricted Declarations - continued from Sequents with Type Conclusions

We continue elaborating on sequents having types as conclusions. A declaration may be annotated as the second one is in the following sequent:

1. x :
2. y :   [not for witness]
3. x+1<y
{z:x<z & z<y }

The sequent above claims that there is some "witness" expression ???, not containing y free, such that

1. x :
2. y :
3. x+1<y
???  {z:x<z & z<y }

in which case the witness y-1  {z:x<z & z<y } would not suffice; however, the witness expression "x+1" would suffice since it does not use y.

Now, why do we care about restricting the use of declared variables from witnesses?
Recalling that k (i.e. {i:| 0  i < k }) is our standard finite set of size k  , consider the difference between the following two types of functions.

Thm* k:x:(k List){y:(k+1)| y greater-bounds x }
Thm* k:x:(k List){y:(k+1)| y greater-bounds x }

where Def y greater-bounds x == i:||x||. x[i]<y,
and ||x|| denotes the length of a list,
and x[i] denotes the member at position i  ||x|| of list x,
the head of a list being considered position 0.

The first is the type of functions which, applied to two arguments, a number k   and a list of numbers less than k, find a number no bigger than k, but bigger than every member of the list. It is of course quite trivial to find such a function-- just use k, as suggested in the proof.
The second, an Intersection Type, is the type of functions of one argument, a list of any type (k List) for any k  , that return such an upper bound, but do not take k itself as an argument. Such functions must examine the list to come up with a bound.

The proofs given for the above two theorems begin similarly, producing the following subgoals respectively:

1. k :
2. x : k List
{y:(k+1)| y greater-bounds x }

1. k :   [not for witness]
2. x : k List
{y:(k+1)| y greater-bounds x }

the difference being simply that the upper sequent can be satisfied by witness "k", but the second requires a witness not involving "k", and indeed the proof can be seen to proceed by induction on list structure. Incidentally, note that the inference to 1. x : A List    B(x) from   B(nil) and 1. u : A  2. v : A List  3. B(v)    B((u.v)) is justified by constructing the witness

Case of x; nil  p ; u.v, rec:r  q(uvr)

from witnesses "p" and "q(uvr)" for the two premise sequents.

Representing Propositions as Types affords Further Uses of Restricted Declarations.

(March 2001 - sfa )

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html