may find the programming style used here rather unusual. For readers not introduced to these languages, some very brief explanations are given in the codes’ presentation. But almost all features of OCaml and Python will be considered either in this first volume or in the second, where object-oriented programming is considered. We hope that these two encodings of formal notions can help readers who are not truly familiar with mathematical formalism.
2.1. Environment, memory and state
2.1.1. Evaluation environment
Let X be a set of identifiers and V a set of values. The association of an identifier x ∈ X with a value v ∈ V is called a binding (of the identifier to its value), and a set Env of bindings is called an execution environment or evaluation environment. Env(x) denotes the value associated with the identifier x in Env. The set of environments is denoted as E.
In practice, the set of identifiers X that are actually used is finite: usually, we only consider those identifiers that appear in a program. An environment may thus be represented by a list of bindings, also called Env:
where {x1 ,x2, . . ., xn} denotes a finite subset of X, known as the domain of the environment and denoted as dom(Env). By convention, Env(x) denotes the value v, which appears in the first (x, v) binding encountered when reading the list Env from the head (here, from left to right).
In this model, a binding can be added to an environment using the operator ⊕. By convention, bindings are added at (the left of) the head of the list representing the environment:
Suppose that a certain operation introduces a new binding of an identifier, which is already present in the environment, for example (x2, vnew):
The so-obtained environment (x2,vnew) ⊕ Env contains two bindings for x2. Searching for a binding starts at the head of the environment, and, with our convention, new bindings are added at the head. So the most recent addition, (x2,vnew), will be the first found. The binding (x2, v2) is not deleted, but it is said to be masked by the new binding (x2, vnew). Several bindings for a single identifier x may therefore exist within the same environment, and the last binding added for x will be used to determine the associated value of x in the environment. Formally, the environment (x, v) ⊕ Env verifies the following property:
By convention, the notation (x2,v2) ⊕ (x1 ,v1) ⊕ Env is used to denote the environment (x2,v2) ⊕ ((x1,v1) ⊕ Env). For example, ((x,v2) ⊕ (x,v1) ⊕Env)(x) = v2
When an environment is represented by a list of bindings, the value Env(x) is found as follows:
Python def valeur_de(env,x): for (x1,v1) in env: if x==x1: return v1 return NoneOCaml let rec valeur_de env x = match env with | [] -> None | (x1, v1) :: t -> if x = x1 then Some v1 else (valeur_de t x) val valeur_de: (‘a * ‘b) list -> ‘a -> ‘b option
If no binding can be found in the environment for a given identifier, this function returns a special value indicating the absence of a binding. In Python, the constant None is used to express this absence of value, while in OCaml, the predefined sum type ’a option is used:
OCaml type ’a option = Some of ’a | None
The values of the type ’a option are either those of the type ’a or the constant None. The transformation of a value v of type ’a into a value of type ’a option is done by applying the constructor Some to v (see Chapter 5). The value None serves to denote the absence of value of type ’a; more precisely, None is a constant that is not a value of type ’a. This type ’a option will be used further to denote some kind of meaningless or absent values but that are needed to fully complete some definitions.
The domain of an environment can be computed simply by traversing the list that represents it. A finite set is defined here as the list of all elements with no repetitions.
Python def union_singleton(e,l): if e in l: return l else: return [e]+l def dom_env(env): r=[] for (x,v) in env: r = union_singleton(x,r) return rOCaml let rec union_singleton e l = if (List.mem e l then l else e::l val union_singleton : ’a -> ’a list -> ’a list let rec dom_env env = match env with | [] -> [] I (x, v) :: t -> (union_singleton x (dom_env t)) val dom_env : (’a * ’b) list -> ’a list
Since the value returned by the function valeur_de is obtained by traversing the list from its head, adding a new binding (x, v) to an environment is done at the head of the list and the previous bindings of x (if any) are masked, but not deleted.
Python def ajout_liaison_env(env,x,v): return [(x,v)]+envOCaml let ajout_liaison_env env x v = (x, v) :: env val ajout_liaison_env : (’a * ’b) list -> ’a -> ’b -> (’a * ’b) list
2.1.2. Memory
The formal model of the memory presented below makes no distinction between the different varieties of physical memory described in Chapter 1. The state of the memory is described by associating a value with the location of the cell in which it is stored. The locations themselves are considered as values, called references. As we have seen, high-level languages allow us to name a location c, containing a value v, by an identifier x bound to the reference r of c.
Let R be a set of references and V a set of values. The association of a reference r ∈ R with a value v ∈ V is represented by a pair (r, v), and a set Mem of such pairs is called here a memory. Mem(r) denotes the value stored at the reference r in Mem. Let M be the set of memories. In practice, the set of references, which is actually used, is finite: once again, only those locations used by a program are generally considered. This means that the memory can be represented by a list, also called Mem:
The existence of a pair (r, v) in a memory records that an initialization or a writing operation has been carried out at this location. Every referenced memory cell may be consulted through reading and can be assigned a new value by writing. In this case, the value previously held in the cell is deleted, it has “crashed”.
Writing a value v at an address r transforms a memory Mem into a memory denoted as Mem[r := v]; if a value was stored at this location r in Mem, then this
