Decidability of definitional equality and conversion of terms into canonical
form play a central role in the meta-theory of a type-theoretic logical
framework. Most studies of definitional equality are based on a confluent,
strongly-normalizing notion of reduction. Coquand has considered a different
approach, directly proving the correctness of a practical equivalance algorithm
based on the shape of terms. Neither approach appears to scale well to richer
languages with, for example, unit types or subtyping, and neither provides a
notion of canonical form suitable for proving adequacy of encodings.
In this paper we present a new, type-directed equivalence algorithm for the LF
type theory that overcomes the weaknesses of previous approaches. The
algorithm is practical, scales to richer languages, and yields a new notion of
canonical form sufficient for adequate encodings of logical systems. The
algorithm is proved complete by a Kripke-style logical relations argument
similar to that suggested by Coquand. Crucially, both the algorithm itself and
the logical relations rely only on the shapes of types, ignoring dependencies
on terms.