The definition of semantic models

The relations between different semantic models

The relations between different approaches to meaning

The relation between computation and the underlying mathematical structures from fields such as , set theory, model theory, category theory, etc.

logic

,^[6] whereby each phrase in the language is interpreted as a denotation, i.e. a conceptual meaning that can be thought of abstractly. Such denotations are often mathematical objects inhabiting a mathematical space, but it is not a requirement that they should be so. As a practical necessity, denotations are described using some form of mathematical notation, which can in turn be formalized as a denotational metalanguage. For example, denotational semantics of functional languages often translate the language into domain theory. Denotational semantic descriptions can also serve as compositional translations from a programming language into the denotational metalanguage and used as a basis for designing compilers.

Denotational semantics

,^[7] whereby the execution of the language is described directly (rather than by translation). Operational semantics loosely corresponds to interpretation, although again the "implementation language" of the interpreter is generally a mathematical formalism. Operational semantics may define an abstract machine (such as the SECD machine), and give meaning to phrases by describing the transitions they induce on states of the machine. Alternatively, as with the pure lambda calculus, operational semantics can be defined via syntactic transformations on phrases of the language itself;

Operational semantics

,^[8] whereby one gives meaning to phrases by describing the axioms that apply to them. Axiomatic semantics makes no distinction between a phrase's meaning and the logical formulas that describe it; its meaning is exactly what can be proven about it in some logic. The canonical example of axiomatic semantics is Hoare logic.

Axiomatic semantics

^[9] is an approach that tries to modularize denotational semantics, splitting the formalization process in two layers (macro and microsemantics) and predefining three semantic entities (actions, data and yielders) to simplify the specification;

Action semantics

^[8] is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program semantics in a formal manner. It also supports denotational semantics and operational semantics;

Algebraic semantics

^[10] define systems that systematically compute "metadata" (called attributes) for the various cases of the language's syntax. Attribute grammars can be understood as a denotational semantics where the target language is simply the original language enriched with attribute annotations. Aside from formal semantics, attribute grammars have also been used for code generation in compilers, and to augment regular or context-free grammars with context-sensitive conditions;

Attribute grammars

(or "functorial") semantics^[11] uses category theory as the core mathematical formalism. Categorical semantics is usually proven to correspond to some axiomatic semantics that gives a syntactic presentation of the categorical structures. Also, denotational semantics are often instances of a general categorical semantics;^[12]

Categorical

^[13] is a catch-all term for any formal semantics that describes concurrent computations. Historically important concurrent formalisms have included the actor model and process calculi;

Concurrency semantics

^[14] uses a metaphor inspired by game theory;

Game semantics

,^[15] developed by Edsger W. Dijkstra, describes the meaning of a program fragment as the function transforming a postcondition to the precondition needed to establish it.

Predicate transformer semantics

To prove that a particular operational semantics for a language satisfies the logical formulas of an axiomatic semantics for that language. Such a proof demonstrates that it is "sound" to reason about a particular (operational) interpretation strategy using a particular (axiomatic) proof system.

To prove that operational semantics over a high-level machine is related by a with the semantics over a low-level machine, whereby the low-level abstract machine contains more primitive operations than the high-level abstract machine definition of a given language. Such a proof demonstrates that the low-level machine "faithfully implements" the high-level machine.

simulation

Computational semantics

Formal semantics (logic)

Formal semantics (linguistics)

Ontology

Ontology (information science)

Semantic equivalence

Semantic technology

Aaby, Anthony (2004). . Archived from the original on 2015-06-19. Semantics.

Introduction to Programming Languages