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