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_1.
- 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_1&E_2) holds assuming that P(E_1) holds and P(E_2)
holds (for arbitrary E_1, E_2).
Syntax rules guide the proof!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: core.tex,v 1.3 1996/02/05 10:34:52 schreine Exp schreine