Invited Paper: Quantitative and Qualitative Semantics (at LICS 1986)

Authors: Jean-Yves Girard

Abstract

The new semantical domains for lambda calculi and similar functional languages are described: quantitative and qualitative domains. Both are based on category-theoretic ideas in contrast to the usual topological ones. Topological convergence and continuity are reformulated by means of category-theoretic direct limits; other categorical concepts such as pull-backs answer for the "stability" of algorithms. The crucial step of defining the function space is handled by means of normal form theorems reminiscent of the Cantor normal form theorem for ordinals.
These new semantics are simpler and more managable than the usual ones. Of course they provide models for familiar functional languages such as finitely typed or untyped lambda calculus, but they also yield more satisfactory models of typed systems -- notably the author's System F (also called "second-order lambda calculus") -- whose semantical treatments till now were based on untyped models. The idea is that a type is an arbitrary domain of the kind considered, say qualitative. Then a (universal) dependent type is just a functor sending types into types. Now if the functor has suitable preservation properties it can be shown that the dependent type is determined by its behavior on those types which are finite domains. This enables us to interpret second-order quantification on types in a very compact way: typically the "universial identity" is interpreted by a structure with only one point! But this structure encodes the identity maps of any domain without limitation on size or the like. One of the by-products of the interpretation of F is the fact that there is an "intrinsic" model of lambda calculus, i.e., a minimal interpretation from which we can recover all possible interpretations.
Perhaps the principal significance of these new semantics is that, since we can easily toy with them, they suggest important modifications of the syntax of lambda calculi. But that is another story.

BibTeX

  @InProceedings{Girard-QuantitativeandQual,
    author = 	 {Jean-Yves Girard},
    title = 	 {Quantitative and Qualitative Semantics},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {258},
    location =   {Cambridge, MA, USA}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }