Concepts and Semantics of Programming Languages 1. Therese Hardin

:= v₂].

      For example, (Mem[r1:= v1 ][r₂:= v₂])(r) = v₂.

      The function valeur_ref computes the value stored at a given location. If nothing has previously been written at this location, the function returns a special value (None), indicating the absence of a known value (i.e. a value resulting from initialization or computation).

Python def valeur_ref(mem,a): if len(mem) == 0: return None else: a1,v1 = mem[0] if a == al: return v1 else: return valeur_ref(mem[1:],a)OCaml let rec valeur_ref mem a = match mem with | [] -> None | (a1, v1) :: t -> if a = a1 then Some v1 els (valeur_ref t a) val valeur_ref : (’a * ’b) list -> ’a -> ’b option

      The following function writes a value into the memory:

      Python def write_mem(mem,a,v): if len(mem) == 0: return [(a,v)] else: a1,v1 = mem[0] if a == a1: return [(a1,v)] + mem[1:] else: return [(a1,v1)] + write_mem(mem[1:],a,v)OCaml let rec write_mem mem a v = match mem with | [] -> [(a, v)] | (a1, v1) :: t -> if a = a1 then (a1, v) :: t else (a1, v1) :: (write_mem t a v) val write_mem : (’a * ’b) list -> ’a -> ’b -> (’a * ’b) list

2.1.3. State

      A state is defined as a pair (Env, Mem) ∈ E × M such that any reference in the domain of Mem is accessible from a binding in Env. A reference is said to be accessible if its value can be read or written from an identifier contained in Env by a series of operations of reading, writing, or reference manipulation.

      Given an environment Env, the set of identifiers X is partitioned into two subsets: which contains the identifiers bound to a reference, and , which contains the others:

      The value associated with an identifier x in is a reference Env(x) = r where a value Mem(r) is stored, which can be modified by writing. Identifiers of are generally called mutable variables.

2.2. Evaluation of expressions

      The value of an expression is computed according to an evaluation environment and a memory, i.e. in a given state. This computation is defined by the evaluation semantics of the expression.

      2.2.1. Syntax

The language of expressions Exp₁ used here will be extended in Chapters 3 and 4. Its syntax is defined in Table 2.1.

Table 2.1. Language of expressions Exp₁

e ::= k	Integer constant	(k ∈ ℤ)
| x	Identifier	(x ∈ X)
| e1 + e2	Addition	(e1, e2 ∈ Exp1)
| !x	Dereferencing	(x ∈ X)

      Thus, an expression e ∈ Exp₁ is either an integer constant k ∈ ℤ, an identifier x ∈ X, an expression obtained by applying an addition operator to two expressions in Exp₁ or an expression of the form !x denoting the value stored in the memory at the location bound to the mutable variable x. Thus, this is an inductive definition of the set Exp₁. Note that Exp₁ does not include an assignment construct. This is a deliberate choice. This point will be discussed in greater detail in section 2.3 by means of an extension of Exp₁.

      NOTE. – The symbol + used in defining the syntax of expressions does not denote the integer addition operator. It could be replaced by any other symbol (for example ⊠). Its meaning will be assigned by the evaluation semantics. The same is true of the constant symbols: for example, the symbol 4 may be interpreted as a natural integer, a relative integer or a character.

      EXAMPLE 2.1.– !x + y is an expression of Exp₁ in the same way as (x + 2) + 3. Parentheses are used here to structure the expression, they are part of the so-called concrete syntax and will disappear in the AST.

The set Exp₁ of well-formed expressions of the language is defined by induction and expressed directly by a recursive sum type. Types of this kind can be constructed in OCaml, but not in Python; in the latter case, they can be partially simulated by defining a class for each sum-type constructor. Each class must contain a method with arguments corresponding exactly to the arguments of the sum type constructors it implements. An implementation of this type in Python is naive, and users must ensure that these classes are used correctly. We know that there are possibilities of programming dynamic type verification mechanisms in Python, which simulate strongtyping (similar to that used in OCaml) and ensure that the code is used correctly; however, these techniques lie outside of the scope of this book. The objective of all implementations shown in this book is simply to illustrate and intuitively justify the correct handling of concepts. As we have already done, we choose this approach to implement sum types.

      Using Python, we define the following classes to represent the constructors of the set Exp1:

      Python class Cstel: def __init__(self,cste): self.cste = cste class Var1: def __init__(self,symb): self.symb = symb class Plusl: def __init__(self,exp1,exp2): self.exp1 = exp1 self.exp2 = exp2 class Bang1: def __init__(self,symb): self.symb = symb

      For example, the expression e₁ = !x + y defined in example 2.1 is written as:

      Python ex_expl = Plusl(Bangl(“x”),Varl(“y”))

      Using OCaml, the type of arithmetic expressions is defined directly as:

      OCaml type ’a exp1 = Cstel of int | Var1 of ’a | Plusl of ’a expl * ’a expl | Bangl of ’a

      Values of this type are thus obtained using either the Cste1 constructor applied to an integer value, in which case they correspond to a constant expression, or using the Var1 constructor applied to a value of type ’a, corresponding to the type used to represent identifiers (the type ’a exp1 is thus polymorphic, as it depends on another type), or by applying the Plus1 constructor to two values of the type ’a expl, or by applying the Bang1 constructor to a value of type ’a. For example, the expression e₁ = !x + y is written as:

      OCaml let ex_exp1 = Plus1 (Bang1 (“x”), Var1 (“y”)) val ex_exp1 : string exp1

      2.2.2.