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

**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} }