Genetic Algorithms in Coq: Generalization and Formalization of the Crossover Operator

In this article we present the implementation and formal verification, using the Coq system [FHB+98], of a generalized version of the crossover operator applied to genetic algorithms (GA) [Hol92]. The first part of this work defines the multiple crossover ⊗`(p, q) of two lists p, q in any finite number of points. This definition generalizes the one given in [UE99] for a maximum number of six points. In the second part, we show that this crossover operator does not depend on the order of the list of points. Then, a more efficient definition of crossover `(p, q) is provided in the third part. Finally, we formally establish the exact relation between these two definitions, using the notion of differences list: ⊗`(p, q) = (dif `)(p, q). 1