§1 DENOTATIONAL SEMANTICS 1

1. Denotational Semantics. Denotational semantics is a formal method to specify the meaning of programming languages. We define an abstract syntax for the language (Term), a meaning function (Me), a polymorphic store (store) and a polymorphic environment (env ).

The code is laid out in this document in a logical form (rather than slavishly following the order the compiler wants), but we must force the code into the right order to make sure that things are defined before use.

⟨ Type Definitions 2 ⟩

⟨ Functions 52 ⟩

⟨ Meaning Function 6 ⟩;

⟨ Test Cases 54 ⟩

2. This is the type of possible declarations, along with the start of the definition of possible terms. They are mutually recursive definitions so they must be connected by an and. The actual declaration type are explained below in the definition of the semantic function for declarations. ⟨ Type Definitions 2 ⟩ ≡

datatype Decl = Var Decl of string×Term | Val Decl of string × Term | Rec Decl of string × Term

and ⟨ Term Definition 5 ⟩;

See also sections 47, 48, 49, 50, and 51. This code is used in section 1.

§3 TERM AND ME 2

3. Term and Me. We define the datatype for the abstract syntax tree and the meaning function in parallel. will worry about putting it all together in the right order.

The meaning function has to have type:

Me : Term ↦ (Value env ) ↦ (Value continuation) ↦ (Value store) ↦ (Value × (Value store)).

That is, it maps abstract syntax trees, environments, continuations, and stores to a value,store pair.

4. The denotational semantics are given in terms of the following:

Me - this is the meaning function itself. Ξ - is an invalid value ε - an expression ξ - a symbol ν - a number ρ - the environment (bindings from names to values) θ - this is the continuation Θ - this is a null continuation that simply returns the value σ - this is the store of values ϕ - a location in the store

x[e/v] - a substitution of the expression e for the name (or whatever) v, where x is usually ρ or σ x[[v]] - v in the context of x, where x is Me, ρ, σ, O or V ⟨x, y⟩ - the tuple composed of x and y

{e} - a continuation that evaluates e in the current context

When either of the environment or store are omitted, the environment or store from the enclosing environment is assumed.

5. The first type of term is the name of a variable or constant. The meaning of a name is the value that the environment contains for that name. For variables, this value is the location in the store where the value may be found. ⟨ Term Definition 5 ⟩ ≡

Term = Var of string

See also sections 7, 9, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35, 37, 39, 41, 43, and 45. This code is used in section 2.

6. Me[[ξ]]ρθσ = θ⟨ρ[[ξ]], σ⟩ ⟨ Meaning Function 6 ⟩ ≡

fun Me (Var x) e c s = c (lookup x e, s)

See also sections 8, 10, 11, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38, 40, 42, 44, and 46. This code is used in section 1.

7. Integer constants. ⟨ Term Definition 5 ⟩+ ≡

| Numeral of int

8. Me[[ν]]ρθσ = θ⟨V[[ν]], σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Numeral n) e c s = c (intValue n, s)

§9 DECLARATIONS 3

9. Declarations.

Declarations come in 3 flavours: val, rec, and var. For all three, the declaration only holds for the evaluation of the expression with which it is composed. val introduces a constant. rec is similar but the symbol is introduced into the environment of the expression (which must be a function) to allow for recursive calls. var introduces a variable. ⟨ Term Definition 5 ⟩+ ≡

| Decl of Decl × Term

10. Me[[var ξ = ε_{1} ; ε_{2}]]ρθσ = Me[[ε_{2}]]ρ[ϕ/ξ]θσ[Me[[ε_{1}]]ρΘσ/ϕ] ⟨ Meaning Function 6 ⟩+ ≡

| Me (Decl (Var Decl (x, V), E)) e c s =

Me V e (

λ (R, ) ⇒ let

val (S, L) = new s R;

val nE = bind x (lvalueValue L) e; in

Me E nE c S

end ) s

11. Me[[val ξ = ε_{1} ; ε_{2}]]ρθσ = Me[[ε_{2}]]ρ[Me[[ε_{1}]]ρΘσ/ξ]θσ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Decl (Val Decl (x, V), E)) e c s =

Me V e (

λ (R, ) ⇒ Me E (bind x R e) c s
) s

