What is the meaning of a program? When we write a program, we represent it using sequences of characters. But these strings are just concrete syntax—they do not tell us what the program actually means. It is tempting to define meaning by executing programs--either using an interpreter or a compiler. But interpreters and compilers often have bugs! We could look in a specification manual.

But such manuals typically only offer an informal description of language constructs. A better way to define meaning is to develop a formal, mathematical definition of the semantics of the language. This approach is unambiguous, concise, and most importantly, it makes it possible to develop rigorous proofs about properties of interest. The main drawback is that the semantics itself can be quite complicated, especially if one attempts to model all of the features of a full-blown modern programming language.

There are three pedigreed ways of defining the meaning, or semantics, of a language:

  • Operational semantics: defines meaning in terms of execution on an abstract machine.

  • Denotational semantics: defines meaning in terms of mathematical objects such as functions.

  • Axiomatic semantics: defines meaning in terms of logical formulas satisfied during execution.

Each of these approaches has advantages and disadvantages in terms of how mathematically so phisticated they are, how easy they are to use in proofs, and how easy it is to use them to implement an interpreter or compiler. We will discuss these tradeoffs later in this course.

Arithmetic Expression

To understand some of the key concepts of semantics, let us consider a very simple language of integer arithmetic expressions with variable assignment. A program in this language is an expression; executing a program means evaluating the expression to an integer. To describe the syntactic structure of this language we will use variables that range over the following domains: is the set of program variables (e.g., foo, bar, baz, i, etc.). is the set of constant integers (e.g., 42, 40, 7). is the domain of expressions, which we specify using a BNF (Backus–Naur Form) grammar: Informally, the expression means that is assigned the value of before evaluating . The result of the entire expression is the value described by .

This grammar specifies the syntax for the language. An immediate problem here is that the grammar is ambiguous. Consider the expression 1 + 2 * 3. One can build two abstract syntax trees:

  +                        *
 / \                      / \
1   *                    +   3
   / \                  / \
  2   3                1   2

There are several ways to deal with this problem. One is to rewrite the grammar for the samelanguage to make it unambiguous. But that makes the grammar more complex and harder to understand. Another possibility is to extend the syntax to require parentheses around all addition and multiplication expressions: However, this also leads to unnecessary clutter and complexity. Instead, we separate the “concrete syntax” of the language (which specifies how to unambiguously parse a string into program phrases) from its “abstract syntax” (which describes, possibly ambiguously, the structure of program phrases). In this course we will assume that the abstract syntax tree is known. When writing expressions, we will occasionally use parenthesis to indicate the structure of the abstract syntax tree, but the parentheses are not part of the language itself. (For details on parsing, grammars, and ambiguity elimination, see or take CS 4120.)

Representing Expressions

The syntactic structure of expressions in this language can be compactly expressed in OCaml using datatypes:

type exp = Var of string
    | Int of int
    | Add of exp * exp
    | Mul of exp * exp
    | Assgn of string * exp * exp

This closely matches the BNF grammar above. The abstract syntax tree (AST) of an expression can be obtained by applying the datatype constructors in each case. For instance, the AST of expression 2 * (foo + 1) is:

Mul(Int(2), Add(Var("foo"), Int(1)))

In OCaml, parentheses can be dropped when there is one single argument, so the above expression can be written as:

Mul(Int 2, Add(Var "foo", Int 1))

We could express the same structure in a language like Java using a class hierarchy, although it would be a little more complicated:

abstract class Expr { }
class Var extends Expr { String name; .. }
class Int extends Expr { int val; ... }
class Add extends Expr { Expr exp1, exp2; ... }
class Mul extends Expr { Expr exp1, exp2; ... }
class Assgn extends Expr { String var, Expr exp1, exp2; .. }

Operational Semantics

We have an intuitive notion of what expressions mean. For example, the 7 + (4 * 2) evaluates to 15, and evaluates to 42. In this section, we will formalize this intuition precisely.

An operational semantics describes how a program executes on an abstract machine. A small-step operational semantics describes how such an execution proceeds in terms of successive reductions--here, of an expression--until we reach a value that represents the result of the computation. The state of the abstract machine is often referred to as a configuration. For our language a configuration must include two pieces of information:

  • a store (also known as environment or state), which maps variables to integer values. During program execution, we will refer to the store to determine the values associated with variables, and also update the store to reflect assignment of new values to variables,

  • the expression to evaluate.

We will represent stores as partial functions from Var to Int and configurations as pairs of expressions and stores: We will denote configurations using angle brackets. For instance, is a configuration where is a store and is an expression that uses two variables, foo and bar. The small-step operational semantics for our language is a relation that describes how one configuration transitions to a new configuration. That is, the relation shows us how to evaluate programs one step at a time. We use infix notation for the relation . That is, given any two configurations and , if the pair is in the relation , then we write . For example, we have . That is, we can evaluate the configuration one step to get the configuration .

Using this approach, defining the semantics of the language boils down to to defining the relation → that describes the transitions between configurations.

One issue here is that the domain of integers is infinite, as is the domain of expressions. Therefore, there is an infinite number of possible machine configurations, and an infinite number of possible single-step transitions. We need a finite way of describing an infinite set of possible transitions. We can compactly describe using inference rules: The meaning of an inference rule is that if the facts above the line holds, then the fact below the line holds. The fact above the line are called premises; the fact below the line is called the conclusion. The rules without premises are axioms; and the rules with premises are inductive rules. We use the notation for the store that maps the variable to integer , and maps every other variable to whatever maps it to. More explicitly, if is the function , then we have:

Now let's see how we can use these rules. Suppose we want to evaluate the expression with a store where and . That is, we want to find the transition for the configuration . For this, we look for a rule with this form of a configuration in the conclusion. By inspecting the rules, we find that the only rule that matches the form of our configuration is LMul, where and but is not yet known. We can instantiate LMul, replacing the metavariables and with appropriate expressions.

Now we need to show that the premise actually holds and find out what is. We look for a rule whose conclusion matches . We find that LADD is the only matching rule:

We repeat this reasoning for and find that the only applicable rule is the axiom VAR:

Since this is an axiom and has no premises, there is nothing left to prove. Hence, and . We can put together the above pieces and build the following proof:

This proves that, given our inference rules, the one-step transition

is derivable. The structure above is called a "proof tree" or "derivation". It is important to keep in mind that proof trees must be finite for the conclusion to be valid.

We can use a similar reasoning to find out the next evaluation step:

And we can continue this process. At the end, we can put together all of these transitions, to get a view of the entire computation:

The result of the computation is a number, 24 . The machine configuration that contains the final result is the point where the evaluation stops; they are called final configurations. For our language of expressions, the final configurations are of the form .

We write for the reflexive and transitive closure of the relation . That is, if using zero or more steps, we can evaluate the configuration to . Thus, we have: