Email Gateway (Aug 22 2022 at 21:14): Email Gateway (Aug 22 2022 at 21:14):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce yet another new AFP entry:
Closest Pair of Points Algorithms, by Martin Rau and Tobias Nipkow
This entry provides two related verified divide-and-conquer algorithms solving the fundamental Closest Pair of Points problem in Computational Geometry. Functional correctness and the optimal running time of O(n log n) are proved. Executable code is generated which is empirically competitive with handwritten reference implementations.
https://www.isa-afp.org/entries/Closest_Pair_Points.html
Larry Paulson
Email Gateway (Aug 23 2022 at 08:12):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
sounds interesting, so I had a look how these things are done these
days. But I guess I read more into the abstract than is there (which
may be my fault). Is it correct that
the connection between the algorithm (e.g. combine) and the
calculation of the running time (e.g. t_combine) is not
mechanically verified (and a skeptical reader would have to
carefully compare the two definitions).
it shows that it is in O(n log n), but it does _not_ show
that this is indeed the optional running time for this task
(which “optimal running time proved” sounds a bit like).
I don't want to say that there is dishonesty in the abstract, but it’s
just that I was mostly curious about how to do these two things :-)
Cheers,
Joachim
Email Gateway (Aug 23 2022 at 08:12):From: Tobias Nipkow <nipkow@in.tum.de>
On 21/01/2020 12:09, Joachim Breitner wrote:
Hi,
Am Dienstag, den 14.01.2020, 12:52 +0000 schrieb Lawrence Paulson:
I’m happy to announce yet another new AFP entry:
Closest Pair of Points Algorithms, by Martin Rau and Tobias Nipkow
This entry provides two related verified divide-and-conquer
algorithms solving the fundamental Closest Pair of Points problem in
Computational Geometry. Functional correctness and the optimal
running time of O(n log n) are proved. Executable code is generated
which is empirically competitive with handwritten reference
implementations.sounds interesting, so I had a look how these things are done these
days. But I guess I read more into the abstract than is there (which
may be my fault). Is it correct that* the connection between the algorithm (e.g.
combine) and the
calculation of the running time (e.g.t_combine) is not
mechanically verified (and a skeptical reader would have to
carefully compare the two definitions).
Correct. We say so in an accompanying paper which is not online yet and of which
this is the abstract. There we also refer to a monadic approach where the result
and the running time are defined simultaneously and that we could have used to
increasew confidence in our t_ functions:
https://www.isa-afp.org/entries/Root_Balanced_Tree.html
* it shows that it is in O(n log n), but it does _not_ show
that this is indeed the optional running time for this task
(which “optimal running time proved” sounds a bit like).
We do not show that the running time is optimal and the grammar is clear: "the
optimal running time is proved" is not the same as "that the running time is
optimal is proved".
Tobias
I don't want to say that there is dishonesty in the abstract, but it’s
just that I was mostly curious about how to do these two things :-)Cheers,
Joachim
Last updated: Apr 19 2024 at 20:15 UTC