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