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
It can can be described in a different way by a function describing a single iteration:
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.
The following is abstracted from Dana Scott's lecture [ Scott76 ] but owes much to Manes and Arbib's book [ Manes&Arbib86] .
Typographically the relation (<=) is shown as an square cornered subset_or_equal symbol.
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
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:
So in consequence an equation/iteration like
has a unique relation do(R) as its solution.
. . . . . . . . . ( end of section Examples) <<Contents | End>>
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.
for all s, lim(s) ::=the lub(map[n]s[..n]).
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 ]
Plotkin has extended the domain model into a domain of sets of elements (from S to @S, approximately) [ Plotkin76 ]
(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>>
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 ]
For a more rigorous description of the standard notations see