Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:proofs_and_induction [2008/02/21 17:25] vkuncak |
sav08:proofs_and_induction [2008/02/21 17:47] vkuncak |
||
|---|---|---|---|
| Line 185: | Line 185: | ||
| ==== Structural Induction ===== | ==== Structural Induction ===== | ||
| + | |||
| + | Consider a language $L$ of function symbols. Let $ar(f)$ denote the number of arguments (arity) of a function symbol $f \in L$. Let ${\it Terms}(L)$ denote the set of all terms in this language. To prove a property for all terms, we show that if the property holds for subterms, then it holds for the term built from these subterms. | ||
| + | \[ | ||
| + | \frac{\bigwedge_{f \in L} \forall t_1,\ldots,t_{ar(f)}.\ (\bigwedge_{i=1}^{ar(f)} P(t_i)) \rightarrow P(f(t_1,\ldots,t_n))} | ||
| + | {\forall t \in {\it Terms}(L). P(t)} | ||
| + | \] | ||
| + | |||
| * [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now) | * [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now) | ||