[Prev][Next][Index][Thread]

Thesis on semantics for type theory

My thesis entiteled

Domains-with-totality semantics for intuitionistic type theory

is now available by anonymous ftp from

ftp.math.uio.no

in the directory

/pub/geirwa/

Both a mini-version (11 pages) and the full version is available (125
pages). The mini-version contains just the abstract, table-of-contents,
introduction, and the bibliography.

I recommend downloading the ps-version (thesis.ps.gz) since I have used
some non-standard fonts. However, a dvi-file is also available
(thesis.dvi.gz).
The file for the mini-version is thesis-mini.ps.gz.

Those who prefer a paper copy can send an email with their address to me
(geirwa@math.uio.no).

The abstract is included below:

**** ABSTRACT ****

The point of departure for this thesis is a hierarchy of (Scott-Ershov)
domains with totality defined and studied by Dag Normann in several papers.
There are two basic variants of this hierarchy studied by Normann: with or
without density of the total elements. This in turn, turns out to depend on
whether the empty type is included among the base types. In this thesis,
several other variants of this hierarchy are defined and analyzed:

\item The {\em effective} version of the hierarchy is developed using
Ershov's theory of enumerations.

\item Extensions with various type-constructors such as the identity type
and the $+$-type.

\item Extensions with universes.

>From the hierarchy of domains a hierarchy of quotient spaces can be derived
by taking quotients of the total elements under the equivalence relation of
hereditarily extensional equality. At this point a natural {\em lifting
problem} appears: Can continuous functions defined on the quotient spaces
be lifted to continuous functions on the domains from which the spaces have
been derived? This question appears in several variants depending on
whether one restricts attention to the effective part of the hierarchy and
whether the total elements are dense in the underlying domains:

\item If the total elements are dense in the domains and the full
(non-effective) hierarchy is considered we prove that liftings exist.

\item If the total elements are not dense and the full (non-effective)
hierarchy is considered we give a partial solution to the problem.

\item If the total elements are dense and the effective part of the
hierarchy is considered effective liftings exist, or more precisely,
effective operations are continuous. This turns out to be a generalization
of a classical theorem from computability theory by Kreisel, Lacombe, and
Shoenfield.

\item If the total elements are not dense and the effective part of the
hierarchy is considered we give a
counter-example which shows that the lifting property fails.

In addition to this, we show in detail how the hierarchy of domains can be
used to give an interpretation of Martin-L\"{o}f's intuitionistic type
theory (ITT). This gives an interpretation with the following properties:

\item The interpretation is within classical set theory.

\item $\Sigma$-types are interpreted as sets of pairs.

\item $\Pi$-types are interpreted as sets of continuous choice functions
(where the notion of continuity is derived from the Scott-topology on the
domains in the hierarchy).

\item The interpretation also gives a model of the logic in the type
theory. Furthermore, this model is (at least to some extent) faithful to
the fact that this logic is intuitionistic; e.g.\ the principle of the
excluded middle does not come out as true.

Using the solutions to the lifting problem, the relation of this model to
Beeson's realizability interpretation of ITT is investigated.

*********


Best regards,

Geir Waagboe
geirwa@math.uio.no
Department of Mathematics
University of Oslo
Norway