Haskell — невозможное возможно?

Известно, что задача определения того, истинна ли некоторая функция 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)) 

Пока, вроде бы, ничего особенного в плане отличий этого типа от обычного Integer.

Вспомним, что мы хотим функцию вида (Nat -> Bool) -> Maybe Nat, результатом которой будет число, на котором поданная на вход функция возвращает True, или Nothing если такого числа нет. Первым приближением может быть, например, подобная функция:

lyingSearch :: (Nat -> Bool) -> Nat lyingSearch f | f Zero = Zero               | otherwise = Succ (lyingSearch (f . Succ)) 

На самом деле, почти очевидно, что в случае существования искомого числа эта функция вернёт верный ответ. Действительно, если f Zero == True, то возвращаемым значением будет Zero — верно. Иначе функция вернёт x+1, где x — значение, на котором истинна функция f(x+1) — тоже верно.
Однако, не зря у этой функции название lyingSearch: в случае, когда искомого числа нет, функция будет на каждом шаге уходить в рекурсию и вернёт, по сути, бесконечность: Succ (Succ (Succ (..., где вложенность никогда не окончится. Из-за ленивости Haskell это — нормальная ситуация. Но ведь бесконечность не является искомым ответом — следовательно в данном случае функция «солжёт».

Что интересно, полностью работающее решение можно сделать на базе приведённой выше функции lyingSearch. Рассмотрим функцию search, определённую так:

search f | f possibleMatch = Just possibleMatch          | otherwise = Nothing     where     possibleMatch = lyingSearch f 

На первый взгляд непонятно, как такое будет работать, и будет ли. Проверим на простых примерах:

ghci> search (\x -> x*x == 16) -- такое работало и для lyingSearch Just (Succ (Succ (Succ (Succ Zero)))) ghci> search (\x -> x*x == 15) Nothing 

То есть, функция search верно определила, что не существует натурального числа с квадратом равным пятнадцати.

На самом деле, если разобраться, то всё просто. Получив от lyingSearch возможный результат (который всегда является допустимым значением типа Nat) мы просто подаём его на вход функции f и проверяем возвращаемое значение. Если искомое число существует, то (как уже выяснено ранее) possibleMatch — как раз это число, и следовательно проверка пройдёт успешно. Иначе, т.к. f завершается для любого входного значения, мы получим False и вернём Nothing.

Функция search действительно работает для любого предиката (функции Nat->Bool), и завершается за конечное время (разумеется, при условии, что f также завершается для любого значения типа Nat). Однако, условие завершения f для любого переданного аргумента очень сильное, и именно оно сильно ограничивает множество допустимых предикатов: например, при f x = x*x + 1 == x будет бесконечный цикл. Казалось бы, что здесь не так, ведь такая функция завершается для любого числа? Оказывается, для любого кроме уже упомянутой бескочности: слева и справа от знака равенства будут бесконечно вложенные Succ (Succ (Succ (..., и соответственно невозможно будет определить, равны ли левая и правая части. Именно по этой причине невозможно использовать данную функцию для создания аналогичной для типа Integer.

Теперь уже можно простыми словами объяснить, почему и каким образом всё работает для всегда завершающихся функций. Ведь если f завершается на переданной ей бесконечности, то есть последовательности Succ (Succ (Succ (..., значит она в любом случае использует (раскрывает) не более некоторого фиксированного числа конструкторов Succ.

Аналогичным по сути способом можно создавать функции вроде search и для других типов. Относительно простым примером также являются действительные числа, представленные каждое в виде бесконечного списка цифр (см. статью Seemingly Impossible Functional Programs). На hackage есть обобщающий пакет infinite-search, который предоставляет соответствующую монаду и сопутствующие функции.

P.S.: эта статья является несколько дополненным «пересказом» Searchable Data Types, поэтому как перевод не помечена.