Denotational Semantics



Example: language with Main Program and Error values

Now we complicate things by making them more realistic...
Let's look at a language where the functions produce either integers or "error" for problems.
We also introduce a more useful meta-language for expression functions.

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]
     end

Any meta-language for expressing functions will do... remember the lisp-cons-like notation from Mills' method?