×

zbMATH — the first resource for mathematics

A verified implementation of algebraic numbers in Isabelle/HOL. (English) Zbl 07176602
Summary: We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle’s code generator. The development combines various existing formalizations such as matrices, Sturm’s theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.

MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Avanzini, M., Sternagel, C., Thiemann, R.: Certification of complexity proofs using CeTA. In: RTA 2015. pp. 23-39. LIPIcs 36 (2015) · Zbl 1366.68105
[2] Brown, Ws, The subresultant PRS algorithm, ACM Trans. Math. Softw., 4, 3, 237-249 (1978) · Zbl 0385.68044
[3] Brown, Ws; Traub, Jf, On Euclid’s algorithm and the theory of subresultants, J. ACM, 18, 4, 505-514 (1971) · Zbl 0226.65041
[4] Cohen, Cyril, Construction of Real Algebraic Numbers in Coq, Interactive Theorem Proving, 67-82 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1360.68744
[5] Cohen, C., Djalal, B.: Formalization of a Newton series representation of polynomials. In: CPP 2016. pp. 100-109. ACM (2016)
[6] Cohen, C.; Mahboubi, A., Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Log. Methods Comput. Sci., 8, 1-2, 1-40 (2012) · Zbl 1241.68096
[7] Divasón, J., Joosten, S., Thiemann, R., Yamada, A.: A formalization of the Berlekamp-Zassenhaus factorization algorithm. In: CPP 2017, pp. 17-29 (2017)
[8] Ducos, L., Optimizations of the subresultant algorithm, J. Pure Appl. Algebra, 145, 149-163 (2000) · Zbl 0941.65044
[9] Eberl, M.: A decision procedure for univariate real polynomials in Isabelle/HOL. In: CPP 2015. pp. 75-83. ACM (2015)
[10] Eberl, M.: Linear recurrences. Archive of Formal Proofs (Oct 2017), http://isa-afp.org/entries/Linear_Recurrences.html, Formal proof development
[11] von zur Gathen, J., Gerhard, J.: Modern computer algebra, 2nd edn. Cambridge University Press, Cambridge (2003) · Zbl 1055.68168
[12] Giesl, Jürgen; Mesnard, Frédéric; Rubio, Albert; Thiemann, René; Waldmann, Johannes, Termination Competition (termCOMP 2015), Automated Deduction - CADE-25, 105-108 (2015), Cham: Springer International Publishing, Cham · Zbl 06515500
[13] Haftmann, Florian; Krauss, Alexander; Kunčar, Ondřej; Nipkow, Tobias, Data Refinement in Isabelle/HOL, Interactive Theorem Proving, 100-115 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1317.68212
[14] Huffman, Brian; Kunčar, Ondřej, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, Certified Programs and Proofs, 131-146 (2013), Cham: Springer International Publishing, Cham · Zbl 1426.68284
[15] Jouannaud, Jp; Lescanne, P., On multiset orderings, Inf. Process. Lett., 15, 2, 57-63 (1982) · Zbl 0486.68041
[16] Krauss, Alexander, Recursive Definitions of Monadic Functions, Electronic Proceedings in Theoretical Computer Science, 43, 1-13 (2010)
[17] Li, W.: Count the number of complex roots. Archive of Formal Proofs (Oct 2017), http://isa-afp.org/entries/Count_Complex_Roots.html, Formal proof development
[18] Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: CPP 2016. pp. 66-75. ACM (2016)
[19] Mahboubi, Assia, Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials, Automated Reasoning, 438-452 (2006), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1222.68369
[20] Mishra, B., Algorithmic Algebra. Texts and Monographs in Computer Science (1993), New York: Springer, New York
[21] Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002) · Zbl 0994.68131
[22] Niven, I.: Irrational Numbers. No. 11 in Carus Mathematical Monographs, Mathematical Association of America (1956)
[23] Prasolov, V.V.: Polynomials. Springer (2004)
[24] Thiemann, René; Yamada, Akihisa, Algebraic Numbers in Isabelle/HOL, Interactive Theorem Proving, 391-408 (2016), Cham: Springer International Publishing, Cham · Zbl 06644756
[25] Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: CPP 2016. pp. 88-99. ACM (2016)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.