LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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)