COMPUTER SCIENCE TECHNICAL REPORT ABSTRACTS

Source: http://reports-archive.adm.cs.cmu.edu/anon/1999/abstracts/99-159.html Parent: https://www.cs.cmu.edu/~fox/publications.html


	CMU-CS-99-159 Computer Science Department School of Computer Science, Carnegie Mellon University --- CMU-CS-99-159 On Equivalence and Canonical Forms in the LF Type Theory Robert Harper, Frank Pfenning September 1999 CMU-CS-99-159.ps CMU-CS-99-159.ps.gz CMU-CS-99-159.pdf Keywords: Logical framework, type theory 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 equivalence 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 form. 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 more expressive 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. 43 pages
--- Return to: SCS Technical Report Collection School of Computer Science homepage This page maintained by reports@cs.cmu.edu

CMU-CS-99-159 Computer Science Department School of Computer Science, Carnegie Mellon University --- CMU-CS-99-159 On Equivalence and Canonical Forms in the LF Type Theory Robert Harper, Frank Pfenning September 1999 CMU-CS-99-159.ps CMU-CS-99-159.ps.gz CMU-CS-99-159.pdf Keywords: Logical framework, type theory 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 equivalence 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 form. 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 more expressive 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. 43 pages

--- Return to: SCS Technical Report Collection School of Computer Science homepage This page maintained by reports@cs.cmu.edu