Denotational Semantics



Example: language of propositional logic

Syntactic Categories
  P in Prop  (propositions)
  F in Form  (formulae)
Syntax BNF
   F  ::=  P  |  ~ F  |  F ==> F
Value Domains
          Bool = { true, false }      boolean logic values
   rho in Assign = P --> Bool         truth assignments
Semantic Functions
   MM :  Form  --> Assign -->  Bool
     means MM mapps a formula and an assignment into a boolean value
     the assignment tells the truth values of atomic propositions
Semantic Equations
   MM [P] rho  =  rho(P) 
   MM [~F] rho  =  ~ MM [F] rho
   MM [F1 ==> F2] rho  =  ~ MM [F1] rho  v  MM [F2] rho