[TYPES] Conversion elimination lemma for Pure Type Systems?
Ahn, Ki Yung
kyagrd at gmail.com
Mon May 17 17:57:59 EDT 2010
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.
More information about the Types-list