Notes on Recursion and Induction principles

 


Notes on Recursion and Induction principles

Recursion is the basis of the computational and expressive power of functional programming languages.
Its working principle is analogous to that used in mathematical proofs by induction.
In fact, in a recursive program the output is defined for the base elements and then, assuming the program correctly works for "simpler", "smaller" elements than the input, the output is defined for the generic input.
The main problem is to understand, for each particular function, what it is intended for "smaller"; this is a notion that varies from case to case and it is essential for a correct use of the recursion mechanism.
We have seen in Notes on Recursion how recursion works and how it is intuitively possible to understand whether a function is correctly defined and whether it terminates.
We have seen in Notes on well founded sets how it is possible to use the notion of well-founded set to precisely formalize for each recursive definition of a function the intuitive notion of "smaller" that we unconsciously use in defining that function.
But this is not enough in case we wish to prove, in a really formal and precise way, that a function computes what it is intend to compute or that a function satisfies some particular property. If we wish to do that, we need to use formal logical tools: the induction principles, be it the usual mathematical induction principle (or its slight generalization, the complete induction) or the very general well-founded induction principle.
Such induction principles are defined and widely discussed in [VS]: Induzione matematica e funzioni ricorsive. You can find in Solutions the solutions of the exercises proposed in [VS]. Such exercises will help you to practice on how to prove properties of function definitions by means of the induction principles.

The present notes contain a brief additional discussion, with examples, on how these principles are related to the definition of recursive functions, and on how they can be used to prove properties of functional programs.
This discussion and examples can be used to introduce and "integrate" the material present in [VS].



Principle of induction and Principle of complete induction

Study in [VS] the principle of mathematical induction
You can notice tha the principle of mathematical induction is a logical rule that implicitely "expresses" also a model of calculation. It corresponds in functional programming to defining numerical functions by recursion like the following one: 

 (define (fact n) 
     (if (= n 0) 
         1 
         (* n (fact (- n 1)))))

the value of the function is given for n=0 and is calculated for n assuming that fact correctly works for n-1.

NOTE: Not all the logical rules, like the principle of induction, posses a constructive, computational, meaning.
For example, to prove that "There exists x such that P(x)" we could use the logical rule of the elimination of the double negation (proof by contradiction): we assume that "It does not exist any x such that P(x) holds" and if from this assumption we get to an absurdity, a contradiction, we can safely infer (in classic logic) that "There exists x such that P(x)".
A proof by contradiction, however, does not give me the actual x for which P(x) holds, we just know that it exists; the rule does not have any "constructive", computational meaning.

The close correspondence betweeen recursive functions and the principles of induction, can be helpful, for example, to use induction to formally prove properties of recursive programs.
It is natural to use the principle of mathematical induction if we wish to show that the factorial is total, i.e. that for all n (fact n) converges
We need:
1. to prove that (fact 0) converges
2. to prove that, for a generic k not equal to 0, (fact k) converges, using the inductive hypothesis that (fact (- k 1)) converges).

Let's consider the definition of factorial given above and let's prove the two points above:
1. if k=0 you evaluate the "then" part of the conditional, therefore the value of the expression that represents the factorial is 1, that is (fact 0) converges ;
2. if k >0 you evaluate the "else" part, hence the value of (fact k) is the value of the expression (* k (fact (- k 1))). Hence, by assuming that the evaluation of (fact (- k 1)) converges, the evaluation of whole expression (* k (fact (- k 1))) trivially converges.


Let's consider now a slightly different type of recursion taking as example the following Scheme function even: 

(define (even? x) 
    (cond ((= x 0) #t) 
          ((= x 1) #f) 
          (else (even? (- x 2)))))

If I want to show a property of this program I do not use the principle of induction but the principle of complete induction, because this way of doing recursion can be considered as the computational counterpart of the principle of complete induction.
In a nutshell, the principle of complete induction uses a stronger hypothesis in comparison to the principle of induction:

- principle of induction: we prove phi(0) and then prove phi(n) assuming that phi(n-1) holds.
- principle of complete induction: we prove phi(0) and then prove phi(n) assuming that phi holds for all the values smaller than n.



Principle of well-founded induction

Study the principle of well-founded induction in [VS].

Notation: We shall use the notation "$x.P(x)" to denote "for all x.P(x)".

We notice that the principle of well-founded induction can be stated in a slightly different and more intuitive way: Let (S,<) be a well-founded set and let M be the set of its minimal elements 

   $x in M. phi(x)       $x not in M.(($y<x. phi(y) ) => phi(x)) 
 ------------------------------------------------------------------ 
                           $x in S. phi(x)

By presenting in this way the principle of well-founded induction, we distinguish between minimal and not minimal elements in S.
For the minimal ones there is no need to use the inductive hypothesis "$y<x. phi(y)" because, when x is minimal, it is always false.
This formulation of the principle of well-founded induction makes it similar to the principle of complete induction and it is often simpler to use.
The principle of well-founded induction allows us to show properties of programs that works on complex domains, not just natural numbers.
To use it correctly we need:
- to understand what is the domain of the function;
- to understand what is the precedence relation induced by the recursion;
- to be sure that this set, with this relation, is well-founded.
It sometimes happens that after having written a recursive program we realize that it does not correctly work or it enters in an endless loop.
This is often due to the fact that the domain of the function is not well founded w.r.t the relation considered. For example, a frequent error in programs on the natural numbers is writing in an incorrect way the base case; this can cause the program to be called endlessly on negative numbers. If this happens, it means that, instead of (N, <), we have implicitly considered (Z,<), which is not well-founded, as domain.

We consider now functions with two or more arguments. When a function takes in input more argumentAs the domain of the function is a cartesian product.
In case of a function that takes a number and a list, if we wish to show that it is a total function we have to find a well-founded relation on the set of the pairs (number,list).
Given two well-founded sets, (S1, <1) and (S2, <2), We can define various well-founded precedence relations on the product set: the product precedence relation and the lexicographic precedence (see [VS] for their definitions).
Often, if the domain is a product of two domains and the relation of precedence is the lexicographic one, you can say that the primary recursion is on the first domain and the secondary one is on the second domain.


We present now a few Scheme functions we have already seen in Notes on Higher Order Functions in Scheme and use the induction principles to prove some of their properties. 

(define (Ftoria F g n) 
       (if (= n 1) 
           (g 1) 
           (F (g n) (Ftoria F g (- n 1)))))

We show now that, if F and g are total, also the function F-toria is total.

The domain of F-toria is given by the Cartesian product of

  • (NxN) -> N the set of the binary functions on natural numbers
  • N -> N the set of the unary functions on natural numbers
  • N\{0} the set of the natural numbers except zero Hence the domain of F-toria is the set ((NxN) -> N) x (N -> N) x (N\{0})
    On this set the induced precedence relation, '<<', having minimal elements of the form (F, g, 1), is the following one:
    (H, h, n-1)  <<   (G, g, n)
    Of course we can also consider the following larger (and simpler) precedence relation:
    (H, h, n-1)  <<   (G, g, n)    iff     n <k.
    with minimal elements still of the form (F, g, 1).
    In both case the relation '<<' is trivially well-founded, so we can use the well-founded induction:
  • If the argument is a minimal triple, the result is (g 1) (recall that we assumed g to be total)l function.
  • If the triple is not minimal, the value of the function is given by the expression (F (g n) (Ftoria F g (- n 1))), whose evaluation always terminates because F and g were assumed to be total and because the evaluation of (Ftoria F g (- n 1)) terminates by the induction hypothesis, since (F, g, n-1) << (F, g, n).



    Let us consider another example: the function ChangeVal 

     (define (ChangeVal f n m) 
     (lambda (x) 
         (if (= x n) 
             m 
             (f x))))

    It returns a function identical to f but for one input, n, on which it returns m and not (f n).
    example:
    ((ChangeVal fact 3 9) 2) = 2
    ((ChangeVal fact 3 9) 3) = 9

    ChangeVal is trivially total.

    We now use ChangeVal inside the following function funz (we do not know what funz computes): which we assume working on functions from naturals to naturals, and on naturals. 

    (define (funz f n) 
    (if (= (f 53) 0) 
        (* (+ 1 2) 5) 
        (+ 7 (funz (ChangeVal f 53 (- (f 53) 1)) n))))

    Despite it is not clear what funz computes, it is however possible to prove that it is total, that is that the recursion terminates on any element of the domain of the function.
    Then the property we wish to prove is

    $ f,n.(funz f n) converges

    We need to identify what is the domain of funz, what is the precedence relation induced by the recursive definition of funz (or a larger one if easier to handle) and prove it well-founded.

    The domain of funz is the Cartesian product of the set of the total functions on the natural numbers and the set N of the natural numbers . The induced precedence relation is the following one

    (h,n)  <<  (g,m)      iff      h(53)  <  g(53)

    This relation is well founded. In fact we cannot have an endless chain of the form

    .... (f3, n3) << (f2, n2) << (f1, n1) << (f0, n0)

    since it would be an endless chain of natural numbers (impossible).

    The minimal elements for this relation are all the pairs (f,n) such that f(53) = 0 (for es. (lambda x) 0), 71))

    We proceed now to prove funz to be total using the principle of well founded induction:

  • If the input pair is a minimal element the value of funz is given by the expression (* (+ 1 2) 5), whose evaluation undoubtly terminates.
  • If we do not have a minimal pair as input, the value of funz is given by the expression (+ 7 (funz ((ChangeVal f 53 (- (f 53) 1)) n))). We notice that in this expression funz is called recursively on value given by the expression ((ChangeVal f 53 (- (f 53) 1)) n), and on n.
    We have also that
    ( ((ChangeVal f 53 (- (f 53) 1)) 53), n) << ((f 53),n)
    since ((ChangeVal f 53 (- (f 53) 1)) 53) = (- (f 53) 1).
    So, by the induction hypothesis, the evaluation of (funz ((ChangeVal f 53 (- (f 53) 1)) n)) terminates and therefore the evaluation of (+ 7 (funz ((ChangeVal f 53 (- (f 53) 1)) n))) terminates.
    We can now apply the logical rule of well-founded induction, obtaining that
    $ f,n.(funz f n) converges



    Another exercise: consider the following function "guess". 

    (define (guess what is) 
    (if (null? is)  
        '() 
        (cons (cond 
                 ((not (number? (car is))) 
		         (guess what (car is))) 
                 ((what (car is)) 0) 
                 (else  (car is))) 
	      (guess what (cdr is)))))

    What does guess computes? Formally prove it by induction.

    What we can say first is that guess is a function with two arguments.
    Inside the body the argument "is" is applied to the predicate "null?" and to the function "car", therefore it is a list (since these are functions that work on lists).
    We can also say that "is" is a list of lists with arbitrary level of nestings, since in the recursive call (car is) is given as second argument of guess, and this means that also the head of "is" can be a list.
    What are the atomic elements of the list "is"? Well, natural numbers, since we apply (car is) to the predicate "number?".
    "what", instead, is a predicate. This can be inferred by the fact that it is present in one of the boolean expressions in the cond cases.
    So guess is a function that takes a predicate and a list with arbitrary level of nestings, with natural numbers as atomic elements, and returns a list (in fact the basic case returns the empty list and the recursive case returns the "cons" of something).
    The output list has the same number of atomic elements of the input one, since no element is ever discarded, something is simply done on every element of the list.
    We can evaluate guess on an example to better understand what it does.
    We first define a predicate on numbers 

     (define (H? n) 
     (= n 3))

    and then we evaluate the expression 

     (guess H? ((2 3) 5))

    The evaluation of this expression informally goes on as follow. 

    (cons (guess H? (2 3)) (guess H? (5))) 

