0 | ||| Properties of Ackermann functions
 1 | module Data.Nat.Ack
 2 |
 3 | %default total
 4 |
 5 | -- Primitive recursive functions are functions that can be calculated
 6 | -- by programs that don't use unbounded loops. Almost all common
 7 | -- mathematical functions are primitive recursive.
 8 |
 9 | -- Uncomputable functions are functions that can't be calculated by
10 | -- any programs at all. One example is the Busy Beaver function:
11 | --   BB(k) = the maximum number of steps that can be executed by a
12 | --           halting Turing machine with k states.
13 | -- The values of the Busy Beaver function are unimaginably large for
14 | -- any but the smallest inputs.
15 |
16 | -- The Ackermann function is the most well-known example of a total
17 | -- computable function that is not primitive recursive, i.e. a general
18 | -- recursive function. It grows strictly faster than any primitive
19 | -- recursive function, but also strictly slower than a function like
20 | -- the Busy Beaver.
21 |
22 | -- There are many variations of the Ackermann function. Here is one
23 | -- common definition
24 | -- (see https://sites.google.com/site/pointlesslargenumberstuff/home/2/ackermann)
25 | -- that uses nested recursion:
26 |
27 | ackRec : Nat -> Nat -> Nat
28 | -- Base rule
29 | ackRec Z m = S m
30 | -- Prime rule
31 | ackRec (S k) Z = ackRec k 1
32 | -- Catastrophic rule
33 | ackRec (S k) (S j) = ackRec k $ ackRec (S k) j
34 |
35 | -- The so-called "base rule" and "prime rule" work together to ensure
36 | -- termination. Happily, the Idris totality checker has no issues.
37 |
38 | -- An unusual "repeating" defintion of the function is given in the
39 | -- book The Little Typer:
40 |
41 | ackRep : Nat -> Nat -> Nat
42 | ackRep Z = (+) 1
43 | ackRep (S k) = repeat (ackRep k)
44 |   where
45 |     repeat : (Nat -> Nat) -> Nat -> Nat
46 |     repeat f Z = f 1
47 |     repeat f (S k) = f (repeat f k)
48 |
49 | -- These two definitions don't look like they define the same
50 | -- function, but they do:
51 |
52 | ackRepRec : (n, m : Nat) -> ackRep n m = ackRec n m
53 | ackRepRec Z _ = Refl
54 | ackRepRec (S k) Z = ackRepRec k 1
55 | ackRepRec (S k) (S j) =
56 |   rewrite sym $ ackRepRec (S k) j in
57 |     ackRepRec k $ ackRep (S k) j
58 |