[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_24_Domains
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Dec 13 14:02:45 PST 2010

Contents

    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

    1. trains::=engine wagon |trains wagon.

      It can can be described in a different way by a function describing a single iteration:

    2. 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 [ Scott76 ] but owes much to Manes and Arbib's book [ Manes&Arbib86] .

    3. DOMAIN::=following
      Net
      1. S::=Set,
      2. Set::Sets,
      3. undefined::S,
      4. ⊥::=undefined,
      5. relation::@(S,S), relation=(1st) is less or equally defined as (2nd).


      6. |- (D1): POSET(set, relation,...) and MINMAX.
      7. POSET::= See http://cse.csusb.edu/dick/maths/math_21_Order.html#POSET.
      8. MINMAX::= See http://cse.csusb.edu/dick/maths/math_21_Order.html#MINMAX.
      9. (above)|- (D2): ⊥=the minima (S).
      10. (above)|- (complete): For all s:Seq(S) & ascending, some lub(x).

        Typographically the relation (<=) is shown as an square cornered subset_or_equal symbol.

      11. <=::=\sqsubseteq,
      12. \sqsubseteq::=relation.


      13. (MAXMIN)|- (D3): For s:ascending, one lub(s).
      14. For s:ascending, lim(s)::=the lub(s).


      15. (def)|- (D4): for f:monotonic, s:ascending, f(s) in ascending.

      16. continuous::@monotonic={f || for all s:ascending( lim(f(s))=f(lim(s)) ) }.

      17. increasing::={f:S->S || for all x( x <= f(x))},

      18. Kleene_sequence::=map[f:S->S]([i]f^i(⊥)),
      19. (above)|- (D5): For \psi:S->S, Kleene_sequence(\psi)= (⊥, f(⊥), f(f(⊥)), ...), [ Manes&Arbib86 ]


      20. (above)|- (D6): for f:increasing, Kleene_sequence(f) in ascending,
      21. (above)|- (D7): for f:increasing, one lub Kleene_sequence(f).
      22. 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

      23. (above)|- (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 [ Scott70 ] Manes and Arbib critique this claim chapter 13, section 1, of [ 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:

      24. wellfounded::@= no (strict_descending_chain ~ finite). [ strict_descending in math_21_Order ]


      (End of Net)

    4. domain::=$ DOMAIN.

      Examples

        .Boolean Domains
      1. BooleanDomain::=$ DOMAIN with following
        1. Set=>{true,false,undefined},
        2. relation=>rel[x,y](x=undefined or x=y)

      2. BoolSeqDomain::=$ DOMAIN with following
        1. Set=>Nat->BooleanDomain,
        2. undefined=>(Nat+>BooleanDomain.undefined),
        3. relation=>rel[x,y](for all n:Nat( x[n] BooleanDomain.relation y[n])

        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:
      3. For all X,Y:Sets, DOMAIN(@(X,Y), {}, ==>)

        So in consequence an equation/iteration like

      4. X'=R;X|Id

        has a unique relation do(R) as its solution.

      . . . . . . . . . ( end of section Examples) <<Contents | End>>

      Flat Domains

      For ANY set we can create a domain by adding a new element.
    5. For S0:Sets, if not ⊥ in S0 then S0.\flat::=S0|{⊥}

    6. FlatDomain::=following
      Net
      1. S0::Sets,
      2. ⊥::Things~S0,
      3. Set::=S0.\flat,
      4. relation::@(Set,Set)=rel[x,y](x=⊥ or x=y in S0),
      5. (above)|- (FD1): DOMAIN(Set, ⊥, relation).

      6. 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).


      7. (above)|- (FD2): continuous=>img(\flat)

        Manes and Arbib [ Manes&Arbib86 ] point out that f can be computable, but f.\flat may not be. They symbolize f.\flat by f^\flat.


      (End of Net)

      Product Domains

    7. PRODUCT::=following
      Net
      1. n::Nat,
      2. D::array 1..n of Sets,
      3. ⊥::array 1..n of Things,
      4. R::array 1..n of Sets,
      5. (above)|- (PD0): For all i:1..n, DOMAIN(Set=>D[i], ⊥[i], R[i]).

      6. Set::= ><(D),
      7. relation::=[x,y](for all i:1..n (x[i]<=[i]y[i]) ),
      8. undefined::=⊥,
      9. (above)|- (PD1): DOMAIN (Set, relation, undefined).

      (End of Net)

    8. For A:array 1..n of $ DOMAIN, ><(D)::=$ PRODUCT(n=>n, D=>A;set, ⊥=>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.

    9. 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.
      1. (above)|- (SD0): DOMAIN. (<=) ::@(Seq(S),Seq(S))= rel[x,y](for all n (x[n] <= y[n]).
      2. undefined::Seq(S)=(Nat+>undefined.S).
      3. (above)|- (SD1): For s:Seq(S), if <=(s) then some lub(s).


      4. (above)|- (SD2): DOMAIN(Seq(S),<=,undefined).

      5. For s:Seq(S), s[..n]::=map[i](if i<=n then s(i) else undefined).


      6. (above)|- (SD3): For all s, n, s[..n] <= s[..n+1] <= s.
      7. (above)|- (SD4): For all s, one lub([n]s[..n]).

        for all s, lim(s) ::=the lub(map[n]s[..n]).


      (End of 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 λ calculus, without making any appeal to computation [ Scott76 ]

      Power Domains

      Plotkin has extended the domain model into a domain of sets of elements (from S to @S, approximately) [ Plotkin76 ]


      References


      (Kleene52): S.C. Kleene, Introduction to Metamathematics, Van Nostrand, 1952.


      (Manes&Arbib86): Manes & Michael Arbib,Algebraic Approaches to Program Semantics, Springer Verlag Monograph 1986 [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 [ACM 86]

    . . . . . . . . . ( end of section Domains) <<Contents | End>>

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End