michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

completed subsection on recursive definitions

Browse source
This commit is contained in:
wadler 2017-12-30 14:48:32 -02:00
parent 76e9b8e690
commit 2800de86e3
1 changed files with 13 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/Naturals.lagda
View file

@ -4,7 +4,6 @@ layout : page
permalink : /Naturals permalink : /Naturals
--- ---
The night sky holds more stars than I can count, though less than five The night sky holds more stars than I can count, though less than five
thousand are visible to the naked sky. The observable universe thousand are visible to the naked sky. The observable universe
contains about seventy sextillion stars. 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 As well as enabling the above shorthand, the pragma also enables a
more efficient internal representation of naturals as the Haskell type more efficient internal representation of naturals as the Haskell type
integer. Whereas representing the natural *n* with `zero` and `suc` integer. Representing the natural *n* with `zero` and `suc`
requires space proportional to *n*, representing it as an integer in requires space proportional to *n*, whereas representing it as an integer in
Haskell only requires space proportional to the logarithm of *n*. 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. a machine with 64-bit words.
@ -540,12 +539,16 @@ Inluding the lines
\end{code} \end{code}
tells Agda that these three operators correspond to the usual ones, tells Agda that these three operators correspond to the usual ones,
and enables it to perform these computations using the corresponing and enables it to perform these computations using the corresponing
Haskell operators on the integer type. Whereas representing naturals Haskell operators on the integer type. Representing naturals with
with `zero` and `suc` requires time proportional to *m* to add *m* and *n*, `zero` and `suc` requires time proportional to *m* to add *m* and *n*,
representing naturals as integers in Haskell requires time proportional to whereas representing naturals as integers in Haskell requires time
the larger of the logarithms of *m* and *n*. In particular, if *m* and *n* proportional to the larger of the logarithms of *m* and *n*. In
are both less than 2⁶⁴, it will require constant time on a machine with particular, if *m* and *n* are both less than 2⁶⁴, it will require
64-bit words. Similarly for multiplication and subtraction. 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 ## Equality is also an inductive datatype