Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:proofs_and_induction [2008/02/21 17:47] vkuncak |
sav08:proofs_and_induction [2008/02/21 17:50] vkuncak |
||
---|---|---|---|
Line 182: | Line 182: | ||
{\forall n \in \mathbb{N}. P(n)} | {\forall n \in \mathbb{N}. P(n)} | ||
\] | \] | ||
- | |||
==== Structural Induction ===== | ==== Structural Induction ===== | ||
+ | |||
+ | Stepwise induction allows us to prove properties of natural numbers by proving that it holds for 0 and that it extends with each successor. Structural induction similarly allows us to prove that if property holds for basic structures and that if it holds for smaller structures then it also holds for larger structures. Examples of such structures are terms or expression trees. | ||
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. | 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. | ||
Line 191: | Line 192: | ||
{\forall t \in {\it Terms}(L). P(t)} | {\forall t \in {\it Terms}(L). P(t)} | ||
\] | \] | ||
+ | Note that if $c$ is a constant we assume $ar(c)=0$. Therefore, structural induction requires us to prove $P(c)$ for all constants $c \in L$. | ||
* [[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) |