Известно, что задача определения того, истинна ли некоторая функция Integer -> Bool хотя бы для одного числа вычислительно неразрешима. Однако, нечто, на первый взгляд кажущееся как раз таким оракулом (а именно, функцией (Integer -> Bool) -> Maybe Integer) будет описано в этой статье.
Для начала, зададим свой тип натуральных чисел, практически дословно следуя их обычному математическому определению (почему это нужно будет видно в дальнейшем):
data Nat = Zero | Succ Nat (Eq, Ord, Show)
Другими словами, натуральное число — это либо ноль, либо некоторое натуральное число, увеличенное на единицу (Succ от слова successor).
Также, для удобства, определим основные операции (сложение, умножение, конвертация из Integer) над числами в таком представлении:
instance Num Nat where
Zero + y = y
Succ x + y = Succ (x + y)
Zero * y = Zero
Succ x * y = y + (x * y)
fromInteger 0 = Zero
fromInteger n = Succ (fromInteger (n-1))