| Denotational Semantics |
Articles about Denotational Semantics |
Website Links For Semantics |
Information AboutDenotational Semantics |
| CATEGORIES ABOUT DENOTATIONAL SEMANTICS | |
| logic in computer science | |
| computational models | |
| formal specification languages | |
| semantics | |
|
In Computer Science , denotational semantics is an approach to formalizing the Semantics of Computer Systems by constructing mathematical objects (called ''denotations'' or ''meanings'') which express the semantics of these systems. Other approaches to providing a Formal Semantics Of Programming Languages include Axiomatic Semantics and Operational Semantics . The denotational approach to semantics was originally developed to deal only with systems defined by a single Computer Program . Later the field broadened to include systems composed of more than one program, such as those found in Networking and Concurrent Systems . Denotational semantics originated in the work of Christopher Strachey and Dana Scott in the 1960s . As originally developed by Strachey and Scott, denotational semantics interpreted the denotation (meaning) of a computer program as a Function that mapped input into output. Later, this proved to be too limiting to allow the definition of denotations (meanings) for programs that included elements such as Recursively Defined functions and data structures. Seeking to address these difficulties, Scott introduced a generalized approach to denotational semantics, based on Domains . Later researchers introduced approaches based on Power Domains , in an effort to address difficulties with the semantics of Concurrent Systems . 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 Domains . Examples of such computational domains are partial functions and Actor event diagram scenarios. The relationship x≤y means that x can computationally evolve to y. If the denotations are partial functions, for example, f≤g may mean that f agrees with g on all values for which f is defined. If the denotations are Actor event diagram scenarios, x≤y means that a system which satisfies x can evolve into a system which satisfies y. Computational domains have the following properties: #''Bottom exists.'' The domain has a least element denoted by ⊥ such that for every element x in the domain ⊥≤x. #''Limits exist.'' As computation continues, the denotations should become better and have a limit so if we have then the Least Upper Bound should exist. The property just stated is called -completeness. #''Finite elements are countable.'' An element x is finite (also called isolated in the domain literature) if and only if whenever A is Directed , ∨A exists and , there exists with . In other words, x is finite if one must go through x in order to get up to or above x via the limit process. #''Every element is the least upper bound of a countable increasing sequence of finite elements.'' Intuitively this means that every element can be reached by a computational process in which each progression is finite. #''The domain is downward closed.'' The mathematical denotation denoted by a system S is found by solving by constructing increasingly better approximations from an initial empty denotation called ⊥S using some denotation approximating function progressionS to construct a denotation (meaning ) for S as follows 2006b : ::DenoteS ≡ ∨i∈ω '''progression'''Si(⊥S). It would be expected that progressionS would be ''monotone'', ''i.e.'', if x≤y then progressionS(x)≤progressionS(y). More generally, we would expect that ::If ∀i∈ω xi≤xi+1, then progressionS(∨i∈ω xi) = ∨i∈ω progressionS(xi) This last stated property of progressionS is called ω-continuity. A central question of denotational semantics is to characterize when it is possible to create denotations (meanings) in according to the equation for DenoteS. A fundamental theorem of computational domain theory is that if '''progression'''S is ω-continuous then DenoteS will exist. It follows from the ω-continuity of progressionS that :::progressionS('''Denote'''S) = '''Denote'''S The above equation motivates the terminology that DenoteS is a ''fixed point'' of '''progression'''S. Furthermore this fixed point is least among all fixed points of progressionS. The denotational semantics of functional programs provides an example of fixed point semantics as shown in the next section. Example of factorial function Consider the factorial function which is defined on all non-negative numbers as follows:
The graph of factorial is the set of all ordered pairs for which factorial is defined with the first element of an ordered pair being the argument and the second element being the value, ''e.g.'', |
|
|