12. The interpretation of the recursive declaration (Me[[rec ξ = ε_{1} ; ε_{2}]]ρθσ) is fairly difficult to describe, short of translating the ML code. There are a couple of ways of doing this, but the one I chose is to implement the Y combinator (fix) in the language and then apply it to the functional we want to make recursive. To bootstrap the process, we put an entry for fix into the environment as a var name with an initial binding to an invalid value, which we replace once we have a definition for the function proper. If we were looking for efficiency, we’d put these in the initial environment and store. ⟨ Meaning Function 6 ⟩+ ≡

| Me (Decl (Rec Decl (x, V), E)) e c s = let

val fixpoint = Proc (  , Proc (  , App (App (Var  , App (Deref (Var  )
, Var  )), Var  )));

val (S, L) = new s invalidValue;

val nE = bind (lvalueValue L) e; in

Me fixpoint nE (

λ (FIX , ) ⇒

Me (App (Deref (Var ), Proc (x, V))) nE ( λ (funcValue R, S) ⇒ Me E (bind x (funcValue R) e) c S | ⇒ raise NotFuncDecl

) (update S L FIX )

) S end

§13 FUNCTION OPERATIONS 4

13. Function operations.

Function abstraction. Define a function of one parameter bound in the scope of the expression. ⟨ Term Definition 5 ⟩+ ≡

| Proc of string× Term

14. Me[[proc ξ => ε]]ρθσ = θ⟨λθ′.λ⟨V, σ′⟩.Me[[ε]]ρ[V/ξ]θ′σ′, σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Proc (x, E)) e c s =

c (

funcValue (

λ C ⇒

λ (V , S) ⇒ Me E (bind x V e) C S

) , s )

15. Function Application. Supply one parameter to the function and execute the function. ⟨ Term Definition 5 ⟩+ ≡

| App of Term× Term

16. The interpretation of function application (Me[[ε_{1}(ε_{2})]]ρθσ) is basically going to be a translation of the ML code. ⟨ Meaning Function 6 ⟩+ ≡

| Me (App (E1 , E2 )) e c s =

Me E1 e (

λ (funcValue f, ) ⇒ Me E2 e (

λ VS ⇒ f c VS

) s

| ⇒ raise NotFunc ) s

17. Call the specified function passing our continuation as a functional parameter. ⟨ Term Definition 5 ⟩+ ≡

| Callcc of Term

18. The interpretation of function application (Me[[callcc ε]]ρθσ) is basically going to be a translation of the ML code. ⟨ Meaning Function 6 ⟩+ ≡

| Me (Callcc E) e c s =

Me E e (

λ (funcValue f, ) ⇒

f c (

funcValue (

λ (C : Value continuation) ⇒ c )

, s ) | ⇒ raise NotFunc

) s

§19 OPERATIONS ON PAIRS 5

19. Operations on Pairs.

Create a pair from the values of two expressions. ⟨ Term Definition 5 ⟩+ ≡

| Pair of Term× Term

20. Me[[<ε_{1},ε_{2}>]]ρθσ = θ⟨Me[[ε_{1}]]ρΘσ, Me[[ε_{2}]]ρΘσ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Pair (E1 , E2 )) e c s =

Me E1 e (

λ (V1 , ) ⇒
Me E2 e (

λ (V2 , S) ⇒ c (pairValue (V1 , V2 ), s)

) s
) s

21. Get the first element from a pair. ⟨ Term Definition 5 ⟩+ ≡

| Fst of Term

22. Me[[fst ε]]ρθσ = θ⟨π_{1}(Me[[ε]]ρΘσ), σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Fst T) e c s =

Me T e ( λ (pairValue (T1 , T2 ), ) ⇒ c (T1 , s) | ⇒ raise NotPair

) s

23. Get the second element from a pair. ⟨ Term Definition 5 ⟩+ ≡

| Snd of Term

24. Me[[snd ε]]ρθσ = θ⟨π_{2}(Me[[ε]]ρΘσ), σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Snd T) e c s =

Me T e ( λ (pairValue (T1 , T2 ), ) ⇒ c (T2 , s) | ⇒ raise NotPair

) s

§25 FLOW OF CONTROL 6

25. Flow of control.

Conditional execution. Only one of the then or else expressions will be executed. ⟨ Term Definition 5 ⟩+ ≡

| Cond of Term × Term× Term

26. Me[[if ε_{1} then ε_{2} else ε_{3} fi]]ρθσ = (if Me[[ε_{1}]]ρΘσ = true then Me[[ε_{2}]] else Me[[ε_{3}]])ρθσ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Cond (E1 , E2 , E3 )) e c s =

Me E1 e ( λ (boolValue true, ) ⇒ Me E2 e c s | (boolValue false, ) ⇒ Me E3 e c s | ⇒ raise NotBool

) s

27. Expression composition. Execute the expressions sequentially. ⟨ Term Definition 5 ⟩+ ≡

| Seq of Term× Term

28. Me[[ε_{1};ε_{2}]]ρθσ = Me[[ε_{1}]]ρ{Me[[ε_{2}]]ρθ}σ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Seq (E1 , E2 )) e c s =

Me E1 e (

λ (V , S) ⇒ Me E2 e c S
) s

29. Indefinite iteration. Execute the second expression as long as the first expression evaluates to true. ⟨ Term Definition 5 ⟩+ ≡

| While of Term× Term

30. Me[[while ε_{1} do ε_{2} od]]ρθσ = (if Me[[ε_{1}]]Θσ = true then Me[[ε_{2}]]ρ{Me[[while …]]ρθ} else θ)σ ⟨ Meaning Function 6 ⟩+ ≡

| Me (While (E1 , E2 )) e c s =

Me E1 e (

λ (boolValue true, S) ⇒

Me E2 e (

λ (V , S) ⇒ Me (While (E1 , E2 )) e c S

) S

| (boolValue false, S) ⇒ c (invalidValue, S) | ⇒ raise NotBool

) s

§31 STORAGE REFERENCES AND UPDATES 7

31. Storage References and Updates.

Allocate storage for a value and return the location of the value in the store. ⟨ Term Definition 5 ⟩+ ≡

| Ref of Term

32. Me[[ref ε]]ρθσ = θ⟨ϕ, σ[Me[[ε]]ρΘσ/ϕ]⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Ref E) e c s =

Me E e (

λ (V , ) ⇒ let

val (nS , L) = new s V; in

c (lvalueValue L, nS ) end

) s

33. Given the location of a datum, get the value currently stored there. ⟨ Term Definition 5 ⟩+ ≡

| Deref of Term

34. Me[[.ε]]ρθσ = θ⟨σ[[Me[[ε]]ρΘσ]], σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Deref E) e c s =

Me E e ( λ (lvalueValue V , S) ⇒ c (access S V , s) | ⇒ raise NotLValue

) s

35. Modify the storage at the location specified by the first expression to have the value of the second expression. ⟨ Term Definition 5 ⟩+ ≡

| Assign of Term× Term

36. Me[[ε_{1}:=ε_{2}]]ρθσ = θ⟨Me[[ε_{2}]]ρΘσ, σ[Me[[ε_{2}]]ρΘσ/Me[[ε_{1}]]ρΘσ]⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Assign (E1 , E2 )) e c s =

Me E1 e (

λ (lvalueValue L, ) ⇒ Me E2 e (

λ (V , ) ⇒ c (V , update s L V)

) s

| ⇒ raise NotLValue ) s

§37 INTEGER OPERATIONS 8

37. Integer Operations.

Add two integers together. ⟨ Term Definition 5 ⟩+ ≡

| Add of Term× Term

38. Me[[ε_{1}+ε_{2}]]ρθσ = θ⟨O[[+]](Me[[ε_{1}]]ρΘσ, Me[[ε_{2}]]ρΘσ), σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Add (E1 , E2 )) e c s =

Me E1 e (

λ (intValue V1 , ) ⇒ Me E2 e (

λ (intValue V2 , ) ⇒ c (intValue (V1 + V2 ), s) | ⇒ raise NotInteger

) s | ⇒ raise NotInteger

) s

39. Multiply two integers. ⟨ Term Definition 5 ⟩+ ≡

| Mult of Term× Term

40. Me[[ε_{1}∗ε_{2}]]ρθσ = θ⟨O[[×]](Me[[ε_{1}]]ρΘσ, Me[[ε_{2}]]ρΘσ), σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Mult (E1 , E2 )) e c s =

Me E1 e (

λ (intValue V1 , ) ⇒ Me E2 e (

λ (intValue V2 , ) ⇒ c (intValue (V1 *V2 ), s) | ⇒ raise NotInteger

) s | ⇒ raise NotInteger

) s

