Go backward to Induction and Recursion Go up to Top Go forward to Unicity of Typing

Structural Induction

• Proof technique for syntax trees.
  • Goal: prove P(t) for all trees t in a a language.
  • Inductive base: Prove that P holds for all trees in stage₁.
  • Inductive hypothesis: Assume that P holds for all trees in stages stage_j with j <= i.
  • Inductive step: Prove that P holds for all trees in stage_i.
• Prove P(t) for all trees t in Expression.
  • P(true) holds.
  • P(not E) holds assuming that P(E) holds (for arbitrary E).
  • P(E₁&E₂) holds assuming that P(E₁) holds and P(E₂) holds (for arbitrary E₁, E₂).

Syntax rules guide the proof!