Zero < Succ undefined  Note: same as Zero < Succ __ = True  by the 2nd equation defining order And Succ (Succ __ ) is an element of Nat: Succ Zero < Succ (Succ undefined)  Note: same as Zero < Succ (Succ __ ) = Zero < Succ undefined  by the 4th equation defining order = True  by the 2nd equation defining order And Succ (Succ (Succ __ ) is an element of Nat, and so forth. So the list of elements in Nat expands: ..., Succ (Succ (Succ __ )), Succ (Succ __ ), Succ __, __, Zero, Succ Zero, Succ (Succ Zero), Succ (Succ (Succ Zero)), ... One can interpret the extra values in the following way: __ corresponds to the natural number about which there is absolutely no information Succ __ to the natural number about which the only information is that it is greater than Zero Succ (Succ __ ) to the natural number about which the only information is that it is greater than Succ Zero And so on There is one further value of Nat, namely the "infinite" number: Succ (Succ (Succ (Succ ...))) It can be defined by this function: infinity :: Nat infinity = Succ infinity It is different from all the other Nat values because it is the only number for which Succ m < infinity for all finite numbers m: Zero < infinity = True Succ Zero < infinity = True Succ (Succ Zero) < infinity = True Thus, the values of Nat can be divided into three classes:  The finite values, Zero, Succ Zero, Succ (Succ Zero), and so on.  The partial values, __, Succ __, Succ (Succ __ ), and so on.  The infinite value. Important: the values of *every* recursive data type can be divided into three classes:  The finite values of the data type.  The partial values, __, and so on.  The infinite values. Although the infinite Nat value is not of much use, the same is not true of the infinite values of other data types. Recap: We have discussed two aspects of the holy trinity of functional programming: recursive data types and recursively defined functions over those data types. The third aspect is induction, which is discussed now. Induction allows us to reason about the properties of recursively defined functions over a recursive data type. In the case of Nat the principle of induction can be stated as follows: in order to show that some property P(n) holds for each finite number n of Nat, it is sufficient to treat two cases: Case (Zero). Show that P(Zero) holds. Case (Succ n). Show that if P(n) holds, then P(Succ n) also holds. As an example, let us prove this property (the identity for addition): Zero + n = n Before proving this, recall that + is defined by these two equations: m + Zero = m m + Succ n = Succ(m + n) Proof: The proof is by induction on n. Case (Zero). Substitute Zero for n in the equation Zero + n = n. So we have to show that Zero + Zero = Zero, which is immediate from the first equation defining +. Case (Succ n). Assume P(n) holds; that is, assume Zero + n = n holds. This equation is referred to as the induction hypothesis. We have to show that P(Succ n) holds; that is, show that Zero + Succ n = Succ n holds. We do so by simplifying the lefthand expression: Zero + Succ n = Succ (Zero + n)  by the 2nd equation defining + = Succ (n)  by the induction hypothesis We have proven the two cases and so we have proven that Zero + n = n holds for all finite numbers of Nat. Full Induction. To prove that a property P holds not only for finite members of Nat, but also for every partial (undefined) number, then we have to prove three things: Case ( __ ). Show that P( __ ) holds. Case (Zero). Show that P(Zero) holds. Case (Succ n). Show that if P(n) holds, then P(Succ n) holds also. To just prove that a property P holds for every partial (undefined) number, then we omit the second case. To illustrate proving a property that holds for every partial number (not for the finite numbers), let us prove the rather counterintuitive result that m + n = n for all numbers m and all partial numbers n. For easy reference, we repeat the definition of + m + Zero = m m + Succ n = Succ(m + n) Proof: The proof is by partial number induction on n. Case ( __ ). Substitute __ for n in the equation m + n = n. So we have to show that m + __ = __, which is true since __ does not match either of the patterns in the definition of +. Case (Succ n). We assume P(n) holds; that is, assume m + n = n holds. This equation is the induction hypothesis. We have to show that P(Succ n) holds; that is, show that m + Succ n = Succ n holds. For the lefthand side we reason m + Succ n = Succ(m + n)  by the second equation for + = Succ(n)  by the induction hypothesis Since the righthand side is also Succ n, we are done. The omitted case (m + Zero = Zero) is false, which is why the property does not hold for finite numbers. As an added bonus, having proved that an equation holds for all partial (undefined) numbers, we can assert that it holds for the infinite number too; that is, P(infinity) holds. Thus, we can now assert that m + infinity = infinity for all numbers m.
Current Thread 


< Previous  Index  Next > 

Re: [xsl] Metadata Stamping, Mandar Jagtap  Thread  [xsl] [ANN] XML Amsterdam 2012 regi, XML Amsterdam 
Re: [xsl] Pattern Matching in XSl , Wendell Piez  Date  RE: [xsl] Pattern Matching in XSl , Kerry, Richard 
Month 
This website was created & generated with <oXygen/>^{®}XML Editor