CS611 Lecture 17 Denotational Semantics of IMP October 10, 2001Scribe: Rohit Ananthakrishna and Manpreet Singh (based on earlier notes from Cristina Patron and SuzanneShontz) Lecturer: Andrew Myers1 Operational Semantics vs. Denotational SemanticsWe have described the behaviour of programs in IMP in an operational manner by inductively definingtransition relations to express evaluation and execution. The style of semantics we used is often calledstructural operational semantics because of the syntax-directed way in which the rules are presented. It isalso called natural semantics because of the way derivations resemble proofs in natural deduction.It is fairly easy to to turn the description of the semantics into a recursive-descent interpreter for IMP.On the other hand, it is hard to compare two programs written in different programming languages. Thissuggests we should define the meaning of a program in terms of the underlying semantic domain. We willhave a semantic function (called denotation) which maps pieces of syntax to meanings. This new style ofsemantics, called denotational semantics, can be thought of as describing a compiler for IMP that convertssyntax into an extensional representation of that syntax.2 Semantic FunctionsDenotational semantics operates on expressions to produce mathematical objects that are the meaning ofthe expression. The mechanism for this is a semantic function, which is usually a mathematical function.We now give an example.Example: C[[ ( λxx)]] = λx ∈ D.xHere C is a semantic function that represents the action of a compiler. It takes as input (λxx), whichis a piece of abstract syntax. (Note: (λxx) should really be thought of as an abstract syntax tree.) It thengives meaning to the expression. The brackets [[ ]] are used to represent this. The meaning of (λxx)isgiven mathematically on the right-hand side of the equation. The meaning is that λ takes x ∈ D and returnsλ(x). This can be thought of in terms of function extensions. In this case, the extension of λ is given by{(a, a) | a ∈ D}.Now that we are using λ−expressions to describe mathematical functions, we need to determine how toparse them.We start off by giving the convention for a mathematical function of several variables. λxyz.e means that λtakes the three variables x, y, and z as input and gives e as output. Because we apply λ left-to-right, this isthe same as λxλyλz.e.Thenextruleforλ−expressions is that they extend as far to the right as possible.Thus, λxλyλz.xλw.w = λx(λy(λz.(x(λw.w)))). Be careful with those parentheses!The final rule is that application is left associative. Thus, xyz =(xy)z = x(y, z).So, an example of a function taking many variables as inputs is f = λxyz.e = λxλyλz.e.Typed functions are simply functions and their types. We will usually write the types of the argumentsfor mathematical functions unless the name of the argument makes it obvious. Suppose we want to add twointegers x and y. This can be achieved using the following PLUS function:PLUS = λx ∈ Z.λy ∈ Z.x + y.1This function takes x ∈ Z and y ∈ Z (one argument at a time) and yields x + y ∈ Z. Thus, the domain isZ × Z and the codomain is Z.Mathematically, this is written as:PLUS :(Z × Z) → Z;(x, y) −→ x + y.Because (Z × Z) → Z is isomorphic to Z → (Z → Z) and because PLUS operates on one input argumentat a time, this is the same as:PLUS ∈ Z → (Z → Z).Note that while application associates to the left, the constructor (→) associates to the right, i.e., Z → Z → Z = Z → (Z → Z).3 Semantic Functions for IMPRecall now the three kinds of expressions in IMP:• arithmetic expressionsa ::= n | X | a0+ a1| a0− a1| a0× a1• boolean expressionsb ::= a0≤ a1| a0= a1|¬b | b0∧ b1| b0∨ b1• commandsX := a0| skip | if b0then c0else c1| while b0do c0What is the intrinsic meaning of these syntactic categories?Let us take for example the arithmetic expressions. Our first thought, when we see an expression is toevaluate it and thus the meaning of an arithmetic expression is an integer. Notice though that this evalua-tion depends on the particular store we have: given store σ, each expression a denotes a unique integer, sothe meaning of an arithmetic expression is really a function from stores to integers. Hence we can define afunction A which translates the syntax of the arithmetic expressions into their meaning:A[[ a]] σ = n ⇔a, σ⇓nSimilarly, given a particular store σ boolean expressions b denotes a unique truth value. We can define:B[[ b]] σ = t ⇔b, σ⇓tSince a command c maps one store into another, we define:C[[ c]] σ = σ⇔c, σ⇓σIn conclusion, we have the meaning functions A, B, C:•A∈Aexp → (Σ → N )•B∈Bexp → (Σ → T )•C∈Com → (Σ → Σ)We say that the arithmetic expression a denotes A[[ a]] a n d A[[ a]] is a denotation of a. Similarly, B[[ b]] i s adenotation of the boolean b and C[[ c]] is a denotation of command c. Each denotation is in fact a function:•A[[ a]]:Σ→ N2•B[[ b]] : Σ → T•C[[ c]]:Σ→ ΣThis signature for C won’t quite work, however, because of the possibility of non-termination. We’ll see howto fix it shortly.The functions A, B, C are defined by structural induction.3.1 Arithmetic DenotationsFirstly, we define the denotation of arithmetic expressions A∈Aexp → (Σ → N ) using structural induction:•A[[ n]] = λσ ∈ Σ.nThis means that the denotation of n is a function which associates the natural number n to any state σ.Similarly,•A[[ X]] = λσ ∈ Σ.σX•A[[ a0+ a1]] = λσ ∈ Σ. A[[ a0]] σ + A[[ a1]] σ•A[[ a0− a1]] = λσ ∈ Σ. A[[ a0]] σ −A[[ a1]] σ•A[[ a0× a1]] = λσ ∈ Σ. A[[ a0]] σ ×A[[ a1]] σNotice that the signs +, −, × on the left-hand sides represent syntactic signs in IMP, whereas the signs onthe right represent operations on numbers.We can write the last three definitions as inductive definitions, similar to the inference rules in the operationalsemantics:A[[ a0]] = f0A[[ a1]] = f1A[[ a0+ a1]] = λσ ∈ Σ.f0σ + f1σInstead of using the λ-notation, we can present the definition of the semantics as a relation between statesand numbers:•A[[ n]] = {(σ, n)|σ ∈ Σ}•A[[ X]] = {(σ, σ(X)|σ ∈ Σ}•A[[ a0+ a1]] = {(σ, n0+ n1)|(σ, n0) ∈A[[ a0]] ∧ (σ, n1) ∈A[[ a1]] }•A[[ a0− a1]] = {(σ, n0− n1)|(σ, n0) ∈A[[ a0]] ∧ (σ, n1) ∈A[[ a1]] }•A[[