# My Weblog

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

While following the Agda tutorial, I wrote this code to compute an. 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.

June 12, 2013 -

## 2 Comments »

1. 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 | Reply

• @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 | Reply