Go backward to Programs are Functions Go up to Top

Program Denotation

Z:=1;

if A=0 then diverge;

Z:=3.

V P

lambdan.(n equals zero) -> _|_ [] three

• Denotation extracts essence of a program.
• Store disappears

  Temporary data structure; not contained in the input/output relation of a program.

• Transformation resembles compilation.
• Simplification resembles optimization.