Empty types in polymorphic lambda calculus

ABSTRACT

The model theory of simply typed and polymorphic (second-order) lambda calculus changes when types are allowed to be empty. For example, the “polymorphic Boolean” type really has exactly two elements in a polymorphic model only if the “absurd” type ∀t.t is empty. The standard &bgr;-&egr; axioms and equational inference rules which are complete when all types are nonempty are not complete for models with empty types. Without a little care about variable elimination, the standard rules are not even sound for empty types. We extend the standard system to obtain a complete proof system for models with empty types. The completeness proof is complicated by the fact that equational “term models” are not so easily obtained: in contrast to the nonempty case, not every theory with empty types is the theory of a single model.

REFERENCES

• 1: H. P. Barendregt. The Lambda Calculus: Rs Syntaz and Semantics. Volume 103 of Studies in Logic, North-Holland, 1981. Revised Edition, 1984.
• 2: V. Breazu-Tannen , T. Coquand, Extensional models for polymorphism, II and Colloquium on Functional and Logic Programming and Specifications (CFLP) on TAPSOFT '87: Advanced Seminar on Foundations of Innovative Software Development, p.291-307, March 1987, Pisa, Italy
• 3: V. Breazu-Tannen and A. R. Meyer. Computable values can be classical. 1986. These Proceedings.
• 4: Kim B. Bruce , Albert R. Meyer, The semantics of second order polymorphic lambda calculus., Proc. of the international symposium on Semantics of data types, p.131-156, July 1984, Sophia-Antipolis, France
• 5: L. Cardelli. A polymorphic calculus with type:type. Technical Report, DEC System Research Center, 1985.
• 6: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 7: T. Coquand. Communication in the TYPES electronic forum (types~xx.lcs.mit.edu). 1986. April 14th.
• 8: Thierry Coquand , Gérard P. Huet, Constructions: A Higher Order Proof System for Mechanizing Mathematics, Invited Lectures from the European Conference on Computer Algebra-Volume I, p.151-184, April 01-03, 1985
• 9: Steven Fortune , Daniel Leivant , Michael O'Donnell, The Expressiveness of Simple and Second-Order Type Structures, Journal of the ACM (JACM), v.30 n.1, p.151-185, Jan. 1983 [doi>10.1145/322358.322370]
• 10: H. Friedman. Equality between functionals. In R. Parikh, editor, Logic Colloqium, '73, pages 22-37, Springer-Verlag, 1975.
• 11: J. Girard. Interpretation fonctionelle et ~limination des coupures dans l'arithm~tique d'ordre supdrieure. PhD thesis, Universit~ Paris VII, 1972.
• 12: J. A. Goguen , J. Meseguer, Completeness of many-sorted equational logic, ACM SIGPLAN Notices, v.17 n.1, p.9-17, January 1982 [doi>10.1145/947886.947887]
• 13: P. Martin-LSf. An intuitionisti~ theory of types" predicative part. In F. Rose and J. Sheperdson, editors, Logic Colloquium III, pages 73-118, North-Holland, Amsterdam, July 1973.
• 14: Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
• 15: A. R. Meyer. What is a model of the lambda calculus? Information and Control, 52(1)'87-122, Jan. 1982.
• 16: Albert R. Meyer , Mark B. Reinhold, "Type" is not a type, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.287-295, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512671]
• 17: J. C. Mitchell. Lambda Calculus Models of Typed Programming Languages. PhD thesis, Massachusetts Institute of Technology, Cambridge, Massachusetts, Aug. 1984.
• 18: E. Moggi. Communication in the TYPES electronic forum ([e-mail]). 1986. February 10th.
• 19: C. Mohring. Algorithm development in the theory of constructions. In Syrup. Logic in Computer Science, pages 84-91, IEEE, 1986.
• 20: J C Reynolds, Three approaches to type structure, Proc. of the international joint conference on theory and practice of software development (TAPSOFT) Berlin, March 25-29, 1985 on Mathematical foundations of software development, Vol. 1: Colloquium on trees in algebra and programming (CAAP'85), p.97-138, April 1985, Berlin, Germany
• 21: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 22: D. Scott. Data types as lattices. SIAM J. Computing, 5:522-587, 1976.
• 23: R. Statman. Completeness, invariance and lambda-definability. J. Symbohe Logic, 47:17-26, 1982.

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

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory; Model theory

General Terms:
Algorithms, Languages, Theory