Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910419210207232 |
|---|---|
| author | de Lima, Thaynara Arielly Avelar, Andréia Borges Galdino, André Luiz Ayala-Rincón, Mauricio |
| author_facet | de Lima, Thaynara Arielly Avelar, Andréia Borges Galdino, André Luiz Ayala-Rincón, Mauricio |
| contents | This paper discusses the extension of the Prototype Verification System (PVS) sub-theory for rings, part of the PVS algebra theory, with theorems related to the division algorithm for Euclidean rings and Unique Factorization Domains that are general structures where an analog of the Fundamental Theorem of Arithmetic holds. First, we formalize the general abstract notions of divisibility, prime, and irreducible elements in commutative rings, essential to deal with unique factorization domains. Then, we formalize the landmark theorem, establishing that every principal ideal domain is a unique factorization domain. Finally, we specify the theory of Euclidean domains and formally verify that the rings of integers, the Gaussian integers, and arbitrary fields are Euclidean domains. To highlight the benefits of such a general abstract discipline of formalization, we specify a Euclidean gcd algorithm for Euclidean domains and formalize its correctness. Also, we show how this correctness is inherited under adequate parameterizations for the structures of integers and Gaussian integers. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_14920 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms de Lima, Thaynara Arielly Avelar, Andréia Borges Galdino, André Luiz Ayala-Rincón, Mauricio Logic in Computer Science This paper discusses the extension of the Prototype Verification System (PVS) sub-theory for rings, part of the PVS algebra theory, with theorems related to the division algorithm for Euclidean rings and Unique Factorization Domains that are general structures where an analog of the Fundamental Theorem of Arithmetic holds. First, we formalize the general abstract notions of divisibility, prime, and irreducible elements in commutative rings, essential to deal with unique factorization domains. Then, we formalize the landmark theorem, establishing that every principal ideal domain is a unique factorization domain. Finally, we specify the theory of Euclidean domains and formally verify that the rings of integers, the Gaussian integers, and arbitrary fields are Euclidean domains. To highlight the benefits of such a general abstract discipline of formalization, we specify a Euclidean gcd algorithm for Euclidean domains and formalize its correctness. Also, we show how this correctness is inherited under adequate parameterizations for the structures of integers and Gaussian integers. |
| title | Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2404.14920 |