Processing math: 0%

Exponentiation

Posted on 2017-04-14 by nbloomf
Tags: arithmetic-made-difficult, literate-haskell

This page is part of a series on Arithmetic Made Difficult.

This post is literate Haskell; you can load the source into GHCi and play along.


{-# LANGUAGE NoImplicitPrelude #-}
module Exponentiation
  ( power, _test_power, main_power
  ) where

import Testing
import Booleans
import NaturalNumbers
import SimpleRecursion
import Plus
import Times

We defined \ntimes as iterated addition; similarly, exponentiation is iterated multiplication. We’ll call this function \npower.

Define \varphi : \nats \rightarrow \nats by \varphi(a) = \next(\zero), and define \mu : \nats \times \nats \times \nats \rightarrow \nats by \mu(k,a,b) = \ntimes(b,a). We define \npower : \nats \times \nats \rightarrow \nats by \npower(a,b) = \simprec(\varphi)(\mu)(b,a).

In Haskell:

Because \npower is defined in terms of simple recursion, it is the unique solution to a system of functional equations.

\npower is the unique map f : \nats \times \nats \rightarrow \nats with the property that for all a,b \in \nats, we have \left\{\begin{array}{l} f(a,\zero) = \next(\zero) \\ f(a,\next(b)) = \ntimes(f(a,b),a). \end{array}\right.

Some special cases.

Let a \in \nats. Then we have the following.

  1. \npower(a,\next(\zero)) = a.
  2. \npower(\zero,\next(a)) = \zero.
  3. \npower(\next(\zero),a) = \next(\zero).
  1. We have \begin{eqnarray*} & & \npower(a,\next(\zero)) \\ & = & \ntimes(\npower(a,\zero),a) \\ & = & \ntimes(\next(\zero),a) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-one-left} = & a \end{eqnarray*} as claimed.
  2. We have \begin{eqnarray*} & & \npower(\zero,\next(a)) \\ & = & \ntimes(\npower(\zero,a),\zero) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-zero-right} = & \zero \end{eqnarray*} as claimed.
  3. We proceed by induction on a. For the base case, we have \npower(\next(\zero),\zero) = \next(\zero). For the inductive step, suppose \npower(\next(\zero),a) = \next(\zero). Now \begin{eqnarray*} & & \npower(\next(\zero),\next(a)) \\ & = & \ntimes(\npower(\next(\zero),a),\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-one-right} = & \npower(\next(\zero),a) \\ & = & \next(\zero) \end{eqnarray*} as needed.

And interaction with \nplus and \ntimes.

Let a,b,c \in \nats. Then we have the following.

  1. \npower(a,\nplus(b,c)) = \ntimes(\npower(a,b),\npower(a,c)).
  2. \npower(a,\ntimes(b,c)) = \npower(\npower(a,b),c).
  3. \npower(\ntimes(a,b),c) = \ntimes(\npower(a,c),\npower(b,c)).
  1. We proceed by induction on c. For the base case c = \zero, note that \begin{eqnarray*} & & \npower(a,\nplus(b,c)) \\ & = & \npower(a,\nplus(b,\zero)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-zero-right} = & \npower(a,b) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-one-right} = & \ntimes(\npower(a,b),\next(\zero)) \\ & = & \ntimes(\npower(a,b),\npower(a,\zero)) \\ & = & \ntimes(\npower(a,b),\npower(a,c)). \end{eqnarray*} For the inductive step, suppose the equality holds for some c \in \nats. Now \begin{eqnarray*} & & \npower(a,\nplus(b,\next(c))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \npower(a,\next(\nplus(b,c))) \\ & = & \ntimes(a,\npower(a,\nplus(b,c))) \\ & = & \ntimes(a,\ntimes(\npower(a,b),\npower(a,c))) \\ & = & \ntimes(\npower(a,b),\ntimes(a,\npower(a,c))) \\ & = & \ntimes(\npower(a,b),\npower(a,\next(c))) \end{eqnarray*} as claimed.
  2. We proceed by induction on c. For the base case c = \zero, note that \begin{eqnarray*} & & \npower(a,\ntimes(b,c)) \\ & = & \npower(a,\ntimes(b,\zero)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-zero-right} = & \npower(a,\zero) \\ & = & \next(\zero) \\ & = & \npower(\npower(a,b),\zero) \\ & = & \npower(\npower(a,b),c). \end{eqnarray*} For the inductive step, suppose the equality holds for some c. Now \begin{eqnarray*} & & \npower(a,\ntimes(b,\next(c))) \\ & = & \npower(a,\nplus(b,\ntimes(b,c))) \\ & = & \ntimes(\npower(a,b),\npower(a,\ntimes(b,c))) \\ & = & \ntimes(\npower(a,b),\npower(\npower(a,b),c)) \\ & = & \npower(\npower(a,b),\next(c)) \end{eqnarray*} as claimed.
  3. We proceed by induction on c. For the base case, we have \begin{eqnarray*} & & \npower(\ntimes(a,b),c) \\ & = & \npower(\ntimes(a,b),\zero) \\ & = & \next(\zero) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-one-left} = & \ntimes(\next(\zero),\next(\zero)) \\ & = & \ntimes(\npower(a,\zero),\npower(b,\zero)) \\ & = & \ntimes(\npower(a,c),\npower(b,c)). \end{eqnarray*} For the inductive step, suppose the equality holds for some c. Now \begin{eqnarray*} & & \npower(\ntimes(a,b),\next(c)) \\ & = & \ntimes(\ntimes(a,b),\npower(\ntimes(a,b),c)) \\ & = & \ntimes(\ntimes(a,b),\ntimes(\npower(a,c),\npower(b,c))) \\ & = & \ntimes(\ntimes(a,\npower(a,c))\ntimes(b,\npower(b,c))) \\ & = & \ntimes(\npower(a,\next(c)),\npower(b,\next(c))) \end{eqnarray*} as claimed.

Testing

Suite:

_test_power ::
  ( TypeName n, Natural n, Equal n, Arbitrary n, Show n
  ) => Int -> Int -> n -> IO ()
_test_power size cases n = do
  testLabel1 "power" n

  let args = testArgs size cases

  runTest args (_test_power_zero_right n)
  runTest args (_test_power_next_right n)
  runTest args (_test_power_one_right n)
  runTest args (_test_power_zero_left n)
  runTest args (_test_power_one_left n)
  runTest args (_test_power_plus_right n)
  runTest args (_test_power_times_right n)
  runTest args (_test_power_times_left n)

Main:

main_power :: IO ()
main_power = do
  _test_power 4 30 (zero :: Unary)