Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator

Concepción Vidal, Felicidad Aguado, José Luis Doncel, Jose María Molinelli, Gilberto Perez

Abstract


In this article we present the implementation and formal verification, using the Coq system, of a generalized version of the crossover operator applied to genetic algorithms (GA). The first part of this work defines the multiple crossover of two lists in any finite number of points, generalizing a previous definition by Uchibori. In the second part, we show that the definition does not depend on the order of the list of points. Then, a more efficient definition of the crossover operation is provided, and formally proved to be equivalent to the previous one, exploiting the notion of difference list.

Full Text:

PDF (English)


DOI: 10.6092/issn.1972-5787/1052

Copyright (c) 2008 Concepción Vidal, Felicidad Aguado, José Luis Doncel, Jose María Molinelli, Gilberto Perez

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.