ON DOMAIN THEORY OVER CDG QUANTALES Pawel Waszkiewicz, Jagiellonian
University, Krakow, Poland

That partial orders and metric spaces can have a unified theory is an
idea due to William Lawvere who saw them both as examples of
categories enriched in a complete, symmetric monoidal closed
category. Lawvere's insight has inspired a research programme called
Quantitative Domain Theory (QDT) that analyzes how generalized metric
spaces can be used as domains of computation. For example, Michael
Smyth considered quasi-uniform and quasimetric spaces for this
purpose. Later Bob Flagg and Ralph Kopperman proposed a generalization
from quasimetric to Q-continuity spaces. Q-continuity spaces are sets
enriched in a quantale Q, which is in addition a completely
distributive complete lattice. In my presentation I assume that Q is a
CDG quantale, i.e. a completely distributive Girard quantale.

A lot is already known about Q-continuity spaces, about their
topology, completion, and about various universal constructions,
especially in the case of generalized metric spaces (i.e. when Q =
[0,+oo] or Q = [0,1]). What is lacking is a study of a mathematically
appealing subclass of Q-continuity spaces consisting of so called
continuous Q-domains. (What makes the class appealing is -- in my
opinion -- the fact that for Q=2 it is precisely the class of
continuous dcpos.)

Therefore, in my talk I will speak about continuous Q-domains that
generalize continuous dcpos. I will show a general method of
constructing continuous Q-domains by the rounded ideal completion of a
Q-abstract basis. One of the nicest, and simplest, applications of
rounded ideal completion in classical domain theory is the
construction of powerdomains as completions of Egli-Milner
preorders. I will use the same instructive example and show how to
define Hoare, Smyth and Plotkin powerdomains over a continuous
Q-domain. My results generalize corresponding theorems about
powerdomains in [BBR98].

My talk aims at a presentation of QDT that is as close to original
Scott's domain theory as possible (this is also a goal of [FSQ96]). I
would like to promote an interpretation of QDT as ``domain theory in
the logic of CDG quantales'' and NOT as theory of generalized metric
spaces. Let me explain it briefly below (next paragraph can serve as a
short abstract of my talk):

My talk is about a generalization of Scott's domain theory in such a
way that its definitions and theorems become meaningful in quasimetric
spaces. The generalization is achieved by a change of logic: the
fundamental concepts of original domain theory (order, way-below
relation, Scott-open sets, continuous maps, etc.) are interpreted as
predicates that are valued in an arbitrary completely distributive
Girard quantale (a CDG quantale). Girard quantales are known to
provide a sound and complete semantics for commutative linear logic
[Yet90], and complete distributivity adds a notion of approximation to
the setup. Consequently, I will speak about domain theory based on the
commutative linear logic with some additional reasoning principles
following from approximation between truth values.

REFERENCES:

[BBR98] Bonsangue, M.M., van Breugel, F. and Rutten, J.J.M.M. (1998) Generalized Metric Spaces: Completion, Topology, and Powerdomains via the Yoneda Embedding, Theoretical Computer Science 193 (1-2), pp. 1--51.

[FSW96] Flagg, R.C., Sunderhauf, P. and Wagner, K.R. (1996) A Logical Approach to Quantitative Domain Theory, Topology Atlas Preprint no. 23, available on-line at: http://at.yorku.ca/e/a/p/p/23.htm

[Yet90] Yetter, D.N. (1990) Quantales and (Noncommutative) Linear Logic, The Journal of Symbolic Logic 55(1), pp. 41--64.