Syntactic Categories
I in Ident (identifiers) E in Exp (expressions) P in Prog (full programs)Syntax BNF
E ::= 0 | 1 | I | (E1 + E2) | (E1 / E2) | if E1 then E2 else E3 | let I = E1 in E2 end P ::= program (I) ; E end .Value Domains
Int = { ..., -2, -1, 0, 1, 2, ... } (integers) rho in Env = Ident --> Int U {undef} (environments)Semantic Functions
EE : Exp --> Env --> Int U {err} PP : Prog --> Int --> Int U {err}Semantic Equations
EE [0] rho = 0 EE [1] rho = 1 EE [I] rho = ite(isInt(rho(I)), rho(I), err) EE [E1 + E2] rho = let n = EE [E1] rho ; n' = EE [E2] rho in ite(isInt(n) and isInt(n'), plus(n,n'), err) end EE [E1 / E2] rho = let n = EE [E1] rho ; n' = EE [E2] rho in if isInt(n) andalso isInt(n') andalso n' != 0 then div(n,n') else err end EE [ if E1 then E2 else E3 ] rho = let n = EE [E1] rho in if isInt(n) then if n=0 then EE [E2] rho else EE [E3] rho else err end EE [[ let I = E1 in E2 end ]] rho = let n = EE [E1] rho in if isInt(n) then EE [[ E2 ]] rho[I |-> n] else err end PP [[ program (I); E end. ]] n = let fun rho(J) = undef in EE [[ E ]] rho[I |-> n] endAny meta-language for expressing functions will do... remember the lisp-cons-like notation from Mills' method?