[TYPES] Conversion elimination lemma for Pure Type Systems?

[Dan Licata]

Hi Ki Yung,

If I've understood you correctly, then I don't think the theorem that
you want is true.  Consider the following example written in LF (which
is a PTS with Pi-kinds and Pi-types), written in Twelf notation:

signature:
o : type.
t : o -> type.
k : o.
r : {f : o -> o} t (f k).

example : t k = r ([ x ] x). 

Both the type of example (t k) and the term (r ([ x ] x)) are normal.
However, to show the typing, you have to use conversion
to show that t (([ x ] x) k) = t k :

                              x : o |- x : o
                             ------------------               .
r : {f : o -> o} t (f k)     ([ x ] x) : o -> o               .
------------------------------------------------              .
r ([ x ] x) : t (([ x ] x) k)                      t (([ x ] x) k) = t k
-------------------------------------------------------------------------
r ([ x ] x) : t k

A technique called "hereditary substitution" might be helpful to you, as
it builds the uses of conversion into the substitution operation, so 
you get better control over where in the derivation conversion happens. 
Some introductions to it are here:

http://www.cs.cmu.edu/~fp/papers/andrews08.pdf
http://www.cs.cmu.edu/~drl/pubs/hl07mechanizing/hl07mechanizing.pdf

-Dan



On May17, Ahn, Ki Yung wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> While I'm trying to prove a property of a calculus which is a variation
> of PTS, I needed a conversion elimination lemma for PTS which can be
> stated as follows:
> 
> "When a PTS typing judgment |- M : A is provable and the term M and its
> type A are both in normal forms, then there exists a derivation that
> does not use any conversion rule."
> 
> Of course, I am assuming the equality in the conversion rule of PTS to
> be beta-equality only, since other definitional equality (e.g. s1 = s2
> for some sort s1 and s2) can obviously require conversion rule for the
> judgments of terms and types with normal forms.
> 
> Seems like quite an obvious property, so I am wondering whether there
> has there been any proofs for such lemma in the literature?
> 
> Thanks in advance.
>