@@ -0,0 +1,60 @@
1+||| Properties of the Ackermann function.
2+module Data.Nat.Ackermann
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.
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.
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
25+-- There are many variations of the Ackermann function. Here is one
27+-- (see https://sites.google.com/site/pointlesslargenumberstuff/home/2/ackermann)
28+-- that uses nested recursion:
30+ackRec : Nat -> Nat -> Nat
34+ackRec (S k) Z = ackRec k 1
36+ackRec (S k) (S j) = ackRec k $ ackRec (S k) j
38+-- The so-called "base rule" and "prime rule" work together to ensure
39+-- termination. Happily, the Idris totality checker has no issues.
41+-- An unusual "repeating" defintion of the function is given in the
42+-- book The Little Typer:
44+ackRep : Nat -> Nat -> Nat
46+ackRep (S k) = repeat (ackRep k)
48+ repeat : (Nat -> Nat) -> Nat -> Nat
50+ repeat f (S k) = f (repeat f k)
52+-- These two definitions don't look like they define the same
53+-- function, but they do:
55+ackRepRec : (n, m : Nat) -> ackRep n m = ackRec n m
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