Re: Response to Karen and to Willem on recursive proofs

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

  • Next message: Dan Tex1: "Re: Mars Rover Controlled By Java" 
    Date: 19 Jan 2004 18:28:37 -0800

    Willem <willem@stack.nl> wrote in message news:<slrnc0ct6e.1jac.willem@toad.stack.nl>...
    > Edward wrote:
    > ) Willem, mein Herr, your answer on program proving was correct but you
    > ) concealed the fact that the steps from what you called the
    > ) "preposition" to the n+1th preposition are trivial except for a for
    > ) or do loop...in which recursion nearly always is necessary.
    >
    > All you need to do is prove that 'preposition-in-loop' holds during the
    > loop, and that 'preposition-in-loop' AND NOT 'loop-condition' implies
    > 'preposition-after-loop'. No recursion involved there.
    >
    > Could you give an example of a correctness proof involving recursion ?

    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

    int nFactorial(int n)
    {
    // n is an integer
    if ( n < 1 ) { ... error handler ... }
    // n is an integer >= 1
    for ( int nFactorial = n, int n2 = n - 1; n2 > 1; n2-- ) nFactorial *= n2;
    //
    // Proof of the for loop validity...using recursion aka induction
    //
    // A recursive proof proves an assertion A true for 1 or 0, and then proves
    // "if the assertion is true for the natural number n, it is true for n+1".
    // But since it can be seen by inspection of the loop termination condition
    // that the above will leave 1 in nFactorial when n=1, I
    // will prove A true for n=2 and then the assertion "if A is true for n it
    // is true for n+1". Zero factorial and one factorial are after all
    // degenerate cases, which sound more fun than they are.
    //
    // The assertion: if n is an integer >=2, nFactorial will contain n! at
    // termination of the loop.
    //
    // A is true for n=2 because you only have to "unroll" the loop in such
    // a way that "correctness proving" becomes identical to "desk checking"
    // as practiced by competent programmers. In Marx's sense, "desk checking"
    // is a praxis which anticipates the Platonism of correctness proofs.
    //
    // // n = 2
    // int nFactorial = n
    // // n = 2 && nFactorial = 2
    // int n2 = n - 1;
    // // n = 2 && nFactorial = 2 && n2 = 1
    // if n2 <= 1 then exit the loop (reversal of loop condition)
    //
    // After this "unrolling" it is clear that nFactorial is 2 which is the
    // factorial of 2 QED: the first part of the recursive proof is complete.
    //
    // The second part of this proof supposes that the loop validly calculates
    // m! where m is an integer > 1. Does it then validly calculate the value of n,
    // where n=m+1? It would seem that it does.
    //
    // Here, nFactorial is assigned the value of n=m+1 while n2 is assigned the
    // value m. The repetition condition allows control to flow to
    // "nFactorial *= n2" which places (m+1)*(m) in nFactorial. But more
    // generally, this step will multiply n times m! since we've asserted that
    // the loop for m does calculate m!.
    //
    // Put another way, after the the sequence (test termination condition for
    // n2, multiply, decrement) is performed, the residual loop is the
    // calculation of m!. But the first pass through
    // the loop calculates n*m!: if m=n-1, the loop calculates n*(n-1)! which
    // is n!.
    //
    // Note that the SYNTAX of the poorly designed C for seems to this non-
    // specialist to make the argument clumsier than it should, for the
    // decrement comes textually before the process.
    //
    // But IF the for loop calculates m! for m=n-1, it calculates n! QED.
    //
    // I'm not a mathematician, and I don't play one in the movies, and they
    // couldn't get Cruise to play my role in A Beautiful Mind. Furthermore, this
    // is an informal proof that doesn't use a formal notation.
    //
    // But it uses MATHEMATICAL recursion...which has "nothing to do" with
    // recursion in programming only in a somewhat moronized separation of
    // disciplines.
    //
    // Recursion in programming is, of course, a subroutine calling itself. But
    // it is deeply linked with mathematical recursion aka induction because
    // programming recursion is just a LOOP unless you can prove, formally or
    // informally, that the inner call deals with fewer (n-1) elements than the
    // containing subroutine.
    //
    // The recursive proof seems a waste of time until you realize that informal
    // correctness proofs using recursion are sociologically identical to
    // productive discourse in productive structured walkthroughs.
    //
    // And it is very interesting to me that this discourse gets often short-
    // circuited by stylistic quibbling because of math anxiety and the pressure
    // software developers are under to provide "results". Of course, I could
    // not resist taking a whack at C's for loop above, so here we have a case
    // of the famous pot, and the dirty kettle.
    //
    // But in dysfunctional structured walkthroughs, people forget (if they ever
    // learned) Aristotle's sage advice in The Rhetoric, which is that the
    // rhetor can supplement his logic with stylistic gestures to the extent that
    // the rhetor self-deprecates in the old and gentlemanly style. Indeed,
    // Dijkstra's rhetoric of the "humble" programmer is consciously or
    // inconsciously Aristotelean in this regard.
    //
    // The issues that have arisen in dysfunctional structured walkthroughs and
    // in childish exchanges on comp.programming MAY be addressed in Husserl's
    // work on the foundations of geometry and general phenomenology, but I
    // haven't read enough of this fantastically difficult thinker to be sure.
    //
    // For example, in both venues, there is no clear separation between token
    // and type. A typo in this environment is unforgiveable for as opposed to
    // discourse in a mathematical community, no shared understanding exists in
    // a bourgeois, tenured community.
    //
    // Uncertainty about job tenure becomes math anxiety with the result that a
    // false certainty is sought in typesetting as opposed to writing. Levels
    // in other words occlude.
    //
    // For Husserl, the "crisis" in the European sciences may have been the
    // attempt to generalize from a mechanical certainty as seen a deduction
    // that was for Kant content-free, to a general social and political
    // certainty.
    //
    // In this context, proof retreats to its original position under Euclid,
    // which is less "proof" and more occluded with teaching.
    //
    // The recursive proof of the algorithm teaches little that we don't already
    // know. But it can be applied to more difficult problems productively, and it
    // also generates a testing methodology: test for zero, test for one, test
    // for "the myriad creatures" as in the Tao.
    //
    // And in the sphere, of brute-force praxis, I have stood up before programming
    // classes and like a stand up guy, used this method to show the students
    // that a Visual Basic program actually worked. In a world constitutive of
    // an attack on consciousness, language, memory, and its replacement by TV,
    // this is quite an accomplishment, if I do say so myself.
    //
    // Genuine symbolic manipulation as seen in both mathematics and in
    // programming teaches a political lesson which goes against the sullen
    // grain, and it is that we can "know".
    //
    //
    return(nFactorial);
    // The function returns n! for all natural numbers QED
    //
    // Recursion is used in proving loop correctness QED QED
    //
    // US out of Iraq
    }

    >
    >
    > SaSW, Willem

  • Next message: Dan Tex1: "Re: Mars Rover Controlled By Java"

    Relevant Pages

    • Re: Response to Karen and to Willem on recursive proofs
      ... The loop invariant only has to be true at the ... )>Could you give an example of a correctness proof involving recursion? ... How about a correctness proof of a recursive algorithm? ...
      (comp.programming)
    • Re: factorial n! program
      ... while the loop version is less so. ... RECURSIVE FUNCTION factRESULT nfatt ... There are better ways to make recursion interesting. ... A horrendous programming problem if you don't use ...
      (comp.lang.fortran)
    • Re: Brian Kernighan, maybe Im not worthy, maybe Im scum
      ... and just hone in on the stuff related to programming and this newsroup] ... moron that was taken from optimization which does hoist when to do so ... compiler design and optimization, including my 1976 text in graduate ... loop in a language in which the designers messed up, ...
      (comp.programming)
    • Re: what does "serialization" mean?
      ... language programming and found that my productivity increased to the ... the use of an expression in the For loop is not only ... acceptable it's good style because it forces the reader to understand. ... If the reader doesn't understand the language he must get ...
      (comp.programming)
    • Re: what does "serialization" mean?
      ... the "how" of assembler languages to the "what" of functional and logic ... > As a general programming heuristic, ... For line is inside the loop and one's style should not perpetuate ... one problem is that the concept of "iterator" doesn't ...
      (comp.programming)