41. Calculate the negative of an integer. ⟨ Term Definition 5 ⟩+ ≡

| Neg of Term

42. Me[[−ε]]ρθσ = θ⟨−Me[[ε]]ρΘσ, σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Neg E) e c s =

Me E e ( λ (intValue V , ) ⇒ c (intValue (0 − V), s) | ⇒ raise NotInteger

) s

§43 BOOLEAN OPERATIONS 9

43. Boolean Operations. Determine if the first integer expression is lower in value than the second. Return a boolean truth value. ⟨ Term Definition 5 ⟩+ ≡

| Less of Term× Term

44. Me[[ε_{1}<ε_{2}]]ρθσ = θ⟨O[[<]](Me[[ε_{1}]]ρΘσ, Me[[ε_{2}]]ρΘσ), σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Less (E1 , E2 )) e c s =

Me E1 e (

λ (intValue V1 , ) ⇒ Me E2 e (

λ (intValue V2 , ) ⇒ c (boolValue (V1 < V2 ), s) | ⇒ raise NotInteger

) s | ⇒ raise NotInteger

) s

45. Calculate the boolean complement of the expression. ⟨ Term Definition 5 ⟩+ ≡

| Not of Term

46. Me[[¬ε]]ρθσ = θ⟨¬Me[[ε]]ρΘσ, σ⟩ ⟨ Meaning Function 6 ⟩+ ≡

| Me (Not E) e c s =

Me E e ( λ (boolValue true, ) ⇒ c (boolValue false, s) | (boolValue false, ) ⇒ c (boolValue true, s) | ⇒ raise NotBool

) s

§47 ENVIRONMENTS 10

47. Environments. An environment captures the bindings of names to values (in this case locations). This trivial implementation has dreadful performance, but it is at least fairly obviously correct. ⟨ Type Definitions 2 ⟩+ ≡

abstype α env =

Env of string ↦ α with

exception unbound variable of string; val newenv =

Env (

λ x ⇒ raise unbound variable x );

fun bind x t (Env f) =

Env (

λ y ⇒

if x = y then

t else

f y

); fun lookup x (Env f) = f x

end;

§48 STORES 11

48. Stores. A store binds locations to values. Once again, this is just about the most inefficient implementation you could come up with (although there actually was a bug in the first version). A store can be thought of as a mapping from locations to values, where new locations are created on demand. ⟨ Type Definitions 2 ⟩+ ≡

abstype α store =

Store of int×(int ↦ α) and lvalue =

lvalue of int

with exception segmentation violation; val newstore =

Store ( 0 , λ x ⇒ raise segmentation violation );

fun new (Store (avail , f)) v =

( Store ( avail + 1 , λ l ⇒

if l = avail then

v else

f l

) , lvalue (avail ) );

fun access (Store ( , f)) (lvalue loc) = f loc; fun update (Store (avail , f)) (lvalue loc) v =

Store ( avail , λ l ⇒

if l = loc then

v else

f l

);

end;

§49 VALUES AND MISCELLANEOUS DEFINITIONS 12

49. Values and Miscellaneous Definitions. Define a continuation to be a mapping from a value,state pair to a resulting value,state. ⟨ Type Definitions 2 ⟩+ ≡

type α continuation = (α × α store) ↦ (α × α store);

50. Values. These are the set of values that can result from a computation. Only the first 3 of these were in the original problem description. I added the others to make the language/interpreter more useful and to catch and report errors. ⟨ Type Definitions 2 ⟩+ ≡

datatype Value =

intValue of int

| lvalueValue of lvalue

| funcValue of Value continuation ↦ Value continuation | boolValue of bool | pairValue of Value × Value | invalidValue | Missing Name of string;

51. These are exceptions that are raised by the semantic function when values are inappropriate. ⟨ Type Definitions 2 ⟩+ ≡

exception NotImplemented ;

exception NotCorrect ;

exception NotPair ;

exception NotLValue;

exception NotBool ;

exception NotInteger ;

exception NotFunc;

exception NotFuncDecl ;

52. Here is an version of the Y fix point operator. We could use it for to implement recursion. It would only be a minor change to make the semantic function use this rather than use ’s builtin recursion. ⟨ Functions 52 ⟩ ≡

