.Open Domains
. Motivation
Domains have been used to explain why recursive definitions can be
approximated by iterative computations.
Another way of looking at domain theory is to say that it is a way of
modelling the fact that certain computations don't have a defined result
and using the model to prove that certain computations will ultimately
provide as close to a complete definition as we could demand.
A map from a set to itself can model recursive definitions - for example
consider the following definition
trains::=engine wagon |trains wagon.
It can can be described in a different way by a function describing
a single iteration:
add_a_wagon::=map [x](engine wagon | x wagon).
A recursive definition makes sense if (1) the map gives a `better`
approximation - and so (2) there is unique (in some sense) `best` thing
that doesn't change when we apply the map. The word
like `better` indicates the need for a partial order and the word `best`
indicates we need a theory of minima/maxima.
Domains include an undefined object which are less defined than any other
object. Scott promotes the use domains that also include the over defined
object - one that can not exist because its specification is contradictory.
. Domain Theory
The following is abstracted from Dana Scott's lecture
.See Scott76
but owes much to Manes and Arbib's book
.See Manes&Arbib86.
DOMAIN::=following
.Net
S::=Set,
Set::Sets,
undefined::S,
\bot::=undefined,
relation::@(S,S),
relation=`(1st) is less or equally defined as (2nd)`.
|-(D1): $POSET(set, relation,...) and $MINMAX.
POSET::=http://www/dick/maths/math_21_Order.html#POSET.
MINMAX::=http://www/dick/maths/math_21_Order.html#MINMAX.
()|-(D2): \bot=the minima (S).
()|-(complete): For all s:Seq(S) & ascending, some lub(x).
Typographically the relation (<=) is shown as an square cornered
subset_or_equal symbol.
<= ::=\sqsubseteq,
\sqsubseteq::=relation.
(MAXMIN)|-(D3): For s:ascending, one lub(s).
For s:ascending, lim(s) ::=the lub(s).
(def)|-(D4): for f:monotonic, s:ascending, f(s) in ascending.
continuous::@monotonic={f || for all s:ascending( lim(f(s))=f(lim(s)) ) }.
increasing::={f:S->S || for all x( x <= f(x))},
Kleene_sequence::=map[f:S->S]([i]f^i(\bot)),
()|-(D5): For \psi:S->S, Kleene_sequence(\psi)= (\bot, f(\bot),
f(f(\bot)), ...),
.See Manes&Arbib86
()|-(D6): for f:increasing, Kleene_sequence(f) in ascending,
()|-(D7): for f:increasing, one lub Kleene_sequence(f).
For f:increasing, Kleene_limit(f) ::=the lub Kleene_sequence(f)
A solution to a recursive set of definitions is the often defined as the
least object in the domain that is not changed by applying the definition
to it - the least fixed_point(_).
Kleene fixed point theorem.
.Source Kleene 52
()|-(KleeneFP): For all f:continuous, Kleene_limit(f) =the least
fixedpoint(f).
Scott argues that computable functions are exactly those that are
continuous in this sense
.See Scott70
Manes and Arbib critique this claim chapter 13, section 1, of
.See Manes&Arbib8686
They claim that there are other ways to establish
the meanings of the functions that can be computed without insisting on
domains and continuity and in particular show that Kleene's theorem has an
equivalent form in category theory and in metric spaces. They give
applications of these theories to programming language semantics.
A well founded domain is essentially one where all the objects
are at least hypothetically constructed by a finite series of steps
from the simplest objects:
wellfounded::@= no (strict_descending_chain ~ finite).
.See http://www/dick/maths/math_21_Order.html#strict_descending
.Close.Net
domain::=$ $DOMAIN.
.Open Examples
.Boolean Domains
BooleanDomain::=$ $DOMAIN with following
.Box
Set=>{true,false,undefined},
relation=>rel[x,y](x=undefined or x=y)
.Close.Box
BoolSeqDomain::=$ $DOMAIN with following
.Box
Set=>Nat->$BooleanDomain,
undefined=>(Nat+>$BooleanDomain.$undefined),
relation=>rel[x,y](for all n:Nat( x[n] $BooleanDomain.$relation y[n])
.Close.Box
. Sets
For S:Sets, (@S,==>) is a complete_poset with {}=the lub(@S) and so (@S,{},
==>) is a domain.
. Partial Functions
Manes and Arbib show that partial functions form a domain:
for all X,Y:Sets, DOMAIN (X<>->Y, {},relation=>(rel[f,g]( pre(f)==>pre(g)
and f o pre(f)= g o pre(f) ) ) ).
. Mutivalued Functions
Manes & Arbib also have defined multivalued functions (X->@Y), which also
form a complete poset and so a domain.
. Relations
Similarly for a set of all relations of one type:
For all X,Y:Sets, DOMAIN(@(X,Y), {}, ==>)
So in consequence an equation/iteration like
X'=R;X|Id
has a unique relation `do(R)` as its solution.
.Close Examples
. Flat Domains
For ANY set we can create a domain by adding a new element.
For S0:Sets,if not \bot in S0 then S0.\flat::=S0|{\bot}
FlatDomain::=following
.Net
S0::Sets,
\bot::Things~S0,
Set::=S0.\flat,
relation::@(Set,Set)=rel[x,y](x=\bot or x=y in S0),
()|-(FD1): DOMAIN(Set, \bot, relation).
For f:S0<>->S0, f.\flat::Set->Set=map[x](if x in pre(f) then f(x) else
undefined),
since undefined isn't in S0, undefined is not in pre(f).
()|-(FD2): continuous=>img(\flat)
Manes and Arbib
.See Manes&Arbib86
point out that f can be computable, but f.\flat may not be. They symbolize
f.\flat by f^\flat.
.Close.Net
. Product Domains
PRODUCT::=following
.Net
n::Nat,
D::array 1..n of Sets,
\bot::array 1..n of Things,
R::array 1..n of Sets,
()|-(PD0):For all i:1..n, DOMAIN(Set=>D[i], \bot[i], R[i]).
Set::= ><(D),
relation::=[x,y](for all i:1..n (x[i]<=[i]y[i]) ),
undefined::=\bot,
()|-(PD1): DOMAIN (Set, relation, undefined).
.Close.Net
For A:array 1..n of $ $DOMAIN, ><(D) ::=$ $PRODUCT(n=>n, D=>A;set,
\bot=>A;undefined, R=>A;relation).$(DOMAIN).
. Derived Domains
For every domain other domains can be constructed - Dana Scott has done
much beautiful prefabrication to ensure that once domains are defined for a
collection of elementary objects then there will be domains for arrays of
objects (see product above), maps between objects, series of objects (see
below), etc.
SEQDOMAIN::=following
.Net
For any domain S, the set of sequences of elements in S is also a domain -
and so in this domain every sequence has a limit.
()|-(SD0): DOMAIN.
(<=) ::@(Seq(S),Seq(S))= rel[x,y](for all n (x[n] <= y[n]).
undefined::Seq(S)=(Nat+>undefined.S).
()|-(SD1): For s:Seq(S), if <=(s) then some lub(s).
()|-(SD2): DOMAIN(Seq(S),<=,undefined).
For s:Seq(S), s[..n]::=map[i](if i<=n then s(i) else undefined).
()|-(SD3): For all s, n, s[..n] <= s[..n+1] <= s.
()|-(SD4): For all s, one lub([n]s[..n]).
for all s, lim(s) ::=the lub(map[n]s[..n]).
.Close.Net
. Self similar domains.
Dana Scott's break through was to demonstrate that there must exist, for
any domain of elements, a domain that includes the elements, the continuous
mappings between them, and the continuous maps between maps, etc. In other
words, there is a mathematical system which gives meaning to the \lambda
calculus, without making any appeal to computation
.See Scott76
. Power Domains
Plotkin has extended the domain model into a domain of sets of elements
(from S to @S, approximately)
.See Plotkin76
.Bibliography
(Kleene52): S.C. Kleene, Introduction to Metamathematics, Van Nostrand,
1952.
(Manes&Arbib86): Manes & Michael Arbib,Algebraic Approaches to Program
Semantics, Springer Verlag Monograph 1986
.See [Manes & Arbib 86]
(Plotkin76): Gordon Plotkin, A power domain construction, SIAM Journal of
Computing, V5 1976, pp 452-487
(Scott70): Dana. S. Scott, "Lattice theory, data types, and semantics," in
R. Rustin (ed.), Formal Semantics of Programming Languages, Prentice Hall,
1970
(Scott76): Dana S Scott, Dana Scott's 1976 Turing lecture in
.See [ACM 86]
.Close Domains