посмотрим еще раз на определение
forsome p = p(find p)(напомню, что p это функция из бесконечных последовательностей нулей и единиц в True/False, а функция forsome должна проверять, выполняется ли p хоть в какой-то точке)
в одной ситуации всё понятно сразу: если p определена как константа (вообще не читает свой вход, а возвращает True или False), то ленивый компилятор даже вникать в определение find не будет, а вернет эту константу — и в этом случае forsome работает правильно
пусть теперь p для возвращения значения достаточно прочитать первые N битов последовательности — будем доказывать индукцией по N, что правильно работают и forsome, и
find p = frst # find(p.(frst#))
where frst = if forsome(p.(0#)) then 0 else 1(напомню, что find должен возвращать пример точки, в которой p верно, если такая точка есть; # обозначает конкатенацию)
функция
p.(0#) в точке x₁ x₂… возвращает p(0 x₁ x₂…) — поэтому ей достаточно прочитать N-1 бит икса — поэтому если p выполняется для какой-либо последовательности, начинающейся с нуля, то frst=0 и find p возвращает правильный первый бит по предположению индукции для forsome… а остальные биты возвращает правильные по предположению индукции для find (оставшиеся подробности индукции опущу)наконец, для любой вычислимой всюду определенной функции p такое N, что p для ответа достаточно первых N битов последовательности, непременно существует — и это топологическое утверждение: проявление компактности множества Кантора (и вот для функций на натуральных числах aka конечных последовательностях 0 и 1 такое свойство очевидно неверно!)
***
после таких фокусов возникают в голове волшебные картины… вот например: если мы умеем проверять равенство функций в смысле совпадения во всех точках — то можно, казалось бы, для одной задачи написать медленный, но точно правильный алгоритм, а дальше любой другой алгоритм решения той же задачи автоматически верифицировать
и в принципе, действительно, можно, но есть две проблемы
первая — что «всюду определенные функции на множестве Кантора» это довольно узкий и бесполезный класс функций… ну вот по тому, что функция p всегда читает не более N(p) битов уже понятно, что ничего особо интересного так реализовать нельзя, правда же?
вторая — что никакой магии на самом деле нет: вот как реализовать forsome без возвышенных слов и хаскелловских трюков? ну вот p ест поток из единиц и нулей… ждем пока p попросит первый бит, после чего одной копии p даем 0, а другой копии даем 1… если p после этого вернула значение, то понятно, что делать… если не вернула, а просит еще бит, то одной копии дали 00, одной 01… и так далее — компактность (сорри, совсем без слов не обошлось ) гарантирует, что рано или поздно это закончится
видно только, что закончится не очень быстро: мы просто перебираем 2^N двоичных последовательностей… в исходном варианте еще и довольно неэффективно всё организовано — но даже если доработать (в блог-посте по прошлой ссылке обсуждаются варианты), то по сути наша магическая проверка корректности алгоритма сводится к тому, что «всё определено на конечном множестве, ну вот на каждой точке этого конечного множества и сравниваем значение с табличным»
и всё-таки если не в самом алгоритме, то в том, как он описан, я какую-то магию вижу… и еще нравится ощущение, что ghci компилирует практически непосредственно математические определения (более опытные люди пишут, правда, что это очень misleading ощущение )