## Computing a^n using binary representation of natural number in Agda

While following the Agda tutorial, I wrote this code to compute a^{n}. Not very elegant example probably because I am not expert and still learning about dependent types. Maybe after getting some more experience and knowledge, I will try to prove the correctness and complexity of this algorithm. See the post of Twan van Laarhoven about proving correctness and complexity of merge sort in Agda.

module PowerFunction where data ℕ⁺ : Set where one : ℕ⁺ double : ℕ⁺ → ℕ⁺ double⁺¹ : ℕ⁺ → ℕ⁺ add : ℕ⁺ → ℕ⁺ → ℕ⁺ add one one = double one add one ( double x ) = double⁺¹ x add one ( double⁺¹ x ) = double ( add x one ) add ( double x ) one = double⁺¹ x add ( double x ) ( double y ) = double ( add x y ) add ( double x ) ( double⁺¹ y ) = double⁺¹ ( add x y ) add ( double⁺¹ x ) one = double ( add x one ) add ( double⁺¹ x ) ( double y ) = double⁺¹ ( add x y ) add ( double⁺¹ x ) ( double⁺¹ y ) = double ( add ( add x y ) one ) mult : ℕ⁺ → ℕ⁺ → ℕ⁺ mult x one = x mult x ( double y ) = double ( mult x y ) mult x ( double⁺¹ y ) = add x ( double ( mult x y ) ) pow : ℕ⁺ → ℕ⁺ → ℕ⁺ pow one _ = one pow x one = x pow x ( double one ) = mult x x pow x ( double y ) = pow ( pow x y ) ( double one ) pow x ( double⁺¹ y ) = mult x ( pow ( pow x y ) ( double one ) )

Computing 2 ^ 6

pow ( double one ) ( double ( double⁺¹ one ))

double (double (double (double (double (double one)))))

If you have suggestion then please let me know.

Why not ?

pow : ℕ⁺ → ℕ⁺ → ℕ⁺

pow x one = x

pow x ( double y ) = mult ( pow x y ) ( pow x y )

pow x ( double⁺¹ y ) = mult x ( mult ( pow x y ) (pow x y) )

When I read definition of pow I wondered why It has more pattern match rules than mult.

Comment by Divyanshu Ranjan | June 12, 2013 |

@Divyanshu I thought about this but I felt that rather than calling pow x y two times to compute pow x ( double y ), just compute it once and do the squaring ( Probably got this instinct from Haskell if you remember the where keyword. )

Comment by tiwari_mukesh | June 12, 2013 |