FORMALIZATION OF ASYMPTOTIC NOTATIONS IN HIGHER-ORDER-LOGIC

Abstract

Asymptotic notations characterize the limiting behavior of a function. They are extensively used in many branches of mathematics and computer science particularly in analytical number theory, combinatorics and computational complexity while analyzing algorithms. Traditionally, the mathematical analysis involving these notations has been done by paper and-pencil proof methods or simulation, which do not provide accurate results. Due to the enormous usage of computational algorithms in safety-critical domains these days, accuracy of asymptotic analysis has become extremely important. We propose to use Formal meth ods, which is a computer based mathematical analysis technique, to perform asymptotic analysis of algorithms. In order to introduce formal verification in this domain, this thesis provides the higher-order-logic formalizations of O, Θ, Ω, o and ω notations and the formal verification of most of their classical properties of interest. The formalization is based on the theory of sets, real and natural numbers and has been done using the HOL4 theorem prover. To demonstrate the practical usefulness and effectiveness of this formalization, we utilize it to formally analyze the computational complexities of the insertion sort and uniqueness of array elements algorithms. Our formalization bears immense potential for the formal analysis of cryptographic protocols in which the asymptotic notations are used to estimate the size of the key so that it will be infeasible to break a system using given number of steps.