=arial size=-1 color=black> Below is a cache of http://www.metacarta.com/Collateral/Documents/English-US/Fixed-points-Scott-Topology-Bukatin.pdf. It's a snapshot of the page taken as our search engine crawled the Web.
The web site itself may have changed. You can check the current page or check for previous versions at the Internet Archive. Yahoo! is not affiliated with the authors of this page or responsible for its content.
Logic of Fixed Points and Scott Topology
Logic of Fixed Points and Scott Topology Michael A. Bukatin
1
,
2
1
Department of Computer Science, Brandeis University, Waltham, MA 02254, USA;
bukatin@cs.brandeis.edu; http://www.cs.brandeis.edu/bukatin/papers.html
2
MetaCarta, Inc., 126 Prospect St., Suite 5, Cambridge, MA 02139
Abstract. Domains with Scott topologies are frequently dened as sets of xed
points of retractions or, more generally, arbitrary Scott continuous transformations of
domains. For the case of retractions, the logical approach to this technique was devel-
oped by Hoofman under the name of continuous information systems. We present this
approach for general Scott continuous transformations, together with its underlying
intuition, a number of applications to closure operations and nitary retractions in the
algebraic case, and a spectrum of outstanding open problems.
1
Introduction
The elementary covariant logical approach to domains is known under the
name of information systems. This approach was introduced by Dana Scott
in 1982 [18] for algebraic bounded complete dcpos. We only consider bounded
complete dcpos in the present paper. Under this approach domain elements are
thought of as theories in a logical calculus, and continuous functions are thought
of as inference engines, deducing information about f (x) from information about
x. These inference engines are known under the name of approximable mappings.
This means that whenever one has a Scott continuous transformation, one can
think of it as a non-standard logic.
A more complicated and less elementary contravariant logical approach to
domains uses the ideas of Stone duality and is beyond the scope of the present
paper (see [1] and references therein).
In Section 3 we present the usual framework of information systems for
algebraic Scott domains. We reformulate the notion of consistency in a more
technically convenient way compared to the standard framework [18].
Section 4 is the key section of this paper. There we show how to take an ar-
bitrary Scott continuous transformation (of a powerset or, more generally, of an
algebraic bounded complete dcpo) and to use the corresponding approximable
mapping as a non-standard logic describing the domain of the xed points of this
transformation. This allows us to explain the intuition underlying the general- Supported in part by NSF Grant CCR-9216185 and Oce of Naval Research Grant ONR
N00014-93-1-1015 and in part by Applied Continuity in Computations Project.
1 ization of the information systems to the case of continuous Scott domains via
non-reexive logic made by R.Hoofman [9]. Hoofman essentially considered in-
ference engines corresponding to retractions and used the resulting non-reexive
logic to describe continuous domains.
Based on this intuition we further generalize the information systems to
domains of xed points of Scott continuous transformations of powersets. This
allows us to go beyond the realm of continuous domains, and if the conjecture
of Section 4.3.1 is correct, this approach would allow to describe all bounded
complete dcpos.
We also discuss the signicance of the algebraic case from the logical point
of view: algebraic Scott domains correspond to the standard logic, while some
of the more general classes of bounded complete domains result from either
Hoofmans non-reexive logic or Sazonovs non-nitary logic [16].
The subsequent sections, which represent our earlier results, may be also
viewed as applications of Section 4. Section 5 studies the notion of subdomain
and the domain of subdomains for the algebraic Scott domains. We show that
the closure operations play an exclusive role in the formation of subdomains in
the algebraic case, as opposed to retractions or projections, even when those are
nitary (i.e. their sets of xed points are algebraic). This exclusive role can be
explained by the intuition presented in Section 4. Namely, well see that it is the
closure operations, and not the nitary retractions in general, that correspond
to the standard logic under our approach.
Section 6 studies nitary retractions and provides the following novel simple
criterion for their nitarity. Consider the approximable mapping r correspond-
ing to a retraction |r|. The relation urv holds, if whenever u is true about x, v
is true about |r|(x). Here x is a domain element, and u and v are nite conjunc-
tions of elementary statements from the underlying logic. Then the retraction
|r| is nitary, if and only if whenever urw, there is such nite conjunction v,
that urv, vrv, vrw. Again, the results can be viewed as an illustration for the
intuition of Section 4. Basically, the reexive conjunctions v form the skele-
ton of the new standard logic describing the domain isomorphic to the Fix(|r|).
Some of the results of Sections 5 and 6 might be known in folklore, as Carl
Gunter suggested to me. However, it turned out to be impossible to trace any
written evidence of that.
2
Related Work and Notation
The canonical reference for the theory of domains equipped with Scott topology
is [2].
The origins of using inverse transitivity to describe non-algebraic continuous
domains should probably be traced to R-structures introduced by Smyth [20].
Hoofman gave this idea its truly logical form in [9].
Among the related papers of interest one should mention the results obtained
by Vickers [21], Edalat and Smyth [8], and more recently Jung, Kegelmann, and
Moshier [11].
2 One should also mention the thesis by Rothe [15] extensively studying re-
tractions in continuous domains.
We assume that all dcpos in this paper have the least element, .
Recall that if an algebraic dcpo is bounded complete, it is called an alge-
braic Scott domain or, simply, a Scott domain, and that if a continuous dcpo is
bounded complete, it is called a continuous Scott domain.
To be consistent with these denitions, if a dcpo is bounded complete, we
call it a complete Scott domain.
3
Algebraic Information Systems and Domains
This section outlines the approach of information systems in the case of algebraic
Scott domains as can be found, e.g. in [18, 12, 13].
The algebraic information systems and domains described in this reect the
standard notions of inference and theories in traditional formal theories.
3.1
Information Systems and Domains
The approach of information systems describes an approximation domain as a
set of theories in a logical calculus. There are two ways to follow this approach.
One could consider a given approximation domain, which obeys certain specic
axioms, and then try to build such a logical calculus, that its theories form an
isomorphic domain. This approach is very useful, when one needs to investigate
which class of domains is covered by a specic variant of information systems,
or when one starts with a given domain to begin with.
However, for didactic purposes, a dierent approach has proven much more
valuable. This approach was used in the rst key paper on information systems
by Dana Scott [18] and works as follows. We presume that there is some approx-
imation domain on the background, but we do not specify it precisely. Then,
having this hypothetical domain in mind, we reason about the desired properties
of our logical systems and impose appropriate axioms describing the behavior
of these systems. Then we dene domains as sets of theories and establish their
properties as theorems rather than postulating them as axioms.
3.1.1
UNKNOWN as a Truth Value
An information system is a logical calculus of elementary statements and their
nite conjuctions. These elementary statements and nite conjunctions should
be viewed as continuous predicates of a special kind on the elements of the
domain in question. These predicates map domains elements to a two-element
set of truth values, however these truth values are not ordinary true and false,
but true and unknown. This crucial feature is usually not emphasized enough,
but one needs to keep it in mind.
The reason for this distinction is that we view a domain element, x, as a
dynamic object, about which only some of the information is known at any given
3 time of the computational process, but which later can be supplemented with
more information, and thus replaced with y, x
y. The information, which
was unknown about x, can become true about y. This dynamic process is,
however, viewed as monotonic with respect to time once a piece of information
becomes true about an element, it remains this way further on.
It is possible to talk about false pieces of information about x these are
such pieces of information which are not true about any y, such that x
y, that
is, the pieces which cannot become true about x during its arbitrary monotonic
evolution. The false truth values will be treated via consistency mechanism,