On equivalence and canonical forms in the LF type theory

ABSTRACT

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 article, 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.

REFERENCES

• 1: H. P. Barendregt, Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 2: Cervesato, I. 1996. A linear logical framework. Ph.D. dissertation. Dipartimento di Informatica, Universitá di Torino.
• 3: Iliano Cervesato , Frank Pfenning, A linear logical framework, Information and Computation, v.179 n.1, p.19-75, November 25, 2002 [doi>10.1006/inco.2001.2951]
• 4: Adriana B. Compagnoni , Healfdene Goguen, Anti-Symmetry of Higher-Order Subtyping, Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, p.420-438, September 20-25, 1999
• 5: Thierry Coquand, An algorithm for testing conversion in type theory, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 6: Dowek, G., Huet, G., and Werner, B. 1993. On the definition of the eta-long normal form in type systems of the cube. In Informal Proceedings of the Workshop on Types for Proofs and Programs, H. Geuvers, Ed. Nijmegen, The Netherlands.
• 7: C. M. Elliott, Higher-order unification with dependent function types, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.121-136, January 1989
• 8: Amy Felty , Dale Miller, Encoding a dependent-type &lgr;-calculus in a logic programming language, Proceedings of the tenth international conference on Automated deduction, p.221-235, July 1990, Kaiserslautern, Germany
• 9: Geuvers, H. 1992. The Church-Rosser property for βη-reduction in typed λ-calculi. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (Santa Cruz, Calif.), A. Scedrov, Ed. IEEE Computer Society Press, Los Alamitos, Calif., pp. 453--460.
• 10: Herman Geuvers , Erik Barendsen, Some logical and syntactical observations concerning the first-order dependent type system λP, Mathematical Structures in Computer Science, v.9 n.4, p.335-359, August 1999 [doi>10.1017/S0960129599002856]
• 11: Neil Ghani, Eta-Expansions in Dependent Type Theory - The Calculus of Constructions, Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, p.164-180, April 02-04, 1997
• 12: Goguen, H. 1994. A typed operational semantics for type theory. Ph.D. dissertation, Edinburgh Univ. Edinburgh, Scotland.
• 13: Healfdene Goguen, Soundness of the Logical Framework for Its Typed Operational Semantics, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, p.177-197, April 07-09, 1999
• 14: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 15: Harper, R. and Pfenning, F. 1999. On equivalence and canonical forms in the LF type theory. Tech. Rep. CMU-CS-99-159. Department of Computer Science, Carnegie Mellon Univ., Pittsburgh, Pa.
• 16: Jay, C. B. and Ghani, N. 1995. The virtues of η-expansion. J. Funct. Prog. 5, 2, 135--154.
• 17: Bengt Nordström , Kent Petersson , Jan M. Smith, Programming in Martin-Lo¨f's type theory: an introduction, Clarendon Press, New York, NY, 1990
• 18: Pfenning, F. 1992. Computation and deduction. Unpublished lecture notes, 277 pp. Revised May 1994, April 1996.
• 19: Pfenning, F. 1993. Refinement types for logical frameworks. In Informal Proceedings of the Workshop on Types for Proofs and Programs, H. Geuvers, Ed. Nijmegen, The Netherlands, 285--299.
• 20: Frank Pfenning, Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.221, June 16-19, 2001
• 21: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 22: Jeff Polakow , Frank Pfenning, Ordered linear logic and applications, 2001
• 23: Jeff Polakow , Frank Pfenning, Natural Deduction for Intuitionistic Non-communicative Linear Logic, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, p.295-309, April 07-09, 1999
• 24: Salvesen, A. 1990. The Church--Rosser theorem for LF with βη-reduction. Unpublished notes to a talk given at the First Workshop on Logical Frameworks in Antibes, France.
• 25: Christopher A. Stone , Robert Harper, Deciding type equivalence in a language with singleton kinds, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325724]
• 26: Streicher, T. 1991. Semantics of Type Theory. Birkhäuser.
• 27: Vanderwaart, J. C. and Crary, K. 2002. A simplified account of the metatheory of linear LF. In Proceedings of the 3rd International Workshop on Logical Frameworks and Meta-Languages (LFM'02), F. Pfenning, Ed. Vol. 70(2). Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, Copenhagen, Denmark. Extended version available as Technical Report CMU-CS-01-154.
• 28: Roberto Virga , Frank Pfenning, Higher-order rewriting with dependent types (lambda calculus), 1999

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory

Keywords:
Logical frameworks, type theory