Denotational semantics: Difference between revisions

Revision as of 17:42, 24 November 2005

Revision as of 18:03, 24 November 2005

Line 7:

==Fixed point semantics==

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|___domaindomains]] <'''Denotations''', ≤>. Examples of such objectscomputational domains are partial functions, sets of states, and [[Actor model|Actor]] event scenarios. The relationship <tt>x≤y</tt> means that <tt>x</tt> can computationally evolve to <tt>y</tt>. If the denotations 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 denotations are [[Actor model|Actor]] event diagram scenarios, <tt>x≤y</tt> means that a system which satisfies <tt>x</tt> can evolve into a system which satisfies <tt>y</tt>.

The relationship <tt>x≤y</tt> means that <tt>x</tt> can computationally evolve to <tt>y</tt>. If the denotations 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 denotations are [[Actor model|Actor]] event diagram scenarios, <tt>x≤y</tt> means that a system which satisfies <tt>x</tt> can evolve into a system which satisfies <tt>y</tt>.

As computation continues, the denotations 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>∨_i∈ω x_i</tt> should exist. The property just stated is called ω-completeness.

Computational domains have the following properties:

#''Limits exist'' As computation continues, the denotations 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>∨_i∈ω x_i</tt> should exist. The property just stated is called ω-completeness.

#''Finite elements are countable'' an element <tt>x</tt> is finite (also called isolated in the ___domain literature) if and only if whenever <tt>A</tt> is directed, <tt>∨A</tt> exists and <tt>x≤∨A</tt>, there exists <tt>a∈A</tt> with <tt>x≤a</tt>. In other words, <tt>x</tt> is finite if one must go through <tt>x</tt> in order to get up to or above <tt>x</tt> via the limit process.

#''Every element is the least upper bound of a countable increasing sequence of finite elements.''

The mathematical denotation denoted by a system <tt>S</tt> is found by solving by constructing increasingly better approximations from an initial empty denotation called <tt>⊥_S</tt> using some denotation approximating function <tt>'''progression'''_S</tt> to constuct a denotation (meaning ) for <tt>S</tt> as follows: