Pull to refresh

Comments 28

search f | f possibleMatch = Just possibleMatch


Вроде как
possibleMatch :: Maybe Nat
поэтому f possibleMatch не написать

Или я ошибся?


Прошу простить, я ошибся.
А почему нельзя просто пройтись по всем значениям Integer вместо Nat?
Возможных значений Integer бесконечное количество (не принимая во внимание ограниченность памяти, конечно), поэтому за конечное время по всем ним пройти нельзя. Собственно, у Nat тоже бесконечное количество возможных значений, которые также нельзя обойти все, но как видно из этой статьи такой обход не требуется :)
Попытался разобраться, как это работает…

test = a*a == 15
	where
	a = lyingSearch (\x -> x*x == 15)

Возвращает False.

Но как????
В вашем примере lyingSearch возращает бесконечную последовательность Succ'ов, потом вы её возводите в квадрат (лениво) и начинаете сравнивать с конечной последовательностью Succ'ов (с 15-ю). За 15 шагов вы выясняете, что они таки не равны.
Я постарался описать это в статье словами, попробую ещё раз несколько подругому.

В данном случае предикат (\x -> x*x == 15) не выполняется ни для какого x, следовательно a здесь будет равно бесконечности (т.е. бесконечной последовательности Succ (Succ (Succ (...). При умножении такого значения само на себя по определённым для Nat правилам умножения будет лениво получаться такая же последовательность (что логично: inf*inf = inf). Оператор сравнения == также ленивый, и после того как он раскроет 15 вложенных Succ с обеих сторон, слева будет ещё Succ, а справа Zero — они, очевидно, не равны :)

Кстати, бесконечность также можно задать и так: inf = Succ inf. Если в вашем коде вместо a = lyingSearch (\x -> x*x == 15) написать теперь a = inf, результат будет таким же (False).
Хм… Я вижу это так: вы ограничили множество значений Integer неотрицательными числами, а множество операций над рассматриваемым множеством значений операциями +, * и ==. + и * — функции двух аргументов, монотонно возрастающие по обоим аргументам. == — единственная операция из набора, возращающая Bool, при этом, как вы верно отметили, требуется, чтобы хотя бы один агрумент == был конечным числом. Тестируемый предикат имеет тип Nat -> Bool, следовательно, тело предиката может иметь только такой вид: B(C1, ..., Cn), где Ci = fi(x) == ci, B — булевская n-местная функция (выражение с операциями, определёнными над типом Bool), fi(x) — многочлен от x, в котором допустимо только складывать мономы (то есть, монотонно возрастающая функция при условии, что deg f(x) > 0 (deg f(x) — степень многочлена f(x))), ci — некоторое неотрицательное целое.

Ясно, что можно ограничиться предикатом вида f(x) == c, поскольку для проверки утверждения «существует неотрицательное целое такое, что B(C1, ..., Cn)» достаточно проверить то же утверждение для каждого Ci и подставить результаты в B (строго говоря, это не совсем так, поскольку для вычисления предиката C1 && C2 в ложное значение не требуется вычислять C1, если известно, что C2 — ложь, а вычисление C1 может и не завершаться). Тонкости возникают с Ci вида c1 == c2, в котором deg f(x) = 0 и, таким образом, f(x) не является монотонно возрастающей функцией. Оставим, однако, эти детали и рассмотрим случай попроще.

Ответ на вопрос вида «существует ли неотрицательное целое x такое, что f(x) == c, где f(x) — монотонно возрастающая функция?» не стоит и гроша ломанного — вам надо перебирать все x от 0 и далее до тех пор, пока f(x) <= c. Так как f(x) монотонно возрастает и является целочисленной функцией, вычисление завершится не более, чем за (c + 1) шагов перебора. Если оно завершится на равентстве, ответ «да», иначе — «нет». Ровно это, впрочем, реализация и делает — осуществляет поиск за линейное время. Однако нет никакой необходимости при решении такого уравнения использовать линейный поиск — вычислительные методы подскажут вам, что уравнение вида f(x) = c, где f(x) — монотонно возрастающая целочисленная неотрицательная функция, прекрасно решаются итерационными методами за более-менее логарифмическое время. Можно попробовать взять обычный метод итераций xi + 1 = f(xi), где x0 = c или, взяв в качестве первого приближения x, скажем, f( c) / 2, устроить бинарный поиск на отрезке [0, f( c)] (f(x) с нашими ограничениями не может расти медленее линейной функции). Заметьте, что это возможно даже без знаний о том, что f(x) — многочлен. Если они есть, то мы знаем, как его дифференцировать, и дело вообще сводится к тривиальному методу Ньютона. О деталях, впрочем, не хочу здесь ничего говорить.

Достоинство предлагаемого в этой статье подхода только в элегантном решении частных случаев (отмеченных в конце второго абзаца), которое выезжает на ленивой модели вычислений Haskell. Однако производительность описанного подхода, ясно, удручающая. Вам банально для хранения неотрицательного целого n нужно O(n) памяти, в общем случае — это катастрофа.

Более того, я не вижу преимуществ и в выразительности такого решения и его простоте — магия, предложенная в статье, требует серьёзных разбирательств, ограничения, которые она накладывает на входные параметры, не очевидны с первого взгляда. Реализация соответствующего алгоритма на C, например, во-первых, намного проще и очевиднее, во-вторых, накладывает видимые невооружённым взглядом ограничения на входные параметры, в-третьих, асимптотически эффективнее и по памяти, и по времени работы, в-четвёртых, является уже давным-давно реализованным в десятке математических библиотек вдоль и поперёк изученным алгоритмом вычислительных методов.
А вообще грустно мне. Я люблю и ценю функциональный подход. Но до тех пор, пока разработчики будут убивать, вероятно, по целому рабочему дню на исследование и описание конструкций, выразимых на их любимом функциональном языке, которые решают наново сто лет назад решённую задачу, но не за константу по памяти и логарифм по времени, а за линейное время и с линейным потреблением памяти, промышленность будет продолжать говорить своё «фииии» функциональному подходу — и будет права.
Мне, если честно, совершенно не важно, что «промышленность» будет говорить функциональному подходу, и тем более моей целью не является популяризация этой парадигмы. В промышленном программировании и многие разделы математики (в том числе и из computer science) не используются например, но это же не значит что они не нужны. Вот и здесь этот пример стоит рассматривать не как что-то, что нужно бежать и применять в «промышленности».
Худшие решения уже решённых задач не ценятся не только в промышленности, но и в математике.
Увы, тут я абсолютно не могу согласиться. Решение уже решённой задачи с другой стороны, абсолютно другим подходом, пусть и менее эффективное сначала, может дать почву для дальнейших обобщений. Как раз в данном случае описанная реализация содержит ту же идею, что и упомянутая мной уже пару раз статья Seemingly Impossible Functional Programs (см. также ссылки в конце неё). Я бы не сказал, что всё это можно тривиально свести к бинпоиску или методу Ньютона.

Кстати, вот мне интересно, какого вы мнения о создателе языка brainfuck например? :) Решение уже решённых задач, причём явно не лучшее.
brainfuck — никому не нужная поделка. Машина Тьюринга — красивая и чрезвычайно полезная (для теории вычислимости, наверное, в первую очередь) конструкция. Я полагаю, что полезно отделять вещи, неприменимые в промышленности сегодня — и вещи, неприменимые нигде, даже в самой экзотической теории. Это не одно и то же.

А линейным перебором уравнения тоже уже решали, ничего нового и тут нет. Никакого «абсолютно другого подхода» я не вижу.
Всю теорию из этого поста можно пересказать в одном предложении: «на компактных функциях можно определить оператор равенства». А заголовок несколько «жёлтый»; впрочем, как и у Seemingly Impossible Functional Programs. Я согласен с вами, что конкретно этот раздел теории сравнимости функций не очень интересен ни с какой точки зрения.

А brainfuck — поделка крайне нужная. Большинство людей, мне кажется, о машине Тьюринга узнают именно через него.
Всю теорию из этого поста можно пересказать в одном предложении: «на компактных функциях можно определить оператор равенства».

Можно то оно можно, только вот люди, не изучающие топологии или что-то типа функана мало что поймут из такой формулировки :)
Я прошёл семестр топологии и сейчас слушаю курс функана. Я не очень понял, что именно хотел сказать ArtyomKazak
Вычислимые (=непрерывные) функции из компактного пространства (в статье это компактификация натуральных чисел, в примере с действительными числами это канторово множество) в пространство с дискретной топологией (здесь это множество {True,False}) равномерно непрерывны (=их можно вычислимым образом сравнивать на равенство/неравенство).

Вроде так, но на 100% точность формулировок не претендую.
Прошу прощения; судя по всему, я и впрямь сказал какую-то лабуду. Я ориентировался на ответ с StackOverflow, недопоняв его смысл.

Upd: а может, и не совсем лабуду. Спачибо chersanya за развёрнутое объяснение.
Я полагаю, что полезно отделять вещи, неприменимые в промышленности сегодня — и вещи, неприменимые нигде, даже в самой экзотической теории. Это не одно и то же.

Это бы было верно и полностью справедливо, если бы существовал критерий по которому можно сказать, что некоторая конкретная вещь «неприменима нигде, даже в самой экзотической теории», и причём никогда не будет применима. В нашем же мире такого критерия не сущетсвует.

А вообще эта ветка дискуссии скатилась в некое философствование, и я не совсем понимаю, что же всё-таки вы хотите здесь показать.
что же всё-таки вы хотите здесь показать


Давайте считать, что я хочу показать это: ценность вашей статьи (особенно учитывая, что частично она просто перевод) возрастёт значительно, если в ней появится чёткая формулировка, какую же именно задачу решает описываемый подход, и исчезнет попытка убедить неискушённого читателя, что эта задача 1) близка неразрешимой проблеме 2) решена здесь неким новым, неизвестным ранее способом.
Тогда статья станет не такой завлекательной. Возможно, ценность её ещё и упадёт.
Дело не только в том, что получилось «худшее решение уже решенной задачи», но и в том, что вообще непонятно, что получилось. Для некоторых функций search работает, для других нет. Для каких? Это в статье не сказано. ramntry приводит некий класс функций. Это в точности тот класс для которого search возвращает правильное значение? (Нет. hint: omega :: Nat; omega = fix Succ). Как говорил Дейкстра, "[they] derive their intellectual excitement from not quite knowing what they are doing".

PS: в определении Nat пропущено deriving.
но и в том, что вообще непонятно, что получилось.

Отлично сказано, на мой взгляд

За цитату отдельное спасибо
Для некоторых функций search работает, для других нет. Для каких? Это в статье не сказано.


Вообще-то сказано, что достаточно чтобы функция завершалась для любого переданного аргумента — достаточно логичное требование, не так ли? Да, это условие не необходимое (например, для функции возвращающей True для нуля и зацикливающейся для всех других аргументов всё сработает верно), но в данном контексте не кажется полезным рассматривать незавершающиеся функции.
Не совсем понятно, что значит условие «достаточно чтобы функция завершалась» в контексте, в котором незавершающиеся функции не рассматриваются. В любом случае, условие «f завершается» не сильно отличается от условия «search завершается», однако последнее бесполезно.
Если честно, не совсем понял вашу мысль в этом сообщении.

Я имел в виду, что для любой функции f, которая всегда завершается, функция search также будет завершаться — т.е. она работает. Никаких других условий на f не накладывается. Другие же функции f (т.е. те, которые не завершаются) не вижу смысла здесь рассматривать.
А вам прям нужно, чтобы всё прочитанное можно было бы сразу применить на практике? :) По поводу же оптимизации, в упомянутой статье Seemingly Impossible Functional Programs рассматривается реализация для действительных чисел (=последовательностей бит), и проводятся значительные оптимизации. Если разбираться досконально, то там материала может и не на одну ещё статью набраться. Несмотря на то, что я всё равно прямо сейчас не знаю, куда это можно было бы применить «в промышленности», выглядит красиво :)
Ну а здесь (в этой статье) я описал простейший для реализации и понимания случай, чтобы любой желающий мог разобраться.
С более-чем-годовой задержкой попробую ответит, в чём я вижу красоту этого решения поставленной задачи. Речь идёт о подходе, который естественен для Хаскелля и может быть воспроизведён односвязными списками на любом другом ЯП (не без сложностей).

Поставлена задача написать функцию (Nat -> Bool) -> Maybe Nat.
Если вообще никаких ограничений на функцию Nat -> Bool не накладываются, задача неразрешима, поскольку (неформально говоря) за конечное время возможно проверить только конечное число вариантов, а никаких других способов пощупать эту функцию у нас нет.
Допустим, на функцию накладываются какие-то ограничения. Допустим, как ramntry предложил, её можно декомпоновать на примитивные равенства f(x)==c. Для такого класса функций существует алгоритм, использующий эти параметры c, который позволяет за менее-чем-линейное время с постоянной памятью найти ответ. Однако какой тогда должна быть сигнатура функции?

Недостаток эффективного подхода заключается в том, что для каждого класса функций, которые представляются в определённом параметрическом виде, нужно писать свой собственный алгоритм, который зависит от всех параметров функции и от всех других особенностей, знания о которых нужны алгоритму для решения поставленной задачи. Не возможно написать решатель (Nat -> Bool) -> Maybe Nat, который бы использовал один из этих целевых алгоритмов, потому что такой решатель не будет иметь информации о «скрытых параметрах» функции.

Один из способов обойти этот недостаток заключается в передачи всех параметров вместе с функцией. В любом случае появление нового класса функций, для которых задача может быть решена, приводят к необходимости переписывать всё либо жертвовать универсальностью решателя и создавать новую функцию.

Как бы то ни было, предложенная в статье функция способна решить задачу на весьма широком диапазоне функций, будучи универсальной и сравнительно простой. Такие неэффективные, но простые и универсальные решатели всегда занимают свою нишу: когда нужно быстро написать надёжный простой код, который хотя бы когда-нибудь выдаст правильный ответ с использованием сколько-угодно дополнительных ресурсов, чтобы использовать его едино- или несколькоразово.
Sign up to leave a comment.

Articles