10.6092/issn.1972-5787/1052
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.
application/pdf
1972-5787
1052
1
en
Gilberto Perez
Journal of Formalized Reasoning
Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator
Text.Serial.Journal
https://jfr.unibo.it/
1
Articles
2008-10-14
2008-04-28
2008-09-23
2016-01-29
25-37
JFR
Gilberto Perez
2008/10/14
10.6092/issn.1972-5787/1052
25
1972-5787
1
en
37
Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator
https://jfr.unibo.it/article/download/1052/732
1
Genetic Algorithms in Coq: Generalization and
Formalization of the Crossover Operator
FELICIDAD AGUADO, JOSÉ LUIS DONCEL, JOSÉ MARÍA MOLINELLI
GILBERTO PÉREZ, CONCEPCIÓN VIDAL
Department of Computer Science
University of A Coruña, Spain


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.   INTRODUCTION
Genetic algorithm theory and theorem proving are two different domains of theo-
retical computer science. Each has its own scientific community and until now little
interaction seemed to exist between the two.
   The so-called evolutive computation is inspired by natural evolution. Among the
evolutive techniques we find genetic algorithms (GA). Basically, they have been
used as optimization techniques to find the best solution for a specific problem
with respect to a particular criterion given by a fitness function f . This function
evaluates each solution and determines how good it is with respect to that criterion.
The main idea is that individuals with higher values of f have a higher probability
of survival in successive generations.
   Genetic algorithm theory was originally developed by a group of researchers from
the University of Michigan led by John Holland ([Hol92]). Although there are dif-
ferent types of GAs, they all share the following three processes: selection, repro-
duction and evaluation. The algorithm repeats these processes cyclically until a
stop condition is reached.
   The elements of the first population are selected randomly. Usually each element
is represented by a string p = p1 . . . pn called a chromosome, where each pi makes
reference to a particular characteristic of the individual and belongs to a finite set
or alphabet D. The most typical is the binary encoding. In this case, the alphabet
D has only two elements, denoted by 0 and 1.
   The selection process can be performed in several ways but it is always inspired
in the idea that better adapted individuals have more chances of being selected for

This research is partially supported by XUNTA DE GALICIA, research project REGACA,
2006/38.


                                             Journal of Formal Reasoning Vol. 1, No. 1, 2008, Pages 25–37.
26     ·     Aguado et al.

reproduction. The more common mechanisms used in reproduction are crossover
and mutation. In the single-point crossover, a position i (with 1 ≤ i ≤ n) is
randomly selected and then two parents
                                            p = p1 . . . pn
                                            q = q1 . . . qn ,
are replaced by their offspring:


                                     p0 = p1 . . . pi qi+1 . . . qn
                                     q 0 = q1 . . . qi pi+1 . . . pn .
   Similar to what happens in nature, some random changes may occur in the ge-
netic content of individuals during reproduction; this is called mutation. Binary
encoding consists in eventually replacing some value 0 by 1 and vice versa. Al-
though this mutation mechanism should not occur frequently, it contributes to the
diversification of the initial population by introducing different or novel character-
istics.
   To evaluate the individuals of a population, a fitness function is used. Presum-
ably, the population will increase its average fitness over time, in such a way that,
by iterating this process, suitable solutions will be found to the problem.
   The single-point crossover was generalized by DeJong ([Jon75]) who talked about
multipoint crossover when more than one point was involved in the cutting. For
example, if we want to cross two parents p and q as above using the points {i, j, k},
the new offspring will be the following:


                        p0 = p1 . . . pi qi+1 . . . qj pj+1 . . . pk qk+1 . . . qn
                        q 0 = q1 . . . qi pi+1 . . . pj qj+1 . . . qk pk+1 . . . pn


   There is no consensus in the GA community about the convenience of choosing
single-point or multipoint crossovers. Empirical results ([Jon75, ECS89]) do not
give conclusive results. Nevertheless, it is accepted that two-point crossover is
better than single-point.
   For a formalization of this multipoint crossover operator, we use the Coq Proof
Assistant. This is an implementation of the Calculus of Inductive Constructions
(CCI), an intuitionistic higher-order logic with dependent types and inductive types
as primitive objects [PM93, CH88]. Coq is both a programming language and a
proof assistant. On the one hand, it allows specifications of programs, and on the
other, permits formalization and verification of mathematical proofs. The user can
introduce definitions and construct proofs in a natural deductive style, which are
mechanically checked/tested/analyzed by the system. Proofs in the Coq system
are constructive, unlike in other systems such as Mizar, HOL or PVS.
   To differentiate computational objects from logical information, two sorts (the
type of a type) of Coq are basically distinguished: the sort P rop for types that



Journal of Formal Reasoning Vol. 1, No. 1, 2008.
Genetic Algorithms in Coq: Generalization and Formalization of the Crossover Operator          ·      27

contain logical terms (the propositions), and the sort Set1 , mainly used to describe
data types and program specifications.
   One of the most attractive aspects of the Coq system is the program extraction.
As a consequence of the Curry-Howard isomorphism, a constructive algorithm of
an object may be “extracted” from the proof of its existence.
   This process removes all logical parts inside terms, preserving only those compu-
tational information parts [PM89].
   In the genetic algorithms context, the formal verification can be used for certify-
ing the correctness of the implementation of some evolutive algorithms and also for
proving properties satisfied by the operators used in genetic programming. More-
over, in a previous work [ADM+ 07], we have formally implemented two crossover
operators specifically designed for problems where the chromosomes are permuta-
tions of a finite list of elements (like in the classical TSP).
   One of the first attempts at the formalization of the foundations of genetic algo-
rithms using a proof system can be found in [UE99].
   Taking this work as an initial point and using the Coq proof assistant, we try
to establish the basis for the formalization of the basic operators in GA (crossover
and mutation) and, at the same time, investigate the formal verification of the
properties satisfied by such operators.
   In the first section, and generalizing the crossover definition that appears in
[UE99], we implement in Coq a first definition of multiple crossover ⊗` , where ` is
any list of natural numbers.
   We prove, in the second section of this work, that for the crossover of two strings p
and q in some points of a list `, we can suppose that ` is in strictly increasing order,
because the crossover determined by two different lists `1 and `2 coincides only if
such lists are the same except perhaps in the order of their elements. This multiple
crossover ⊗` requires a double recursion. That is why we propose in the third
section of this work an alternative and more efficient crossover definition ` (p, q).
We also prove that, if we define, from an increasing ordered list `, the so-called list
of differences, dif `, then the result of both crossover operators coincides; that is:
  (dif `) (p, q) = ⊗` (p, q).

2.   THE MULTIPLE CROSSOVER OPERATOR
Let D be a non-empty and non-unitary finite set. Let p = p1 . . . pm and q = q1 . . . qr
be two finite sequences (chromosomes) of elements of D. We will represent them
in Coq as lists of elements of D (whose set is denoted by (list D))2 . Uchibori and
Endou in [UE99] define the crossover
                            crossover(p, q, n) = p ↑ n + + q ↓ n,
for any pair of lists p and q and any natural number n. Here ++ represent the
concatenation of lists and ↑, ↓ are the operators defined by:

1 Both   sorts P rop and Set being of sort T ype.
2 The   implementation of polymorphic lists in Coq can be found in [INR].




                                                   Journal of Formal Reasoning Vol. 1, No. 1, 2008.
28      ·     Aguado et al.

  Definition 2.1. Let p = (p1 , . . . , pn ) be a finite sequence of elements of D (where
n is the length of p) and m ∈ N. We define:
                                    (
                                       (p1 , . . . , pm ) if m < n,
                         p↑m=
                                       p                  if m ≥ n
                                 (
                                  (pm+1 , . . . , pn ) if m < n,
                            p↓m=
                                  []                   if m ≥ n
where [ ] denotes the empty list.
  Uchibori and Endou also define the crossover in two points, n1 and n2 , as
     crossover(p, q, n1 , n2 ) = crossover(crossover(p, q, n1 ), crossover(q, p, n1 ), n2 )
and repeat this process until the crossover in six points. This construction is gen-
eralized by using the recursive definition of the crossover function presented below
(see Definition 2.2).
  Because each finite list of natural numbers defines a crossover operator (crossover
by this sequence of points), we will call this list a crossover pattern.
  Definition 2.2. Let ` (pattern) be a list of natural numbers, the crossover func-
tion ⊗` : (list D) × (list D) −→ (list D) is defined as:
                        (
                          p                                   if ` = [ ],
            ⊗` (p, q) =
                          (⊗t (p, q) ↑ n) + + (⊗t (q, p) ↓ n) if ` = n :: t
where p and q are elements of type (list D) and n :: t is the list with head n and
tail t.
To specify the previous definitions in Coq and to formally prove their properties,
first, we should declare in Coq the type of data D. As it is a set, we will associate
it with the type Set because, from the point of view of program extraction, Set is
the type of the propositions with constructive content.
Variable D: Set.

   When we define the operators ↑, ↓ and ⊗ in Coq3 , we call them, respectively,
f irst, cutting 4 and crossover (for each list `, ⊗` is the crossover `).
Fixpoint first (m: nat) (p: (list D)){struct p}: (list D) :=
  match m, p with
  | 0, _ => nil
  | _, nil => nil
  | S x, h :: p1 => h :: first x p1
  end.

Fixpoint cutting (m: nat) (p: (list D)){struct p}: (list D) :=
  match m, p with
  | 0, x => x

3 Alldefinitions, lemmas and theorems written in a typewriter font have been formalized in the
Coq system.
4 Note that the functions f irst and cutting are the functions take and drop in Haskell.


Journal of Formal Reasoning Vol. 1, No. 1, 2008.
Genetic Algorithms in Coq: Generalization and Formalization of the Crossover Operator         ·      29

  | _, nil => nil
  | S x, _ :: p1 => cutting x       p1
  end.

Fixpoint crossover (l: list nat) (p q: (list D)){struct l}: (list D):=
  match l with
  | nil => p
  | n :: t => (first n (crossover t p q)) ++ (cutting n (crossover t q p))
  end.

   There are some properties of ↑ and ↓ operators in [DN91, Kot93, UE99] which
are verified using the MIZAR system. Here we have used Coq to (formally) prove
some of these properties and also to obtain some new ones. We begin with technical
results, some of them appearing in [DN91]. Their proofs are obtained by simplify-
ing (beta reduction) and using the implementation of ↑ and ↓ and the recurrence
schemes in Coq. These results will serve to automate later proofs. We include all
of them in the following proposition.
  Proposition 2.3. If p, q ∈ (list D) and n, m ∈ N, it holds that:
—p ↑ 0 = [ ]
—p ↓ 0 = p
—[ ] ↑ n = [ ]
—[ ] ↓ n = [ ]
—If p ↓ 0 = q, then p = q
—length p ≤ n ⇒ (p ↑ n) = p
—length p ≤ n ⇒ (p ↓ n) = [ ]
—(p + + q) ↑ n = (p ↑ n) + + (q ↑ (n − length p))5
—(p + + q) ↑ (length p) = p
—(p + + q) ↑ ((length p) + n) = p + + (q ↑ n)
—n ≤ length p ⇒ (p + + q) ↑ n = p ↑ n
—length p = length q ⇒ length (p ↑ n) = length (q ↑ n)
—length (p ↑ n) = min (n, (length p))
—((p ↑ m) ↑ n) = (p ↑ min(n, m)) = ((p ↑ n) ↑ m)
—(p + + q) ↓ n = (p ↓ n) + + (q ↓ (n − length p))
—n ≤ length p ⇒ (p + + q) ↓ n = (p ↓ n) + + q
—length p ≤ n ⇒ (p + + q) ↓ n = (q ↓ (n − length p))
—length p = length q ⇒ length (p ↓ n) = length (q ↓ n)
—length (p ↓ n) = (length p) − n
—(p ↓ m) ↓ n = p ↓ (n + m) = (p ↓ n) ↓ m
—(p ↑ n) + + (p ↓ n) = p.
—(p ↓ n) ↑ m = (p ↑ (m + n)) ↓ n
—(p ↑ n) ↓ m = (p ↓ m) ↑ (n − m)
—(p ↑ n) ↓ n = [ ]

5 Note   that subtraction n − m in Coq is 0 when n ≤ m.

                                                  Journal of Formal Reasoning Vol. 1, No. 1, 2008.
30     ·     Aguado et al.

   The classical crossover operator used in genetic algorithms works with strings
of the same length. That is why, throughout this paper, we will assume that our
lists of elements of D have this property. First, we prove that, when we apply the
crossover operator to these lists, it preserves the length of the strings. This result
will prove extremely useful in some results afterwards.
  Theorem 2.4. For any ` ∈ (list N) and any p, q ∈ (list D) with length p =
length q, it holds that
                                length (⊗` (p, q)) = length p.
Lemma length_crossover: forall (l: (list nat)) (p q: (list D)),
   length p = length q -> length (crossover l p q) = length p.

  The following theorem guarantees that if two lists `1 and `2 define the same
crossover operator, the result remains true when we add the same list ` at the
beginning of both lists.
   Theorem 2.5. Let p, q be elements of (list D) with length p = length q and let
`, `1 , `2 be elements of (list N). If ⊗`1 (p, q) = ⊗`2 (p, q), then
                              ⊗(`++`1 ) (p, q) = ⊗(`++`2 ) (p, q).
Theorem add_list: forall (l l1 l2: (list nat)), (forall (p q: (list D)),
   length p = length q -> crossover l1 p q = crossover l2 p q) ->
      (forall (p q: (list D)), length p = length q ->
         crossover (l ++ l1) p q = crossover (l ++ l2) p q).

  We include now two theorems which have turned out to be fundamental in the
development of our work. In addition, they generalize all the results concerning the
crossover operator appearing in [UE99].
  Theorem 2.6. Taking ` ∈ (list N) and also p, q ∈ (list D), it can be proven
that:
—⊗(0::`) (p, q) = ⊗` (q, p)
—⊗(0::[ ]) (p, q) = q
—⊗(n::`) (p, q) = ⊗` (p, q), if length p = length q ≤ n.
  Theorem 2.7. Let ` ∈ (list N), n, m ∈ N and p, q ∈ (list D) with length p =
length q. It holds that:
                         ⊗(n :: (m :: `)) (p, q) = ⊗(m :: (n :: `)) (p, q)
and
                              ⊗(n :: (n :: `)) (p, q) = ⊗` (p, q) .
Theorem swap_crossover2: forall (l: (list nat)) (p q: (list D)) (n m: nat),
   length p = length q ->
      crossover (n :: (m ::l)) p q = crossover (m :: (n ::l)) p q.
Theorem elim_rep: forall (l: (list nat)) (p q: (list D)) (n: nat),
   length p = length q -> crossover (n :: (n ::l)) p q = crossover l p q.




Journal of Formal Reasoning Vol. 1, No. 1, 2008.
Genetic Algorithms in Coq: Generalization and Formalization of the Crossover Operator       ·      31

3.   CANONICAL LISTS AND PATTERN CROSSOVER
The multipoint crossover operator used in the GA theory discussed in the Intro-
duction depends on the sites where we are going to cut the strings, but the order
of the points is not relevant. Our crossover operator ⊗` (p, q) also verifies, as a
consequence of 2.5 and 2.7 that, if `1 and `2 are two lists with the same elements,
but in different order, then
                                  ⊗`1 (p, q) = ⊗`2 (p, q),
for any pair of strings p and q of the same length.
   Then, we can always suppose that ` is a list in strictly increasing order, and if
this is not the case, we should reorder its elements. Moreover, 2.7 reveals that the
repeated elements in a list can be eliminated without any change in the result of
the crossover operator.
   So, for any list `, we know that ⊗` (p, q) = ⊗`0 (p, q), `0 being the list obtained
with the same elements of ` but in strictly increasing order and after deleting the
repeated elements two by two. Given any list ` of natural numbers, one of the
objectives of this section is to formally implement in Coq a function that returns
the list `0 which now has the required properties and called the canonical list of `.
   First, we implement in Coq a function that, given ` a list of natural numbers in
strictly increasing order and n a natural number, returns a new list which is also
in strictly increasing order. The following function removes n from ` when n is an
element of ` and inserts n in the right position of ` in other case.
Fixpoint insert_sd (n:nat) (l: (list nat)){struct l}: (list nat):=
  match l with
  | nil => (n :: nil)
  | n1 :: l1 => match lt_eq_lt_dec n n1 with
     |inleft (left _) => n :: l         (* n < n1 *)
     |inleft (right_) => l1             (* n = n1 *)
     |inright _ => n1 :: insert_sd n l1 (* n1 < n *)
                end
  end.

  Now, with this function insert sd, we obtain another function canon that returns
the canonical list of any list `.
Fixpoint canon (l: (list nat)){struct l}: (list nat) :=
  match l with
  | nil => nil
  | n1 :: l1 => insert_sd n1 (canon l1)
  end.

  To obtain a formal proof of certain properties of the lists in strictly increasing
order we need a predicate implementing this concept. The intuitive idea we usually
have about this predicate is “a list where any element is strictly less than the next
one”.
Inductive st_crec: (list nat) -> Prop :=
  | st_crec_nil: st_crec nil
  | st_crec_unit: forall (n: nat), (st_crec (n :: nil))
  | st_crec_cons: forall (n1 n2: nat) (l: (list nat)),
       (n1 < n2) -> st_crec (n2 :: l) -> st_crec (n1 :: n2 :: l).

                                                Journal of Formal Reasoning Vol. 1, No. 1, 2008.
32      ·    Aguado et al.

  As expected, if ` is a canonical list, then ` is a strictly increasing ordered list and
the function canon does not modify the lists with this property.
     Theorem 3.1. Given any ` ∈ (list N) and n, m ∈ N, it follows that:
—(st crec (n :: `)) ∧ (m < n) ⇒ (st crec (m :: `))
—st crec ` ⇒ st crec (insert sd n `)
—The canonical lists are strictly increasing ordered lists.
—st crec ` ⇒ (canon `) = `
  As mentioned previously, the crossover operator defined by ` is exactly the same
as the one defined by its canonical list.
  Now, we have all the ingredients to prove that:
   Theorem 3.2. For ` ∈ (list N), p, q ∈ (list D) of the same length and n ∈ N, it
follows that:
—⊗(insert sd n `) (p, q) = ⊗n :: ` (p, q).
—⊗(canon `) (p, q) = ⊗` (p, q).

Theorem crossover_ins: forall (l: (list nat)) (p q: (list D)) (n: nat),
   length p = length q -> crossover (insert_sd n l) p q = crossover (n :: l) p q.

Theorem crossover_can_eq: forall (l: (list nat)) (p q: (list D)),
   length p = length q -> crossover (canon l) p q = crossover l p q.

     Immediately, we obtain the corollary:
  Corollary 3.3. Take `1 , `2 ∈ (list N) such that (canon `1 ) = (canon `2 ). It can
be proven that
                                    ⊗`1 (p, q) = ⊗`2 (p, q),
for any pair of strings p, q ∈ (list D) of the same length.
Theorem crossover_canon: forall (l1 l2: (list nat)),
   canon l1 = canon l2 -> (forall (p q: (list D)),
      length p = length q -> crossover l1 p q = crossover l2 p q).

  To prove the reciprocate of Corollary 3.3, we need to assume that D is a set
with at least two different elements (this always occurs when we work with genetic
algorithms) and also we need to compare any pair of elements of D. As Coq works
with intuitionistic logic, we must assume the existence of a decidability algorithm
for D. This is going to be a parameter of our specification.
Variable a b: D.

Axiom two_el: ~ (a = b).

Parameter decD: forall d d’: D, {d = d’} + {~ (d = d’)}.

  Making use of the decidability algorithm assumed before, we obtain the proof of
the decidability with respect to the equality of the lists whose elements are in D.
  A result required to achieve our goal is:

Journal of Formal Reasoning Vol. 1, No. 1, 2008.
Genetic Algorithms in Coq: Generalization and Formalization of the Crossover Operator          ·      33

  Theorem 3.4. For any non-empty and strictly increasing ordered list ` ∈ (list N),
we can find two strings p, q ∈ (list D) of the same length such that:
                                       ⊗` (p, q) 6= p
Lemma canon_crossover_lnil: forall (l: (list nat)),
   st_crec l -> ~(l=nil) -> exists p: (list D), exists q:(list D),
      length p = length q /\ ~(crossover l p q = p).

     Now, we can prove:
  Theorem 3.5. For any pair of different lists `1 , `2 ∈ (list N) in strictly increas-
ing order, it is possible to find p, q ∈ (list D) of the same length satisfying:
                                  ⊗`1 (p, q) 6= ⊗`2 (p, q).
Lemma canon_crossover: forall (l1 l2: (list nat)),
   st_crec l1 -> st_crec l2 -> ~(l1=l2) -> exists p: (list D), exists q:(list D),
      length p = length q /\~(crossover l1 p q = crossover l2 p q).

     Finally, the reciprocate of 3.3 is:
  Corollary 3.6. Let `1 , `2 ∈ (list N) be two pairs of lists with canon `1 6=
canon `2 . We can find two strings p, q ∈ (list D) of the same length verifying:
                                  ⊗`1 (p, q) 6= ⊗`2 (p, q).
Lemma cor_canon_crossover: forall (l1 l2: (list nat)),
   ~(canon l1 = canon l2) -> exists p: (list D), exists q:(list D),
      length p = length q /\ ~(crossover l1 p q = crossover l2 p q).

4.       CROSSOVER WITH DIFFERENCES
If we analyze, from a computational point of view, the calculation of the crossover
operator ⊗` (p, q), for any pair of strings p, q, we conclude that it is not very efficient
because, when the list ` is of the form ` = n :: t, we need a double recursion in
t to compute the crossover ⊗` (p, q) (see Definition 2.2). In the previous section,
we have proven that we can always suppose that ` is a list in strictly increasing
order. Now, we propose an alternative definition of crossover, more efficient than
the previous one.
     Definition 4.1. Let ` be any list of natural numbers. The function n crossover
     `: (list D) × (list D) −→ (list D) is defined as:
                              (
                               p                                    if ` = [ ],
                   ` (p, q) =
                               (p ↑ n) + +(   t   (q ↓ n, p ↓ n)    if ` = n :: t
Fixpoint n_crossover (l:list nat) (p1 p2: (list D)){struct l}: (list D) :=
  match l with
  | nil => p1
  | n :: t => (first n p1) ++ (n_crossover t (cutting n p2) (cutting n p1))
  end.

     This new crossover operator also conserves the length of the strings.
   Theorem 4.2. Let ` be any list of natural numbers ` ∈ (list N) and p, q ∈
(list D). If length p = length q, then length ( ` (p, q)) = length p.
                                                   Journal of Formal Reasoning Vol. 1, No. 1, 2008.
34      ·     Aguado et al.

Lemma length_n_crossover: forall (l: (list nat)) (p q: (list D)),
   length p = length q -> length (n_crossover l p q) = length p.

  It is easy to prove that ⊗` (p, q) = ` (p, q), if ` = [ ] or ` = n :: [ ] and n is
any natural number. This is also true in the general case, that is, we take a list
` = {n1 , . . . , nk } in strictly increasing order, and use it to construct another list
called differences list, denoted by dif ` = {n1 , m2 , . . . , mk } with mi = ni − ni−1 ,
for each 2 ≤ i ≤ k. We shall prove that the multiple crossover with pattern ` is the
same as the new one defined with dif `,
                                       ⊗` (p, q) =    (dif `) (p, q).

     To obtain the differences list of `, we implement a recursive function in Coq:
Fixpoint dif_rec (l: (list nat))(n: nat){struct l}: (list nat) :=
  match l with
  | nil => nil
  | n1 :: l1 => (n1 - n) :: (dif_rec l1 n1)
  end.

Definition dif (l: (list nat)) := dif_rec l 0.


  Note that ` must be a strictly increasing ordered list.
  The following auxiliary lemmas are necessary to prove the main result of this
section:
  Lemma 4.3. Let ` ∈ (list N), p, q ∈ (list D) with the same length and n ∈ N
such that (n :: `) is a strictly increasing ordered list. We can prove that
                                   (⊗` (p, q)) ↑ n = p ↑ n.
Lemma first_elem_crossover: forall (l: (list nat)) (p q: (list D)) (n: nat),
   length p = length q -> st_crec (n :: l) -> first n (crossover l p q) = first n p.

  Lemma 4.4. Let ` ∈ (list N), p, q ∈ (list D) with the same length and n ∈ N
such that (n :: `) is a strictly increasing ordered list. It holds that:
                       (dif rec ` n)   (p ↓ n, q ↓ n) = (       (dif `) (p, q))   ↓ n.
 Lemma dif_rec_Dif_crossover: forall (l: (list nat)) (p q: (list D))(n: nat),
    length p = length q -> st_crec (n :: l)->
       n_crossover (dif_rec l n) (cutting n p) (cutting n q) =
              cutting n (n_crossover (dif l) p q).

     Finally, we verify:
  Theorem 4.5. Let p, q ∈ (list D) with the same length and ` ∈ (list N) a strictly
increasing ordered list. It can be proven that:


                                       (dif `)   (p, q) = ⊗` (p, q).
Theorem n_crossover_eq_crossover: forall (l: (list nat)) (p1 p2: (list D)),
   length p1 = length p2 -> (st_crec l) ->
      n_crossover (dif l) p1 p2 = crossover l p1 p2.

     Proof:
     If we proceed by structural induction over the list `, we obtain two cases:
Journal of Formal Reasoning Vol. 1, No. 1, 2008.
Genetic Algorithms in Coq: Generalization and Formalization of the Crossover Operator                           ·     35

(1) If ` = [ ], it follows directly that                   [ ] (p, q)   = p = ⊗[ ] (p, q).
(2) In the case ` = a :: `1 , we have:


                   (dif (a :: `1 ))   (p, q) = p ↑ a + +                  (dif rec `1 a)      (q ↓ a, p ↓ a).
       As the list a :: `1 is in strictly increasing order, by 4.3 we have that:

                                              (⊗`1 (p, q)) ↑ a = p ↑ a.
     Now, if we apply 4.4 and the recurrence hypothesis, we obtain:


             (dif rec `1 a)   (q ↓ a, p ↓ a) = (              (dif `1 ) (q, p))       ↓ a = (⊗` (q, p)) ↓ a
     and then, from the above equalities, it can be proven that:
      (dif (a :: `1 )) (p, q) = ⊗`1 (p, q)) ↑ a + + (⊗`1 (q, p)) ↓ a = ⊗(a :: `1 ) (p, q).

5.     EQUIVALENCE WITH CLASSICAL FORMALIZATION
For genetic algorithms, the classical crossover with one point starts with two strings
(parents) and after the reproduction process obtains two strings (children)6 in the
following way:


                         n    (p, q) = (p ↑ n + + q ↓ n, q ↑ n + + p ↓ n).
     The corresponding implementation in Coq of this operator would be:
Definition crossover_s (n: nat) (t: (list D)*(list D)) :=
   (((first n (fst t)) ++ (cutting n (snd t)),
    ((first n (snd t)) ++ (cutting n (fst t))))).

  In the same way, the multiple crossover with a list of points can be seen as
the composition (sequential concatenation) of the corresponding simple crossover
operators:


                         [n1 ;n2 ;...;nk ]   (p, q) =         n1   (    n2 (. . . (    nk   (p, q))))
or more formally:
  Definition 5.1. If ` (pattern) is any list of natural numbers, we define the crossover
function ` : (list D) × (list D) −→ (list D) × (list D) as:
                                              (
                                                  (p, q)                       if ` = [ ],
                               ` (p, q)   =
                                                  ( n(       t   (p, q)))      if ` = n :: t.
     We implement this function in Coq in the following way:
Fixpoint crossover_m (l: (list nat)) (t: (list D)*(list D)){struct l}:
  (list D)*(list D) :=

6 Usually   in the context of GA the size of the population remains fixed after the reproduction
process.
                                                                   Journal of Formal Reasoning Vol. 1, No. 1, 2008.
36       ·    Aguado et al.

     match l with
     | nil => ((fst t),(snd t))
     | n :: l1 => crossover_s n (crossover_m l1 ((fst t),(snd t)))
     end.

  We include now a result which shows that our crossover definition does not distort
the “classical” crossover operator used in genetic algorithms:
     Theorem 5.2. For any ` ∈ (list N) and p, q ∈ (list D), we have verified that:


                                `   (p, q) = (⊗` (p, q), ⊗` (q, p)).
Lemma equiv_crossover: forall (l: (list nat)) (p q: (list D)),
   (crossover_m l (p,q)) = ((crossover l p q),(crossover l q p)).

6.     CONCLUSIONS AND FUTURE WORK
Starting from Uchibori and Endou [UE99], we develop a generalization of multiple
crossover definitions (in a GA context) and a formally verified implementation of
this operator in a functional programming language. This operator can be directly
used in the implementation of any genetic algorithm. The following objectives have
been achieved:
—The properties of the paper [UE99] and some new ones referring to the generalized
 crossover operator have been formally verified.
—It has been proven that multiple crossover is not related to the order of the points
 where it is applied.
—A more efficient definition of multiple crossover (based on “lists of differences”)
 has been developed and implemented; moreover, its equivalence with the initial
 definition was formally proven.
—And, finally, we introduce a direct definition of multiple crossover closer to the
 concept used normally in GA. We demonstrate its equivalence with the definition
 previously implemented in this paper.
   This work uses the Coq proof assistant and its system of code extraction. Some
of the final results were suggested by the very development of the proofs of some
properties. The required effort for the formalization of the results has allowed to
clarify some points of the proofs. Moreover, in some cases it has also led to a more
detailed proof of the statements.
   The work could be completed in two ways:
—It would be interesting to specify and prove intrinsic properties of the mutation
 operator in Coq. Another point would be to create a GA library in Coq and to
 develop general tactics of automatization in Fields and Ring tactics style which
 would improve the efficiency of the development.
—We are also interested in the formalization of the crossover operator and its
 properties in the PVS system ([COR+ 95]), which would allow us to analyze, in
 a pragmatic way, the similarities and differences existing between both Proof
 Assistants.


Journal of Formal Reasoning Vol. 1, No. 1, 2008.
Genetic Algorithms in Coq: Generalization and Formalization of the Crossover Operator       ·      37

References
[ADM+ 07] F. Aguado, J. L. Doncel, J. M. Molinelli, G. Pérez, C. Vidal, and
          A. Vieites. Certified genetic algorithms: Crossover operators for per-
          mutations. In R. Moreno-Dı́az, F. Pichler, and A. Quesada-Arencibia,
          editors, EUROCAST, volume 4739 of Lecture Notes in Computer Sci-
          ence, pages 282–289. Springer, 2007.
[CH88]    T. Coquand and G. Huet. The calculus of constructions. Inf. Comput.,
          76(2-3):95–120, 1988.
[COR+ 95] J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A tutorial
          introduction to PVS. In Workshop on Industrial-Strength Formal Spec-
          ification Techniques, April 1995.
[DN91]    A. Darmochwal and Y. Nakamura. The topological space E2T. Arcs,
          line segments and special polygonal arcs. Journal of Formalized Math-
          ematics, 3:617–621, 1991.
[ECS89]   L. J. Eshelman, R. A. Caruana, and J. D. Schaffer. Biases in the
          crossover landscape. In Proceedings of the third international conference
          on Genetic algorithms, pages 10–19, San Francisco, CA, USA, 1989.
          Morgan Kaufmann Publishers Inc.
     +
[FHB 98] J. C. Filliâtre, H. Herbelin, B. Barras, S. Boutin, C. Cornes, J. Courant,
          C. Murthy, C. Parent, Ch. Paulin-Mohring, A. Saı̈bi, and B. Werner.
          The coq proof assistant reference manual. Technical report, 1998.
[Hol92]   J. H. Holland. Adaptation in natural and artificial systems. MIT Press,
          Cambridge, MA, USA, 1992.
[INR]     INRIA. The coq standard library. http://coq.inria.fr/library/.
[Jon75]   K. A. De Jong. An analysis of the behavior of a class of genetic adaptive
          systems. PhD thesis, Ann Arbor, MI, USA, 1975.
[Kot93]   J. Kotowicz. Functions and finite sequences of real numbers. Journal
          of Formalized Mathematics, 5:1–4, 1993.
[PM89]    Ch. Paulin-Mhoring. Extraction de programmes dans le calcul des con-
          structions. Thése de doctorat, Université de Paris VII, January 1989.
[PM93]    Ch. Paulin-Mohring. Inductive definitions in the system coq - rules and
          properties. In TLCA ’93: Proceedings of the International Conference
          on Typed Lambda Calculi and Applications, pages 328–345, London,
          UK, 1993. Springer-Verlag.
[UE99]    A. Uchibori and N. Endou. Basic properties of genetic algorithm. Jour-
          nal of Formalized Mathematics, 8:151–160, 1999.




                                                Journal of Formal Reasoning Vol. 1, No. 1, 2008.
