Verification of closest pair of points algorithms. (English) Zbl 07614680
Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12167, 341-357 (2020).
Summary: We verify two related divide-and-conquer algorithms solving one of the fundamental problems in Computational Geometry, the Closest Pair of Points problem. Using the interactive theorem prover Isabelle/HOL, we prove functional correctness and the optimal running time of \(\mathcal{O}(n \log n)\) of the algorithms. We generate executable code which is empirically competitive with handwritten reference implementations.
For the entire collection see [Zbl 1498.68017].
For the entire collection see [Zbl 1498.68017].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Akra, M., Bazzi, L.: On the solution of linear recurrence equations. Comput. Optim. Appl. 10(2), 195-210 (1998). https://doi.org/10.1023/A:1018373005182 · Zbl 0898.39003 · doi:10.1023/A:1018373005182 |
| [2] | Bentley, J.L., Shamos, M.I.: Divide-and-Conquer in multidimensional space. In: Proceedings of Eighth Annual ACM Symposium on Theory of Computing, STOC 1976, pp. 220-230. ACM (1976). https://doi.org/10.1145/800113.803652 · Zbl 0365.68050 |
| [3] | Bertot, Y.: Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs. In: Fischer, B., Uustalu, T. (eds.) ICTAC 2018. LNCS, vol. 11187, pp. 3-10. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02508-3_1 · Zbl 1518.68417 · doi:10.1007/978-3-030-02508-3_1 |
| [4] | Brun, C., Dufourd, J., Magaud, N.: Designing and proving correct a convex hull algorithm with hypermaps in Coq. Comput. Geom. 45(8), 436-457 (2012). https://doi.org/10.1016/j.comgeo.2010.06.006 · Zbl 1247.65021 · doi:10.1016/j.comgeo.2010.06.006 |
| [5] | Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009) · Zbl 1187.68679 |
| [6] | Dufourd, J.: An intuitionistic proof of a discrete form of the Jordan Curve Theorem formalized in Coq with combinatorial hypermaps. J. Autom. Reasoning 43(1), 19-51 (2009). https://doi.org/10.1007/s10817-009-9117-x · Zbl 1187.68525 · doi:10.1007/s10817-009-9117-x |
| [7] | Dufourd, J.-F., Bertot, Y.: Formal study of plane delaunay triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 211-226. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_16 · Zbl 1291.68337 · doi:10.1007/978-3-642-14052-5_16 |
| [8] | Eberl, M.: Proving Divide and Conquer complexities in Isabelle/HOL. J. Autom. Reasoning 58(4), 483-508 (2016). https://doi.org/10.1007/s10817-016-9378-0 · Zbl 1414.68101 · doi:10.1007/s10817-016-9378-0 |
| [9] | Eberl, M.: Verified real asymptotics in Isabelle/HOL. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC 2019. ACM, New York (2019). https://doi.org/10.1145/3326229.3326240 |
| [10] | Ge, Q., Wang, H.T., Zhu, H.: An improved algorithm for finding the closest pair of points. J. Comput. Sci. Technol. 21(1), 27-31 (2006). https://doi.org/10.1007/s11390-006-0027-7 · Zbl 1190.68070 · doi:10.1007/s11390-006-0027-7 |
| [11] | Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 279-294. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_21 · Zbl 1317.68213 · doi:10.1007/978-3-642-39634-2_21 |
| [12] | Immler, F.: A verified algorithm for geometric zonotope/hyperplane intersection. In: Certified Programs and Proofs, CPP 2015, pp. 129-136. ACM (2015). https://doi.org/10.1145/2676724.2693164 |
| [13] | Jiang, M., Gillespie, J.: Engineering the Divide-and-Conquer closest pair algorithm. J. Comput. Sci. Technol. 22(4), 532-540 (2007) · doi:10.1007/s11390-007-9066-y |
| [14] | Meikle, L.I., Fleuriot, J.D.: Mechanical theorem proving in computational geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol. 3763, pp. 1-18. Springer, Heidelberg (2006). https://doi.org/10.1007/11615798_1 · Zbl 1159.68556 · doi:10.1007/11615798_1 |
| [15] | Narboux, J., Janicic, P., Fleuriot, J.: Computer-assisted theorem proving in synthetic geometry. In: Sitharam, M., John, A.S., Sidman, J. (eds.) Handbook of Geometric Constraint Systems Principles. Discrete Mathematics and Its Applications, Chapman and Hall/CRC (2018) |
| [16] | Nipkow, T.: Verified root-balanced trees. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 255-272. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-71237-6_13 · Zbl 1503.68052 · doi:10.1007/978-3-319-71237-6_13 |
| [17] | Nipkow, T., Klein, G.: Concrete Semantics with Isabelle/HOL. Springer, Heidelberg (2014). http://concrete-semantics.org · Zbl 1410.68004 |
| [18] | Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9 · Zbl 0994.68131 · doi:10.1007/3-540-45949-9 |
| [19] | Pereira, J.C., Lobo, F.G.: An optimized Divide-and-Conquer algorithm for the closest-pair problem in the planar case. J. Comput. Sci. Technol. 27(4), 891-896 (2012) · Zbl 1280.68282 · doi:10.1007/s11390-012-1272-6 |
| [20] | Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 346-361. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44755-5_24 · Zbl 1005.68557 · doi:10.1007/3-540-44755-5_24 |
| [21] | Preparata, F.P., Shamos, M.I.: Computational Geometry: An Introduction. Springer, Heidelberg (1985). https://doi.org/10.1007/978-1-4612-1098-6 · Zbl 0575.68059 · doi:10.1007/978-1-4612-1098-6 |
| [22] | Puitg, F., Dufourd, J.: Formalizing mathematics in higher-order logic: a case study in geometric modelling. Theor. Comput. Sci. 234(1-2), 1-57 (2000). https://doi.org/10.1016/S0304-3975(98)00228-X · Zbl 0945.68178 · doi:10.1016/S0304-3975(98)00228-X |
| [23] | Rau, M., Nipkow, T.: Closest pair of points algorithms. Archive of Formal Proofs, Formal proof development, January 2020. http://isa-afp.org/entries/Closest_Pair_Points.html |
| [24] | Sack, J.R., Urrutia, J. (eds.): Handbook of Computational Geometry. North-Holland Publishing Co., Amsterdam (2000) · Zbl 0930.65001 |
| [25] | Shamos, M.I., Hoey, D.: Closest-point problems. In: 16th Annual Symposium on Foundations of Computer Science (SFCS 1975), pp. 151-162, October 1975. https://doi.org/10.1109/SFCS.1975.8 |
| [26] | Zhou, Y., Xiong, P., Zhu, H.: An improved algorithm about the closest pair of points on plane set. Comput. Res. Dev. 35(10), 957-960 (1998) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
