Mechanisation of the AKS Algorithm
- PDF / 844,376 Bytes
- 52 Pages / 439.37 x 666.142 pts Page_size
- 101 Downloads / 215 Views
Mechanisation of the AKS Algorithm Hing Lun Chan1
· Michael Norrish1,2
Received: 15 November 2019 / Accepted: 6 May 2020 © Springer Nature B.V. 2020
Abstract The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result, establishing “PRIMES in P” by a brilliant application of ideas from finite fields. This paper describes an implementation of the AKS algorithm in our theorem prover HOL4, together with a proof of its correctness and its computational complexity. The complexity analysis is based on a conservative computation model using a writer monad. The method is elementary, but enough to show that our implementation of the AKS algorithm takes a number of execution steps bounded by a polynomial function of the input size. This establishes formally that the AKS algorithm indeed shows “PRIMES is in P”. Keywords Theorem-proving · Automated reasoning · AKS algorithm · Number theory · Finite fields computational complexity · Writer monad · Machine model
1 Introduction The AKS algorithm is a decision procedure for primality testing, i.e., given an input number n, it returns “true” if n is prime, and “false” otherwise. The significance of the AKS paper [5], “PRIMES is in P”, is that the number of steps taken by the algorithm is bounded by some polynomial function of the bitsize of n. We present the first complete formalisation of the AKS algorithm. proving its correctness and verifying that it runs in polynomial time. The underlying theories are diverse: from number theory arising from Pascal and Leibniz triangles to abstract algebra concerning finite fields. In order to demonstrate that the algorithm runs in polynomial time, we develop a complexity analysis toolkit using a simple monadic framework, which is adequate for the AKS algorithm and its subroutines. Our contribution consists of: 1. A formal statement of the AKS algorithm, with a correctness proof.
B
Hing Lun Chan [email protected] Michael Norrish [email protected]
1
Australian National University, Canberra, Australia
2
Canberra Research Laboratory, Data61, Canberra, Australia
123
H. L. Chan, M. Norrish
2. A formal implementation of the AKS algorithm, with a correctness proof and an analysis of its run-time complexity, based on a simple machine model. 3. A thorough analysis of basic number-theoretic subroutines suitable for computational complexity studies of algorithms.
1.1 The AKS Algorithm The AKS team first published their algorithm in 2002 [4]. In 2004 [5], they revealed a revised version with a streamlined algorithm: Input: integer n > 1. Output: whether n is PRIME or COMPOSITE. If (n = bm for b ∈ N and m > 1), return COMPOSITE. Find the smallest k satisfying orderk (n) ≥ log n2 . For each (1 < j ≤ k), if 1 < gcd( j, n) < n, return COMPOSITE. If (k ≥ n), return PRIME. For each (c = 1 to (SQRTϕ(k))log n) if (X + c)n ≡ Xn + c (mod n, Xk − 1), return COMPOSITE. 6. return PRIME.
1. 2. 3. 4. 5.
Algorithm 1: The algorithm in AKS revised paper, [5]. Technical details such as orderk (n) ≥ log n2 ,
Data Loading...
