если вы написали две функции, которые определены на бесконечном множестве, то кажется очевидным, что нельзя написать программу, которая только применяя эти функции (не имея доступа к их коду) проверит за конечное время, равны ли они (в математическом смысле: совпадают ли они во всех точках) — и всё же иногда это возможно!
функции мы будем рассматривать на множестве Кантора, т.е. на бесконеных последовательностях 0 и 1
т.к. мы пишем программу — и функции на последовательностях, и сами последовательности у нас будут, конечно, только вычислимые; кроме того, они будут всюду определенные (можно написать
type Cantor = Natural -> Bit, но надо иметь в виду, что если такая функция для числа 17 не определена, то она не задает элемент множества Кантора)мы хотели бы сравнить две функции из Cantor, т.е., если угодно, написать функцию
equal :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool (здесь написано, что если для типа y определено сравнение, то equal сравнивает две функции Cantor→y)если функции НЕ равны, то это уж точно можно понять за конечное время, т.к. любые вычислимые функции на Cantor зависят только от какого-то числа первых битов — это проявление компактности канторовского множества, из-за которой любая непрерывная функция на нем равномерно непрерывна (ср. с натуральными числами, где легко придумать вычислимую функцию которая никаким фиксированным количеством первых битов не определяется!)
но, на первый взгляд, если функции равны, то невозможно понять, до какого момента надо их сравнивать
и всё же можно за конечное время установить не только неравенство, но и равенство:
data Bit = Zero | One
deriving (Eq)
type Natural = Integer
type Cantor = Natural -> Bit
(#) :: Bit -> Cantor -> Cantor
x # a = \i -> if i == 0 then x else a(i-1)
forsome :: (Cantor -> Bool) -> Bool
find :: (Cantor -> Bool) -> Cantor
forsome p = p(find p)
find p = first # find(p . (first #))
where first = if forsome(p . (Zero #)) then Zero else One
equal :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool
equal f g = not(forsome(\a -> f a /= g a))
здесь функция forsome проверяет, существует ли точка множества Кантора, в которой верно p (что само по себе не менее удивительно, чем проверка равенства функций… и собственно через такой «бесконечный поиск за конечное время» равенство мгновенно переписывается), а find находит точку, в которой верно p, если таковая есть
при этом определение find через forsome крайне прямолинейное: «если существует пример с первым битом 0, то первый бит равен 0, иначе первый бит равен 1 (а дальше применяем find для определения оставшихся битов)»… и кажется, что пока ничего особо не сделано — но вот такое короткое (и вроде бы тоже довольно тавтологичное) определение forsome чудесным образом позволяет “вытянуть себя за волосы из болота”
мб позже будет комментарий, как это работает — но сразу оставлю ссылку на источник — Martin Escardo по диссертации Ulrich Berger'а; и спасибо коллеге Раскину за объяснения
хочу еще отметить, что это история не про хаскелл, можно напрячься и на питоне (например) переписать — но тут приятно, что синтаксис хорошо соответствует (некоторой) математике