Defining, calculating and reasoning in Higher-Order Logic: Complex and Hypercomplex Analysis and applications

The occasional ambiguity of traditional mathematical notations, and the increasing complexity of proofs, has led to the situation that the use of a proof-verification system is desirable if not, in some situations, unavoidable. Moreover, by merging calculation techniques and proofs, theorem provers also allow a deep interconnection of the three basic mathematical activities, that is, defining, calculating and reasoning. In this thesis we explore such activities from different points of view, dealing with complex and hypercomplex analysis and computability theory using the HOL Light theorem prover. More precisely, the work is divided into four parts, each independent from the others. In the first we report on a formal development of quaternions and their algebraic structure, and we discuss automatic and certified procedures to perform calculations on them. The second part is dedicated to investigate the formalization of possible applications of our framework about quaternions. They are interesting theories on their own and, at the same time, a test for our work. In particular, we formalize basics definitions and theorems about two of the most recent and stimulating theories based on quaternions, that is, ''Slice regular quaternionic functions'' and ''Pythagorean-Hodograph curves''. Slice regular functions extend, in a suitable way, the notion of complex holomorphic function to the quaternionic case whereas, PH-curves are a class of polynomial functions with many theoretical properties and several significant computational advantages in many fields like computer-aided design (CAD), digital motion control, path planning, robotics applications and animation. The main points of the work presented in the first two parts has been published in proceedings of the 8th International Conference on Interactive Theorem Proving in Brasilia 2017. In part three and four we consider computability as a theory on its own. In particular, we focus on two radically different models of computation (but equally important), namely ''Turing Machines'' and ''quantum computing''. We give the basic definitions and we develop two certified systems to simulate computations in such models. Moreover, by implementing the concepts of Turing machines and quantum circuits in HOL Light, we explore these different approaches formalizing some simple different problems they can solve.