Go backward to Fixed Point Semantics Go up to Top

Substitution Principles

• E[[LET I = E₁ IN E₂]] = E[[ [E₁/I]E₂ ]]

  LET X = a₀ IN
      LET Y = X CONS NIL IN
          (HEAD Y) CONS X CONS NIL
  => LET Y = a₀ CONS NIL IN
      (HEAD Y) CONS a₀ CONS NIL
  => (HEAD (a₀ CONS NIL)) CONS a₀ CONS NIL
  => a₀ CONS a₀ CONS NIL

• E[[LETREC I = E₁ IN E₂]] = ?
  • Substitute [[E₁]] for [[I]] in [[E₂]].
  • Substitute [[E₁]] for [[I]] in resulting expression.
  • Continue until occurences of [[I]] eliminated.
  • Number of substitutions is unbounded!
  • Substitute occurences only when required for further simplification!

Computation is substitution; in implementation environment becomes run-time structure.