5 ms·

If I made a zeno's paradox loop: bigFloat delta = 0.5 bigFloat total = 0.0 while total < 1.0: total+=delta delta*=0.5 Where does this fit

• deleted 11y ago
  [deleted]
• emillon 11y ago
  This kind of proofs usually are separated in two steps: - correction: define a loop invariant. Assuming the loop terminates, it will hold when the program exits the loop. - termination: define a loop variant, something that changes at every iteration. If you can find a variant that is a strictly decreasing sequence of natural numbers (or an increasing, bounded sequence), you've established that the loop terminates. Once you've done these two steps you know that the program terminates and the invariant holds at the end. (in your case, you won't be able to find a good variant - depending on the floating point semantics you use of course).
• spacehome 11y ago
  The two loop invariants would be: 1.0 == total + delta * 2 and delta > 0, so the while condition would never be false. The amount of memory required to store the delta variable should be at least log_2(n) bits, where n is the iteration number. This has to be true, regardless of the implementation details of bigFloat because delta has to take on n distinct values. Eventually it exhausts the memory of the machine. It seems pretty straightforward, unless your compiler is smart enough to see what's going on and optimize the body of the loop away, in which case it wouldn't terminate.
• AnimalMuppet 11y ago
  You're asking for a loop invariant to prove that a non-terminating loop terminates? That seems... somewhat contradictory. Either you can't prove that with a loop invariant, or the proof must be invalid. As you said, the machine eventually runs out of memory. But "loop invariants" don't usually include the machine running out of memory as the termination condition, because that's more a crash than a loop termination. (That is, whatever part of the program you wanted to execute after the zeno loop won't execute, because the program terminated, not just the loop.) So when we talk about loop termination, program-crashing events are usually out of scope. (That's something we also need to prove - no undesirable side effects - but that's actually a separate issue.)
• SixSigma 11y ago
  delta > epsilon when this is false, the loop should terminate even BigFloats have limited precision
  • spacehome 11y ago
    I think this depends on implementation. I don't know exactly what the grandfather means by BigFloat, but by analogy with BigInteger, I assume it's arbitrary precision.
    • SixSigma 11y ago
      Arbitrary means the epsilon is chosen, not unbounded. I have just also realised that delta would be 0 if < epsilon. So the invariant delta > 0, break when false. (I think, the OP is my introduction to invariant loops). Scheme, for instance, has a 32 bit mantissa for BigFloat by default [1] Haskell's mantissa precision is determined by the type of the mantissa when created [2] For GNU MPFR "the precision in bits can be set exactly to any valid value" [3] which is what is used in Lisp, Python, Perl, Racket, Java, ADA, Ruby & Eiffel. [1] https://github.com/55portal55/bigfloat/blob/master/bigfloat.scm https://github.com/55portal55/bigfloat/blob/master/bigfloat.... [2] https://hackage.haskell.org/package/numbers-3000.2.0.1/docs/Data-Number-BigFloat.html https://hackage.haskell.org/package/numbers-3000.2.0.1/docs/... [3] http://www.mpfr.org/mpfr-current/mpfr.html http://www.mpfr.org/mpfr-current/mpfr.html
      • spacehome 11y ago
        > Arbitrary means the epsilon is chosen, not unbounded. This is not the commonly understood nomenclature, notwithstanding what some languages call a BigFloat. See: https://en.wikipedia.org/wiki/Arbitrary-precision_arithmetic https://en.wikipedia.org/wiki/Arbitrary-precision_arithmetic In any case, it's clearly not what Rhapso intended, either, because otherwise his code snippet wouldn't exhaust memory.
        • SixSigma 11y ago
          OK, you're right. damn those implementations :)
• Animats 11y ago
  Termination is not about the loop invariant. You also need a measure of termination, which is usually a nonnegative integer which decreases on each iteration. In our Pascal-F system, we had a MEASURE statement for that. You didn't need it for FOR loops, though.