We have now seen two operational models for programming languages: small-step and large-step. In this nnote, we consider a different semantic model, called denotational semantics.
The idea in denotational semantics is to express the meaning of a program as the mathematical function that expresses what the program computes. We can think of an IMP program as a function from stores to stores: given an an initial store, the program produces a final store. For example, the program can be thought of as a function that when given an input store , produces a final store that is identical to except that it maps foo to the integer ; that is, . We will model programs as functions from input stores to output stores. As opposed to operational models, which tell us how programs execute, the denotational model shows us what programs compute.
A Denotational Semantics for IMP
For each program , we write for the denotation of , that is, the mathematical function that represents: Note that is actually a partial function (as opposed to a total function), both because the store may not be defined on the free variables of the program and because program may not terminate for certain input stores. The function is not defined for non-terminating programs as they have no corresponding output stores.
We will write for the result of applying the function to the store 𝜎. That is, if is the function that denotes, then we write to mean the same thing as .
We must also model expressions as functions, this time from stores to the values they represent. We will write for the denotation of arithmetic expression , and for the denotation of boolean expression . Now we want to define these functions. To make it easier to write down these definitions, we will describe (partial) functions using sets of pairs. More precisely, we will represent a partial map as a set of pairs and such that, for each ,there is at most one pair of the form in the set. Hence is the same as .
We can now define denotations for IMP. We start with the denotations of expressions: The denotations for commands are as follows: Note that , where is the composition of relations, defined as follows: if and then is . If and are total functions, then is function composition. But now we have a problem: the last “definition” is not really a definition because it expresses in terms of itself! This is not a definition but a recursive equation. What we want is the solution to this equation.
Fixed Points
We gave a recursive equation that the function must satisfy. To understand some of the issues involved, let’s consider a simpler example. Consider the following equation for a function This is not a definition for , but rather an equation that we want to satisfy. What function, or functions, satisfy this equation for ? The only solution to this equation is the function .
In general, there may be no solutions for a recursive equation ( e. g, there are no functions In general, there may be no solutions for a recursive equation ( e. g, there are no functions that satisfy the recursive equation , or multiple solutions (e.g., find two functions that satisfy
We can compute solutions to such equations by building successive approximations. Each approximation is closer and closer to the solution. To solve the recursive equation for , we start with the partial function ( i. e, is the empty relation; it is a partial function with the empty set the partial function ( i. e, is the empty relation; it is a partial function with the empty set for it's domain). We compute successive approximations using the recursive equation. This sequence of successive approximations gradually builds the function .
We can model this process of successive approximations using a higher-order function that takes one approximation and returns the next approximation : where A solution to the recursive equation is a function such that . In general, given a function , we have that is a fixed point of if We also write to indicate that is a least fixed point of
So the solution to the recursive equation is a fixed-point of the higher-order function We can compute this fixed point iteratively, starting with and at each iteration computing The fixed point is the limit of this process:
Denotation for Loops
We can now write the correct denotation case for while loops as the fixed point of a higher-order function:
