Denotational Semantics

Example: language with function calls

Now we complicate things even more...

Syntactic Categories

```  I in Ident  (identifiers)
L in Lexp   (l-expressions, or references)
E in Exp    (expressions, commands)
P in Prog   (full programs)
```
Syntax BNF
```   L  ::=  I
E  ::=  0 | 1 | I | !L | E1; E2 | (E1 + E2)
|  let I = E1 in E2 end
|  new I := E1 in E2 end
|  L := E
|  if E1 then E2 else E3
|  while E1 do E2
|  function I1 (I2) = E1 in E2 end
|  call I (E)
P  ::=  program (I) ; E end .
```
Value Domains
```       n in Int = { ..., -2, -1, 0, 1, 2, ... }         (integers)
alpha in Loc                                         (no structure details...)
sigma in States = Loc --> Int U {unused}             (states, of memory)
f in Func = States --> Int --> (Int * States)
rho in Env = Ident --> Int U Loc U Func U {undef}
```
Semantic Functions
```   LL : Lexp --> Env --> States --> Loc
MM : Exp --> Env --> States --> (Int * States)
PP : Prog --> Int --> Int
```
Semantic Equations
```   (* include all from previous example   *)
(* plus these new ones                 *)

MM [ function I1 (I2) = E1 in E2 end ] rho sigma =
let f sigma' n = MM [E1] rho[I2 |-> n] sigma'
in  MM [E2] rho[I1 |-> f] sigma
end

(* environment for function eval is bound at definition time *)

MM [ call I (E) ] rho sigma =
let (n,sigma') = MM [E] rho sigma
f = rho(I)
in  f sigma' n
end

```