Парсер Хабра: Haskell — невозможное возможно?

пятница, 8 ноября 2013 г.

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, поэтому как перевод не помечена.

This entry passed through the Full-Text RSS service — if this is your content and you're reading it on someone else's site, please read the FAQ at fivefilters.org/content-only/faq.php#publishers. Five Filters recommends: