Denotational Semantics

Denotational semantics is a formal method for expressing the semantic definition of a programming language (or a program in that language).

Other approaches are axiomatic (Hoare methods), algebraic (Guttag ADTs), and operational (a virtual machine, Java).

In denotational semantics, the idea is to map every syntactic entity in a PL into some appropriate mathematical entity. The math is the "denotation" for the syntax, of the "syntax denotes the semantic entity."

Each denotational semantic definition consists of 5 parts:

  1. syntactic categories
  2. BNF defining the structure of the syntactic categories
  3. value domains (the mathmatical entities to be mapped)
  4. semantic functions (signatures for mappings from syntax to semantic domains)
  5. semantic equations (the rules defining the semantic functions) mappings )
In general, there will be one semantic function for each syntax category, and one semantic equation for every production in the syntax grammar.

Example: language of non-negative integers

Syntactic Categories
  D in Digits  (decimal digits)
  N in Num     (decimal natural numbers)
Syntax BNF
   D  ::=  0  |  1  |  ...  |  9
   N  ::=  D  |  N  D 
Value Domains
   Nat = { 0, 1, 2, 3, 4, ... }   natural numbers
Semantic Functions
   DD :  Digits --> Nat
   MM :  Num    --> Nat
Semantic Equations
   DD [0] = 0
   DD [1] = 1
   DD [2] = 2
   DD [9] = 9
   MM [D] = DD [D]
   MM [N D] = 10 * MM [N] + MM [D]