(cons (cons 2 (guess H? (3))) (guess H? (5))) 

(cons (cons 2 (0)) (guess H? (5))) 

(cons (cons 2 (0)) (5)) 

((2 0) 5)

    We notice the recursion is on lists since we have recursive calls like (guess what (car is)) and (guess what (cdr is)).
    What is the precedence relation induced by the program guess?

    ls << ls'    iff    ls has a smaller nesting level than ls' or, in case they have the same nesting level, the number of numerical elements and empty lists is smaller.

    This precedence relation is well-founded since it is a lexicographical one on two well-founded precedence relations, i.e.

    <<   =   <lex (<', <'')

    where   ls  <'  ls'    iff   nest(ls)  <  nest(ls') (where nest(l) is the nesting level of the list l)
    and   ls  <'' ls'    iff   #(ls)  < #(ls') (where #(l) is the number of natural numbers and empty lists present in l)

    We now prove by well-founded induction that, if we denote by S the domain of guess, $ls in S.P(ls) holds, where
    P(ls)  =   (guess ls) returns ls where any element el such that (what el) is true is replaced by 0

  • Basic case
    The only minimal element of S is '():
    (guess what '()) = '(). Then P holds on the minimal elements of S.
  • Inductive step
    We consider the generic element "is" and assume that P holds for all the elements preceding it.
    Then, by the induction hypothesis, we have that (guess (car is)) and (guess (cdr is) return lists similar to the arguments but for the numbers verifying the predicate, replaced by 0.
    It is easy now to check that (guess is) produces the right list.
    We have then verified all the premises and we can apply the principle of well-founded induction to infer that $ls in S.P(ls) holds.

    •