Formal Research Of Crossover Operators Based On Higher-order Logic

With the rapid increase of the scale of computer systems, the correctness of system design is becoming more and more serious. Formal methods have become an important means to solve the problem. Compared with the traditional simulation and test, it has higher reliability and better completeness.Among them, theorem proving method gets more attention, because it can verify the system specification and be not limited by the sizes of systems.Genetic algorithms have been applied to more and more fields with high security requirements. However, there is no formal genetic algorithm in the theorem prover, which limits the application of formal methods in related fields. The study on the formalization of genetic algorithms in HOL4 has important research significance and practical value to extend the application fields of theorem proving systems.It is well known that the crossover operators play a key role in the ability of genetic algorithms. The commonly used crossover operators include one-point and multi-point crossover operator. In this paper, we first formally analyze crossover operators and define their process of generating offspring as crossover operation. Through formal abstraction of crossover operation, a general structured model is presented. Based on the generalized model, a formal model of crossover operation is proposed by using double-recursion method. Then, the formalized crossover operation is used to formalize the one-point and the multi-point crossover operator respectively. Their related properties are proved by using the methods of support for high-level proof steps, rewriting tactics and automated reasoners. Simultaneously, the proofs of the properties of crossover operators guarantee the correctness of the formalized crossover operators. Finally, in order to illustrate the practicability of the formalized crossover operators, two-point crossover operator is applied to genetic algorithm for solving the robot path planning problem.The establishment of the formal model of crossover operation not only enriches the operation functions in HOL4, but also enhances the reasoning ability of HOL4. The formalized crossover operators can be directly applied to any formal implementation of genetic algorithms. The realization of genetic algorithm in robot path planning is completed by using the formalized crossover operator. This work excavates the application potential of formalized crossover operators and provides a effective example for automatic program of genetic algorithm in theorem prover.