Email Gateway (Aug 22 2022 at 16:51): Email Gateway (Aug 22 2022 at 16:51):From: Manuel Eberl <eberlm@in.tum.de>
I forgot to attach the error message. Here it is:
Unofficial version of Isabelle/HOL (unidentified repository version)
Run out of store - interrupting threads
Run out of store - interrupting threads
Failed to recover - exiting
FATAL: exception not rethrown
standard_error terminated
standard_output terminated
Cannot read message:
Connection reset
message_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 134
Email Gateway (Aug 22 2022 at 16:53):From: Fabian Immler <immler@in.tum.de>
Hi Manuel,
Your concrete example should not be out of reach of the approximation tactic.
On my Mac, I can do e.g.,
lemma "exp (exp 16000 :: real) > 0"
by (approximation 80)
which proves the goal in about 10s (both in 32 and 64 bit mode).
Therefore I am not sure if it is really the large exponents that pose the problem here.
As a side note on the tactic in general, if you care about performance: In my experience,
you get good results (here about 5s) by setting the precision to about half the precision of the native integer type (i.e., 15 for x86 and 30 for x86_64).
Fabian
smime.p7s
Email Gateway (Aug 22 2022 at 16:53):From: Manuel Eberl <eberlm@in.tum.de>
Ah sorry, I misread. Try it again with 160000. ;)
My current workaround is to first do the computation in ML using
hardware floating-point numbers. If the result is finite (i.e. not NaN
or Infinity) and the proposition holds for the resulting numbers, I call
approximation.
It's not pretty and certainly not "complete", but it handles all of my
use cases pretty well so far.
The only proper solution I can think of would be to add some kind of
precision for the exponent as well, and if an exponent exceeds that
number, the computation is aborted with an error.
As a side note on the tactic in general, if you care about performance: In my experience,
you get good results (here about 5s) by setting the precision to about half the precision of the native integer type (i.e., 15 for x86 and 30 for x86_64).
That's not an issue here since I chose 10 anyway. That's usually enough
for my needs.
Manuel
Email Gateway (Aug 22 2022 at 16:54):From: Fabian Immler <immler@in.tum.de>
Am 05.03.2018 um 12:33 schrieb Manuel Eberl <eberlm@in.tum.de>:
Ah sorry, I misread. Try it again with 160000. ;)
My current workaround is to first do the computation in ML using
hardware floating-point numbers. If the result is finite (i.e. not NaN
or Infinity) and the proposition holds for the resulting numbers, I call
approximation.It's not pretty and certainly not "complete", but it handles all of my
use cases pretty well so far.
We actually do something similar in quickcheck[approximation] (~~/src/HOL/Decision_Procs/approximation_generator.ML):
Trying to find counterexamples with IEEE floating point arithmetic and certifying them by approximation.
The only proper solution I can think of would be to add some kind of
precision for the exponent as well, and if an exponent exceeds that
number, the computation is aborted with an error.
Yes, this would be a solution. One could also think of computing the bounds with IEEE floating point numbers.
As a side note on the tactic in general, if you care about performance: In my experience,
you get good results (here about 5s) by setting the precision to about half the precision of the native integer type (i.e., 15 for x86 and 30 for x86_64).That's not an issue here since I chose 10 anyway. That's usually enough
for my needs.Manuel
Email Gateway (Aug 22 2022 at 17:01):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I noticed that the approximation tactic behaves very poorly when the
input is very large. For instance, attempting to prove "exp (exp 16000
:: real) > 0" with it results in the tactic running for about a minute
or two before. The entire Isabelle system becomes unresponsive and
eventually stops with one of Isabelle/jEdit's "total existence failure"
messages.
Now, obviously, I am not expecting the tactic to be able to prove this –
it uses software floating-point numbers and the exponents here are
staggeringly large. However, I am wondering if it is possible to make
the tactic fail gracefully, or at least not take down the entire system.
Otherwise it is highly problematic to use this tactic as a solver in the
background, which I intend to do.
Manuel
Last updated: Nov 21 2024 at 12:39 UTC