资料来源 : Free On-Line Dictionary of Computing

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)