From 2800de86e3fcc48047f7523f97ad8c73357b71a8 Mon Sep 17 00:00:00 2001 From: wadler Date: Sat, 30 Dec 2017 14:48:32 -0200 Subject: [PATCH] completed subsection on recursive definitions --- src/Naturals.lagda | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/Naturals.lagda b/src/Naturals.lagda index e17d7c0c..261cafa7 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -4,7 +4,6 @@ layout : page permalink : /Naturals --- - The night sky holds more stars than I can count, though less than five thousand are visible to the naked sky. The observable universe contains about seventy sextillion stars. @@ -233,10 +232,10 @@ one corresponding to zero and one to successor. As well as enabling the above shorthand, the pragma also enables a more efficient internal representation of naturals as the Haskell type -integer. Whereas representing the natural *n* with `zero` and `suc` -requires space proportional to *n*, representing it as an integer in +integer. Representing the natural *n* with `zero` and `suc` +requires space proportional to *n*, whereas representing it as an integer in Haskell only requires space proportional to the logarithm of *n*. In -particular, if `n` is less than 2⁶⁴, it will require just one word on +particular, if *n* is less than 2⁶⁴, it will require just one word on a machine with 64-bit words. @@ -540,12 +539,16 @@ Inluding the lines \end{code} tells Agda that these three operators correspond to the usual ones, and enables it to perform these computations using the corresponing -Haskell operators on the integer type. Whereas representing naturals -with `zero` and `suc` requires time proportional to *m* to add *m* and *n*, -representing naturals as integers in Haskell requires time proportional to -the larger of the logarithms of *m* and *n*. In particular, if *m* and *n* -are both less than 2⁶⁴, it will require constant time on a machine with -64-bit words. Similarly for multiplication and subtraction. +Haskell operators on the integer type. Representing naturals with +`zero` and `suc` requires time proportional to *m* to add *m* and *n*, +whereas representing naturals as integers in Haskell requires time +proportional to the larger of the logarithms of *m* and *n*. In +particular, if *m* and *n* are both less than 2⁶⁴, it will require +constant time on a machine with 64-bit words. Similarly, representing +naturals with `zero` and `suc` requires time proportional to the +product of *m* and *n* to multiply *m* and *n*, whereas representing +naturals as integers in Haskell requires time proportional to the sum +of the logarithms of *m* and *n*. ## Equality is also an inductive datatype