Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms

Thaynara Arielly de Lima, Andréia Borges Avelar, André Luiz Galdino, Mauricio Ayala-Rincón

TL;DR

This paper extends the PVS algebra library to formalize divisibility, prime and irreducible elements, and the linkage between principal ideal domains and unique factorization domains within an abstract ring setting. It introduces a general, parameterized Euclidean gcd algorithm for Euclidean domains and proves its termination and correctness, then instantiates the framework to concrete rings such as $Z$ and $Z[i]$ and to arbitrary fields. The work demonstrates how abstract formalization yields portable results that specialize cleanly to classical gcd computations and factorization properties, enabling modular arithmetic and Euler–Fermat-style reasoning within Euclidean domains. It situates these developments among other formalizations (Isabelle/HOL, Lean, Coq, HOL Light, etc.) and outlines ongoing extensions, including quaternions and potential code-extraction workflows via PVSio.

Abstract

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.

Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms

TL;DR

This paper extends the PVS algebra library to formalize divisibility, prime and irreducible elements, and the linkage between principal ideal domains and unique factorization domains within an abstract ring setting. It introduces a general, parameterized Euclidean gcd algorithm for Euclidean domains and proves its termination and correctness, then instantiates the framework to concrete rings such as and and to arbitrary fields. The work demonstrates how abstract formalization yields portable results that specialize cleanly to classical gcd computations and factorization properties, enabling modular arithmetic and Euler–Fermat-style reasoning within Euclidean domains. It situates these developments among other formalizations (Isabelle/HOL, Lean, Coq, HOL Light, etc.) and outlines ongoing extensions, including quaternions and potential code-extraction workflows via PVSio.

Abstract

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.
Paper Structure (10 sections, 4 theorems, 4 equations, 1 figure)

This paper contains 10 sections, 4 theorems, 4 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Formalization of Euclidean Domains
  3. Prime and irreducible elements on rings
  4. Unique Factorization Domains
  5. Euclidean Rings
  6. Formalization of gcd Algorithm for Euclidean Domains
  7. Related Work and work in progress
  8. Related work
  9. Work in progress and applications
  10. Conclusions and Future Work

Key Result

Theorem 2.1

Let $a, b$, and $u$ be elements of a commutative ring $R$ with identity.

Figures (1)

  • Figure 1: Ring theories expanding the PVS algebra library

Theorems & Definitions (4)

  • Theorem 2.1: Th.3.2, Hungerford hungerford80
  • Theorem 2.2: Th.3.4, Hungerford hungerford80
  • Theorem 2.3: Th.3.7, Hungerford hungerford80
  • Theorem 2.4: Th.3.9, Hungerford hungerford80