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:- Operational semantics: the semantics of a language is described as the set of the computations of programs. These are usually expressed as a partial function between the language's closed terms (i.e. the programs) and the resulting values, if any, where values are a set of closed normal form terms with observable type. This partial function is named the evaluation function.
- Denotational semantics: programs are mapped to elements in some mathematical model, the intended model. As an example, in functional programs are usually mapped to functions.
- Logical semantics: specifies a class of possible models for the language.
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