Re: Response to Karen and to Willem on recursive proofs

From: Edward G. Nilges (spinoza1111_at_yahoo.com)
Date: 01/21/04 

Date: 20 Jan 2004 17:17:27 -0800

Willem <willem@stack.nl> wrote in message news:<slrnc0qe1m.6nc.willem@toad.stack.nl>...

I have skipped over the working set of trolls including Randy Howard.
I will also skip Richard Heathfield who is higher on the evolutionary
scale than the troll and is more a gnome. Per my committment I shall
keep the focus here on program correctness proving and deduction of
behavior, mit seinem relationship to a critical theory of computer
science.

> )> Could you give an example of a correctness proof involving recursion ?
>
> Edward wrote:
>
> ) My reply's conditions are these, since I have considerable other committments:
> )
> ) (1) The reply shall exclusively focus on Willem's question. It shall contain
> ) some high flights but they shall relate to the matter at hand except for the
> ) last line in the post.
> )
> ) (2) There is a working set of trolls in this ng who won't be answered.
> )
> ) OK, for the reply. The following extempore C function
> )
> ) int nFactorial(int n)
> ) {
> ) if ( n < 1 ) { ... error handler ... }
> ) for ( int nFactorial = n, int n2 = n - 1; n2 > 1; n2-- ) nFactorial *= n2;
> ) return(nFactorial);
> ) }
> )
> ) has this correctness proof
>
> I'll snip the correctness proof, but I should mention that you've got your
> terminologies mixed, that was an _inductive_ proof.

The use of the word "terminologies" reifies understanding and means,
literally, that the mathematician becomes a mathematical clerk. The
proof was indeed "inductive" but the problem with calling it
"inductive" as a teacher is that it is then promptly confused with an
*empirical* argument. That's why an alternate description is
"recursive".

And in a substantive sense, the proof recurses for it mentions itself
in the second half. We've proved QED for m bounded by n and need only
to prove that if A(m) then A(m+1).

> Instead I'll write down how I would prove it, *without* induction.
>
> (I had to pull apart the statements into multiple lines to be able to put
> comments between them. The bits with 'max' are because the loop is a bit
> unclean in that n2 could be zero after the loop.)
>
> Of course, if you use a while-loop, you don't have the problem that you
> have to account for three jumps within the loop. I grant you that.
> But then, VB has the same problem with its for loop. And even worse
> problem, because increments or decrements happen implicitly.

The increments and decrements are as explicit as hell, for Next
intIndex1 is in effect a command to increment or decrement, context
sensitive with regards to the Step clause.

The for loop of C is overgeneral and overexplicit because when it was
designed good programmers were still having problems with loops.

>
> P.S: Can you have a variable with the same name as a function ?

Not in Visual Basic. Nor in C to my knowledge. Chalk up a point in
favor of Hungarian Notation!
>
>
> int nFactorial(int n)
> {
> int n2, f;
> // n is an integer
> if ( n < 1 ) { error() }
> // n >= 1
> for (
> f = n,
> n2 = n - 1;
> // Guard
> // f * max(n2,1)! == n!
> n2 > 1;
> // f * max(n2,1)! == n!
> // n2 > 1
> // Note: jump to begin of loop body.
>
> // Note: jump from end of loop body.
> // f * max(n2-1,1)! == n!
> n2--;
> // f * max(n2,1)! == n!
> // Note: Jump to guard
> )
> // begin of loop body
> // f * max(n2,1)! == n!
> // n2 > 1
> f *= n2;
> // f * max(n2 - 1,1)! == n!
> // End of loop body.
> // Loop guard was false, so:
> // n2 <= 1
> // f * max(n2,1)! == n!
> // Therefore: f == n!
> return(f);
> // Function returns n!
> }
>
>
> Very simple, and no induction required.

As a layperson I would have to ask if it is not "hidden" in the max.
Also, I consider my proof more elegant. Even an Intuitionist cannot
get by without recursion and I don't know why delenda est.

>
> If you use a while loop, and do the edge case differently:
>
> int nFactorial(int n)
> {
> int n2, f;
> // n is an integer
> if ( n < 1 ) { error() }
> // n >= 1
> n2 = n;
> f = 1;
> // f * n2! == n!
> // n2 >= 1
> while (n2 > 1) {
> // f * n2! == n!
> // n2 > 1
> f *= n2;
> // f * (n2-1)! == n!
> // n2 > 1
> n2--;
> // f * n2! == n!
> // n2 >= 1
> // Note: THis is the same as the prep. before the loop.
> }
> // f * n2! == n!
> // n2 == 1 (Loop guard was false)
> // Therefore: f == n!
> return (f);
> // Function returns n!
> }
>
> Easy, huh.

I agree that (1) this does not need recursion and (2) it is an elegant
and illuminating proof: the last five lines are very exciting.

The line after the loop closure can be rewritten because you've shown
how inside the loop it is invariantly true. Essentially the proof
creates a vision of the algorithm as "unrolled" for any N and replaced
by a series of multiplies.

I do not know whether it disproves the need for recursion ANYWHERE in
proving programs correct (or deductively predicting their behavior).
Can you provide a proof that recursion is never needed?

My concern happens to be codifying ways in which informal, natural
language proofs can be used, and I need to keep the language informal
and not at all symbolic. Your approach is useful since mine was less
detailed and your approach would be better for teaching students who
don't know recursion.

My concern is the use of natural language because as soon as you
formalize something sufficiently and you have at least one computer,
there is an irresistable tendency to want to create, not
knowledge-in-students, but Yet Another programming tool or programming
language which in many cases is destructive of knowledge-in-students.

Instead of learning to discourse as did Dijkstra in natural language
about program behavior, the student masters a proof notation, inline
and preprocessed with his program, and the result isn't that the
programs become self-assuring.

Instead they become a mass of claptrap because the connection with the
human world (in the form of insight) has been abandoned in favor of
gear.

Thanks for an illuminating proof. I shall keep this simpler approach
in mind.

Does it work for

int nFactorial(int intN)
{
    if (intN < 1) { ... error ... };
    if (intN == 1) return(1);
    return(nFactorial(intN - 1));
}

?

Relevant Pages

  • Re: Learning Lisp in Linux?
    ... like programming in assembly language.) ... (if (zero? ... (loop for n from 1 upto n ... even heard of the concept of recursion. ...
    (comp.lang.lisp)
  • Re: First Program
    ... an array. ... I am just beginning to learn this language. ... int total = 0; ... good,) but not in a similar loop in add_array. ...
    (comp.lang.c)
  • Re: Need help with C Language
    ... I have 2 qs about statements and their meanings in the C language. ... int a ... when will the IF loop be true and when will it ... assigned a new value or what is happ ...
    (comp.lang.c)
  • Re: C recursion question
    ... Recursion is a fundamental idea in both informatics and pure ... mathematics. ... ML/1 is a macro language devised a long time ago by Peter Brown at the ... explicit loops usually involve a loop ...
    (alt.comp.lang.learn.c-cpp)
  • Re: finding max and min integers - newbie question
    ... > Alas, while at it, why didn't you use recursion instead of the ... > loop, and additional function arguments instead of the local ... int FindMin(int* Data, int Size) ...
    (comp.lang.cpp)