.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