My Weblog

Blog about programming and math

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 - Posted by | Agda, Programming | , , ,

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


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

Join 268 other followers

%d bloggers like this: