Pure Type Systems in Rewriting Logic

Mark-Oliver Stehr and Jose Meseguer

Keywords: Pure Type Systems, Logical Framework, Calculus of Constructions, Higher Order Logic, Typed Lambda Calculus, Rewriting Logic

Pure type systems (PTS) generalize the lambda-cube, which already contains important systems, like the simply typed and the (higher-order) polymorphic lambda calculi, a system LP close to the logical framework LF, and their combination, the calculus of constructions CC. PTS systems are considered to be of key importance, since their generality and simplicity makes them an ideal basis for representing higher-order logics either directly, via the propositions-as-types interpretation, or via their use as a logical framework. In [4] we show how the definition of PTS systems can be formalized in membership equational logic. It is noteworthy that the representational distance between the informal mathematical presentation of PTS systems with identification of alpha-equivalent terms and the membership equational logic specification of PTS systems is close to zero. In contrast to a higher-order representation in LF or Isabelle, this first-order inductive approach is closer to mathematical practice, and the adequacy of the representation does not require complex meta-logical justifications. It has also greater explanational power, since we explain higher-order calculi in terms of a first-order system with a very simple semantics.

We have also introduced uniform pure type systems (UPTS) a more concrete variant of PTS systems that do not abstract from the treatment of names, but use a uniform notion of names based on CINNI [1], a new first-order calculus of names and substitutions. UPTS systems solve the problem of closure under alpha-conversion, that has been discussed by Pollack (1993) and also encountered by Magnussen (1994), in a very elegant way. A membership equational logic specification of UPTS systems can be given that contains the equational substitution calculus and directly formalizes the informal presentation.

Furthermore, the reference [4] describes how meta-operational aspects of UPTS systems, like type checking and type inference, can be formalized in rewriting logic. For this purpose the inference system of a UPTS system is specified as a rewrite theory. The result of this formalization is an executable specification of UPTS systems that is correct w.r.t. the more abstract specification in a very obvious way.

Relevant References:

  1. Mark-Oliver Stehr: CINNI - A New Calculus of Explicit Substitutions and its Application to Pure Type Systems, Manuscript, CSL, SRI-International, Menlo Park, CA, USA, May 1999
  2. Manuel Clavel, Francisco Duran, Steven Eker, Jose Meseguer, Mark-Oliver Stehr: Maude as a Formal Meta-Tool. In the proceedings of FM'99, The World Congress On Formal Methods. Toulouse, France, September 20-24, 1999. Also appeared in the book OBJ/CafeOBJ/Maude at Formal Methods '99, Kokichi Futatsugi, Joseph Goguen and Jose Meseguer (Eds.), Theta (Bucharest), September 1999, ISBN 973-99097-1-X.
  3. Mark-Oliver Stehr: Type Theory in a Membership Equational Logic Framework (Talk given at Cornell)
  4. Mark-Oliver Stehr, Jose Meseguer: Pure Type Systems in Rewriting Logic , Proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999. Paper available here . Extended version submitted for publication.