fun fix f x = f (fix f) x;

See also section 53. This code is used in section 1.

53. The empty continuation. ⟨ Functions 52 ⟩+ ≡

§54 TEST OF THE MACHINE 13

fun nullContinuation x = x; 54. Test of the Machine. Testing is no substitute for correct implementation, but it is somewhat heartwarming to see such an abstract interpreter actually work.

First of all define a test function that will accept any program in the language and execute it, returning the result. ⟨ Test Cases 54 ⟩ ≡

fun test n = let

val (V , S) =

Me n newenv nullContinuation newstore

handle unbound variable x ⇒ (Missing Name x, newstore);

in V end;

See also sections 55, 56, 57, 58, and 59. This code is used in section 1.

55. A few dead simple tests to show that integers and pairs work properly. ⟨ Test Cases 54 ⟩+ ≡

test (Numeral 3); test (Neg (Add (Numeral 3, Numeral 39))); test (Fst (Pair (Numeral 3, Numeral 4))); test (Snd (Pair (Numeral 3, Numeral 4))); test (Seq (Numeral 3, Numeral 4));

56. Test binding names, both through value declarations and λ bindings. Also verify that function abstraction, function application, and call-with-current-continuation work. ⟨ Test Cases 54 ⟩+ ≡

val X = ; val Y = ; val FIX = and F = ; test (Decl (Val Decl (X, Numeral 29), Var X)); test (App (Proc (X, Numeral 17), Numeral 7)); test (App (Proc (X, Add (Var X, Numeral 1)), Numeral 7)); test (Decl (Val Decl (X, Proc (Y , Var Y)), Add (Numeral 3, App (Var X, Numeral 55)))); test (Decl (Val Decl (X, Proc (Y , Seq (App (Var Y , Numeral 33), Numeral 44)))

, Add (Numeral 3, Callcc (Var X))));

57. Now for some real excitement: recursive functions. Surprise! Surprise! They actually work. ⟨ Test Cases 54 ⟩+ ≡

val fact = Rec Decl (X, Proc (Y , Cond (Less (Var Y , Numeral 2)

, Numeral 1, Mult (App (Var X, Add (Var Y , Neg (Numeral 1))), Var Y))));

test (Decl (fact , App (Var X, Numeral 1))); test (Decl (fact , App (Var X, Numeral 5))); 58. Ok, so let’s use some CPU time! Try fibonacci ⟨ Test Cases 54 ⟩+ ≡

val fib = Rec Decl (X, Proc (Y , Cond (Less (Var Y , Numeral 2), Numeral 1, Add (App (Var X, Add (

Var Y , Neg (Numeral 1))), App (Var X, Add (Var Y , Neg (Numeral 2)))))));

test (Decl (fib, App (Var X, Numeral 1))); test (Decl (fib, App (Var X, Numeral 5))); test (Decl (fib, App (Var X, Numeral 10))); test (Decl (fib, App (Var X, Numeral 15))); test (Decl (fib, App (Var X, Numeral 20))); test (Decl (fib, App (Var X, Numeral 25))); test (Decl (fib, App (Var X, Numeral 28)));

59. Finally test that reference bindings and iteration work properly. ⟨ Test Cases 54 ⟩+ ≡

test (Assign (Ref (Numeral 2), Numeral 3)); test (Decl (Var Decl (X, Numeral 1), Deref (Var X))); test (Decl (Var Decl (X, Numeral 1), Seq (Assign (Var X, Add (Numeral 22, Deref (Var X))), Deref (

Var X))));

test (Decl (Var Decl (X, Numeral 1), (Decl (Var Decl (Y , Numeral 0), Seq (While (Less (Deref (Var X), Numeral 11), Seq (Assign (Var Y , Add (Deref (Var Y), Deref (Var X))), ( Assign (Var X, Add (Numeral 1, Deref (Var X)))))), Deref (Var Y)))))); §60 INDEX 15

60. Index.

