-
Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms
Authors:
Thaynara Arielly de Lima,
Andréia Borges Avelar,
André Luiz Galdino,
Mauricio Ayala-Rincón
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, an…
▽ More
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.
△ Less
Submitted 23 April, 2024;
originally announced April 2024.
-
Reconfigurable Heterogeneous Parallel Island Models
Authors:
Lucas Ângelo da Silveira,
Thaynara Arielly de Lima,
Mauricio Ayala-Rincón
Abstract:
Heterogeneous Parallel Island Models (HePIMs) run different bio-inspired algorithms (BAs) in their islands. From a variety of communication topologies and migration policies fine-tuned for homogeneous PIMs (HoPIMs), which run the same BA in all their islands, previous work introduced HePIMs that provided competitive quality solutions regarding the best-adapted BA in HoPIMs. This work goes a step f…
▽ More
Heterogeneous Parallel Island Models (HePIMs) run different bio-inspired algorithms (BAs) in their islands. From a variety of communication topologies and migration policies fine-tuned for homogeneous PIMs (HoPIMs), which run the same BA in all their islands, previous work introduced HePIMs that provided competitive quality solutions regarding the best-adapted BA in HoPIMs. This work goes a step forward, maintaining the population diversity provided by HePIMs, and increasing their flexibility, allowing BA reconfiguration on islands during execution: according to their performance, islands may substitute their BAs dynamically during the evolutionary process. Experiments with the introduced architectures (RecHePIMs) were applied to the NP-hard problem of sorting permutations by reversals, using four different BAs, namely, simple Genetic Algorithm, Double-point crossover Genetic Algorithm, Differential Evolution, and self-adjusting Particle Swarm Optimization. The results showed that the new reconfigurable heterogeneous models compute better quality solutions than the HePIMs closing the gap with the HoPIM running the best-adapted BA.
△ Less
Submitted 5 May, 2022;
originally announced May 2022.
-
Teaching Interactive Proofs to Mathematicians
Authors:
Mauricio Ayala-Rincón,
Thaynara Arielly de Lima
Abstract:
This work discusses an approach to teach to mathematicians the importance and effectiveness of the application of Interactive Theorem Proving tools in their specific fields of interest. The approach aims to motivate the use of such tools through short courses. In particular, it is discussed how, using as case-of-study algebraic notions and properties, the use of the proof assistant Prototype Verif…
▽ More
This work discusses an approach to teach to mathematicians the importance and effectiveness of the application of Interactive Theorem Proving tools in their specific fields of interest. The approach aims to motivate the use of such tools through short courses. In particular, it is discussed how, using as case-of-study algebraic notions and properties, the use of the proof assistant Prototype Verification System PVS is promoted to interest mathematicians in the development of their mechanized proofs.
△ Less
Submitted 29 October, 2020;
originally announced October 2020.
