2001/10/11 by Robert Harper, Frank Pfenning, Harper, Robert +1 · 1 citation
Computer Science · Mathematics · #Advanced Topics in Algebra #Algebraic structures and combinatorial models #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0110028
41 pages
arxiv created 2001/10/11 · openalex publication_date 2001/10/11 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 unit types or subtyping, and neither directly addresses the problem of conversion to canonical. 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.