On Equivalence and Canonical Formsin the LF Type TheoryROBERT HARPER and FRANK PFENNINGCarnegie Mellon UniversityDecidability of de finiti onal equality and conversion of terms into canonical form play a centralrole in the meta-theory of a type-theoretic logical framework. Most studies of definitional equalityare based on a confluent, strongly-normalizing notion of reduction. Coquand has considered adifferent approach, directly proving the correctness of a practical equivalance algorithm based onthe 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 provingadequacy of e ncodings.In this paper we present a new, type-directed equivalence algorithm for the LF type theorythat overcomes the weaknesses of previous approaches. The algorithm is practical, scales to richerlanguages, and yields a new notion of canonical form sufficient for adequate encodings of logicalsystems. The algorithm is proved complete by a Kripke-style logical relations argument similarto that suggested by Coquand. Crucially, both the algorithm itself and the logical relations relyonly on t he shapes of types, ignoring dependencies on terms.Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Language]:Mathematical Logic—Lambda calculus and related systemsGeneral Terms: Languages, TheoryAdditional Key Words and Phrases: Logical frameworks, type theory1. INTRODUCTIONAt present the mechanization of constructive reasoning relies almost entirely ontype theories of various forms. The principal reason is that the computationalmeaning of constructive proofs is an integral part of the type theory itself. The maincomputational mechanism in such type theories is reduction, which has thereforebeen studied extensively.For logical frameworks the case for type theoretic meta-languages is also com-pelling, since they allow us to internalize deductions as objects. The validity of adeduction is then verified by type-checking in the meta-language. To ensure thatproof checking remains decidable under this representation, the type checking prob-Author’s addresses:Department of Computer Science, Carnegie Mellon University, Pittsbu rgh, PA 15213, U.S.A.,[email protected], [email protected] work has been supported by the National Science Foundation under grants CCR-9619584and CCR-9988281.Permission to make digital/hard copy of all or part of this material without fee for personalor classroom use provided that the copies are not made or distributed for profit or commercialadvantage, the ACM copyright/server notice, the title of the publication, and its date appear, andnotice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish,to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.c 20?? ACM 1529-3785/20??/0700-0001 $5.00ACM Transactions on Computational Logic, Vol. ?, No. ?, ?? 20??, Pages 1–41.2 · R. Harper and F. Pfenninglem for the meta-language must also be decidable. To support deductive s ystemsof practical interest, the type theory must support dependent types, that is, typesthat depend on objects.The correctness of the representation of a logic in type theory is given by an ade-quacy theorem that correlates the syntax and deductions of the logic with canonicalforms of suitable type. To establish a precise correspondence, canonical forms aretaken to be β-normal, η-long forms. In particular, it is important that canonicalforms enjoy the property that constants and variables of higher type are “fully ap-plied” — that is, each occurrence is applied to enough arguments to reach a basetype.Thus we see that the methodology of logical frameworks relies on two fundamen-tal meta-theoretic results: the decidability of type checking, and the existence ofcanonical forms. For many type theories the decidability of type checking is eas-ily seen to reduce to the decidability of definitional equality of types and terms.Therefore we focus attention on the decision problem for definitional equality andon the conversion of terms to canonical form.Traditionally, both problems have been treated by considering normal forms forβ, and possibly η, reduction. If we take definitional equality to be conversion,then its decidability follows from confluence and strong normalization for the cor-responding notion of reduction. In the case of β-reduction this approach to decidingdefinitional equality works well, but for βη-reduction the situation is much m orecomplex. In particular, βη-reduction is confluent only for well-typed terms, andsubject reduction depends on strengthening, which is difficult to prove directly.These technical problems with βη-reduction have been addressed with differentmethods by Salvesen [1990], Geuvers [1992], and Goguen [1999], but neverthelessseveral problems remain. First, canonical forms are not βη-normal forms and soconversion to canonical form must be handled separately. The work by Dowek etal. [1993] shows how to do this for the Calculus of Constructions, but it is not clearthat their approach would scale to theories such as those including linear types,unit types, or subtyping. Second, the algorithms implicit in the reduction-basedaccounts are not practical; if two terms are not definitionally equal, we can hopeto discover this without reducing both to normal form.These problems were side-stepped in the original paper on the LF logical frame-work [Harper et al. 1993] by restricting attention to β-conversion for definitionalequality. This is sufficient if we also restrict attention to η-long forms [Felty andMiller 1990; Cervesato 1996]. This restriction is somewhat unsatisfactory, especiallyin linear variants of LF [Cervesato and Pfenning 2002].More recently, η-expansion has been studied in its own right, using modificationof standard techniques from rewriting theory to overcome the lack of strong nor-malization when expansion is not restricted [Jay and Ghani 1995; Ghani 1997].In the dependently typed case, even the definition of long normal form is notobvious [Dowek et al. 1993] and the technical development is fraught with diffi-culties. We have not been able to reconstruct the proofs given by Ghani [1997].The approach taken by Virga [1999] relies on a complex intermediate system withannotated terms.To address the problems of practicality, Coquand suggested abandoning