Powerdomain

1 definition found

From The Free On-line Dictionary of Computing (27 SEP 03) [foldoc]:

  powerdomain
       
           The powerdomain of a {domain} D is a domain
          containing some of the {subsets} of D.  Due to the asymmetry
          condition in the definition of a {partial order} (and
          therefore of a domain) the powerdomain cannot contain all the


          subsets of D.  This is because there may be different sets X
          and Y such that X <= Y and Y <= X which, by the asymmetry
          condition would have to be considered equal.
       
          There are at least three possible orderings of the subsets of
          a powerdomain:
       
          Egli-Milner:
       
          	X <= Y  iff  for all x in X, exists y in Y: x <= y
          	        and  for all y in Y, exists x in X: x <= y
       
          ("The other domain always contains a related element").
       
          Hoare or Partial Correctness or Safety:
       
          	X <= Y  iff  for all x in X, exists y in Y: x <= y
       
          ("The bigger domain always contains a bigger element").
       
          Smyth or Total Correctness or Liveness:
       
          	X <= Y  iff  for all y in Y, exists x in X: x <= y
       
          ("The smaller domain always contains a smaller element").
       
          If a powerdomain represents the result of an {abstract
          interpretation} in which a bigger value is a safe
          approximation to a smaller value then the Hoare powerdomain is
          appropriate because the safe approximation Y to the
          powerdomain X contains a safe approximation to each point in
          X.
       
          ("<=" is written in {LaTeX} as {\sqsubseteq}).
       
          (1995-02-03)