Concepts and Semantics of Programming Languages 1. Therese Hardin

Чтение книги онлайн.

      By convention, the notation (x₂,v₂) ⊕ (x₁ ,v₁) ⊕ Env is used to denote the environment (x₂,v₂) ⊕ ((x₁,v₁) ⊕ Env). For example, ((x,v₂) ⊕ (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: