# 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