Re: Response to Karen and to Willem on recursive proofs

From: FM (dartdanfm_at_yahoo.com)
Date: 01/24/04 

Date: Sat, 24 Jan 2004 22:59:34 GMT

<blmblm@myrealbox.com> wrote:
> Willem <willem@stack.nl> wrote:
> >)> Technically, this method proves that *if* a loop terminates, it terminates
> >)> with the right answer. You have to *prove* that a loop terminates as well,
> >)> but you can do that separately.
> >
> >FM wrote:
> >
> >) And how would you do that exactly?
> >
> >IIRC, it involves showing that some function f(n), a function that has the
> >state space of the loop as its domain, and N as its range, decreases at
> >every iteration. Usually, you can discard almost all of the state space
> >and concentrate on the value of one variable, and all you have to prove is
> >that that variable (or a sumple algebraic function on that variable)
> >decreases but doesn't go below zero.
> >
> >For example, for the factorial loop, you prove that 'n' decreases at every
> >iteration, but that it doesn't go below zero.
>
> Another nitpick: One of the requirements here is that f(n) decreases
> *by at least some threshold amount* at each iteration. Well, maybe
> this goes without saying for any fixed-size type, but if we were
> working in the idealized world of pure mathematics, and the value of
> f(n) was not constrained to be an integer ....

Well, he said N (as in the set of natural numbers) is the range
of f(n), so it has that constraint.

Dan.

Relevant Pages

  • Re: In Simulink,how to change an element of a stat
    ... >> John Creighton wrote: ... >>> conditions of the delay block to the state space matrix ... >>> zero derivative. ... > It may be that you weakness is not simulink but control theory. ...
    (comp.soft-sys.matlab)
  • Re: In Simulink,how to change an element of a stat
    ... >> John Creighton wrote: ... >>> If you have the state space matrix as the output of a delay ... >> zero derivative. ... It may be that you weakness is not simulink but control theory. ...
    (comp.soft-sys.matlab)