access : 34, \underline{48}. Add : 37, 38, 55, 56, 57, 58, 59. App: 12, 15, 16, 56, 57, 58. Assign: 35, 36, 59. avail : 48. bind : 10, 11, 12, 14, \underline{47}. bool : 50. boolValue: 26, 30, 44, 46, 50. Callcc: 17, 18, 56. Cond : 25, 26, 57, 58. continuation: 3, 18, \underline{49}, 50. Decl : \underline{2}, 9, 10, 11, 12, 56, 57, 58, 59. Deref : 12, 33, 34, 59. env : 1, 3, 47. Env : 47. E1 : 16, 20, 26, 28, 30, 36, 38, 40, 44. E2 : 16, 20, 26, 28, 30, 36, 38, 40, 44. E3 : 26. fact : \underline{57}. fib: \underline{58}. fix : \underline{52}. FIX : 12, \underline{56}. fixpoint : \underline{12}. Fst : 21, 22, 55. funcValue: 12, 14, 16, 18, 50. intValue: 8, 38, 40, 42, 44, 50. invalidValue: 12, 30, \underline{50}. Less : 43, 44, 57, 58, 59. loc: 48. lookup: 6, \underline{47}. lvalue: \underline{48}, 50. lvalueValue: 10, 12, 32, 34, 36, 50. Me: 1, 3, \underline{6}, \underline{8}, \underline{10}, \underline{11}, \underline{12}, \underline{14}, \underline{16}, \underline{18}, \underline{20}, \underline{22}, \underline{24},

\underline{26}, \underline{28}, \underline{30}, \underline{32}, \underline{34}, \underline{36}, \underline{38}, \underline{40}, \underline{42}, \underline{44}, \underline{46}, 54. Missing Name: 50, 54. Mult : 39, 40, 57. nE : \underline{10}, \underline{12}. Neg : 41, 42, 55, 57, 58. new : 10, 12, 32, \underline{48}. newenv : \underline{47}, 54. newstore: \underline{48}, 54. Not : 45, 46. NotBool : 26, 30, 46, \underline{51}. NotCorrect : \underline{51}. NotFunc: 16, 18, \underline{51}. NotFuncDecl : 12, \underline{51}. NotImplemented : \underline{51}. NotInteger : 38, 40, 42, 44, \underline{51}. NotLValue: 34, 36, \underline{51}.

NotPair : 22, 24, \underline{51}.

nS : \underline{32}.

nullContinuation: \underline{53}, 54.

Numeral : 7, 8, 55, 56, 57, 58, 59.

Pair : 19, 20, 55.

pairValue: 20, 22, 24, 50. Proc: 12, 13, 14, 56, 57, 58. Rec Decl : 2, 12, 57, 58. Ref : 31, 32, 59. segmentation violation: \underline{48}. Seq : 27, 28, 55, 56, 59. Snd : 23, 24, 55. store: 1, 3, 48, 49. Store: 48. Term: 1, 2, 3, 5, 9, 13, 15, 17, 19, 21, 23, 25, 27,

29, 31, 33, 35, 37, 39, 41, 43, 45. test : \underline{54}, 55, 56, 57, 58, 59. T1 : 22, 24. T2 : 22, 24. unbound variable: \underline{47}, 54. update: 12, 36, \underline{48}. Val Decl : 2, 11, 56. Value: 3, 18, \underline{50}. Var : 5, 6, 12, 56, 57, 58, 59. Var Decl : 2, 10, 59. VS : 16. V1 : 20, 38, 40, 44. V2 : 20, 38, 40, 44. While: 29, 30, 59.

§60 NAMES OF THE SECTIONS 16

⟨ Functions 52, 53 ⟩ Used in section 1. ⟨ Meaning Function 6, 8, 10, 11, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38, 40, 42, 44, 46 ⟩ Used in section 1. ⟨ Term Definition 5, 7, 9, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35, 37, 39, 41, 43, 45 ⟩ Used in section 2. ⟨ Test Cases 54, 55, 56, 57, 58, 59 ⟩ Used in section 1. ⟨ Type Definitions 2, 47, 48, 49, 50, 51 ⟩ Used in section 1.

Denotional Semantics and an ML Interpreter for a Functional Programming Language

for CS742, Dominic Duggan

Table of Contents

Section Page

Denotational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1 Term and Me . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3 Function operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4 Operations on Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 5 Flow of control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6 Storage References and Updates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 7 Integer Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 8 Boolean Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 9 Environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 10 Stores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 11 Values and Miscellaneous Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 12 Test of the Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 13 Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 15

                       \begin{matrix}c \\ ◯ \end{matrix} 1991, Dave Mason <dmason@plg.uwaterloo.ca>