Semantics

The term that applies in various ways to describe what the programs of a language mean. This is usually intended equivalent to describing what does the program produce as its output, or to mapping programs to other mathematical objects which are "better understood" than programs. As a consequence, the styles to express a language's semantics are usually divided in three classes:

A different approach to defining the semantics of a language is describing when two program are equivalent, i.e. when they can replace each other in all the relevant contexts. Formally, this means defining an equational theory over the programs of a language, which is named an axiomatic semantics if it is axiomatizable. Since the notion of "relevant context" can be flexibly adapted to the situation, different equational theories (and therefore different semantics) can be defined for a same language by equating processes at a more or less fine grain according to need. This is the case of pi calculus, whose many semantics equate processes according to their mutual ability to simulate each other, and different flavors of "bisimulation" are adopted according to the kind of relevant observable behaviors. This approach is commonly adopted for most calculi for concurrent, communicating distributed processes. The equational theories determined by bisimulations at a coarser grain than step-by-step mutual simulation are named observational semantics.

Proving equivalence of two programs from their operational, denotational, or logical semantics implies, respectively, determining whether two programs always produce the same values when applied on the same argument, whether the denotation of two programs is the same in the intended model, and whether the denotation of the program is the same in all the possible models. In any case they all define an equational theory. For sequential languages and formal calculi like the lambda calculus, the "natural" equivalence between programs is that defined by the operational semantics. When the equational theory defined by a language's denotational semantics is sound and complete wrt that of its operational semantics, the former is said to be fully abstract.

Category-theoretic semantics use the concepts of category theory.


Page in this topic: Algebraic Specification  


Also linked from: Algebra and coalgebra   Bisimulation   C Compiler dlopen VM   Combining Languages   Eidola   Functional   Hypertext   Initiality and finality   Janus   Language   Macro   Oz   Programming Language Semantics 101   Reification   Sheep   Transparent   WYSIWYM