The denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do. The theory makes use of a computational mathematical [[Domain theory|___domain]] <'''Denotations''', ≤>. Examples of such objects are partial functions, sequencessets of states, and [[Actor model|Actor]] event diagramsscenarios. UsuallyThe there is a partial ordering <tt>≤</tt> on these objects withrelationship <tt>x≤y</tt> meaningmeans that <tt>x</tt> iscan compatiblecomputationally withevolve but possibly less defined than <tt>y</tt>. In other words, </tt>x</tt> approximatesto <tt>y</tt>. If the objectsdenotations are partial functions, for example, <tt>f≤g</tt> may mean that <tt>f</tt> agrees with <tt>g</tt> on all values for which <tt>f</tt> is defined. If the objectsdenotations are [[Actor model|Actor]] event diagram denotationsscenarios, <tt>x≤y</tt> means that as system which satisfies <tt>x</tt> iscan aevolve possibleinto initiala historysystem ofwhich satisfies <tt>y</tt>.
As computation continues, the approximationsdenotations should become better and have a limit so if we have <tt>∀i∈ω x<sub>i<sub>≤x<sub>i+1<sub> then the [[least upper bound]] <tt>∨<sub>i∈ω</sub> x<sub>i</sub></tt> should exist. The property just stated is called ω-completeness.
The mathematical objectdenotation denoted by a system <tt>S</tt> is found by solving by constructing increasingly better approximations from an initial empty approximationdenotation called <tt>⊥<sub>S</sub></tt> using some approximationdenotation buildingapproximating function <tt>'''progression'''<sub>S</sub></tt> to constuct a denotation (meaning ) for <tt>S</tt> as follows:
