Неподвижная точка

[ermouth]

У меня впервые выплыла серьёзная задачка, в решении которой я применил понятие из сабжа – этот факт стоит зафиксировать. Раньше всякие там красивые понятия типа y-combinator или теорема Банаха были просто такими интересными зверьками. Ну, дожили вот )

Неподвижная точка функции это например вот что. Если взять калькулятор, набрать на нём какое-то число и много раз подряд нажимать на кнопку cos, в какой-то момент число меняться перестанет (либо начнёт колебаться на 1 в последнем разряде из-за округления).

Вот это число и будет неподвижной точкой той конкретной реализации взятия косинуса в вашем калькуляторе.

В реальной жизни мне это понадобилось в неожиданном месте – для валидации данных jQuery.my-форм на сервере с помощью описания самой формы.

Дело в том, что описание формы jQuery.my не содержит валидатора конечных данных – там есть только

1. функции-связыватели полей ввода и данных (“свяжи значение из поля ввода "Год” с ячейкой памяти data.year”) в обе стороны
2. валидаторы полей ввода (не данных)
3. указатели зависимостей (мы явно говорим, после изменения каких полей какие ещё поля надо заново проверять и пересчитывать)
4. ограничители на максимальную глубину связывания зависимостей (для избежания бесконечных циклов когда А зависит от Б, и Б – от А)

То-есть когда форма уже нарисована на экране, всё понятно. А вот когда она на сервере и никакой html-странички, в которой форма нарисована, нет – что делать не очень ясно было в общем случае.

Поля ввода совершенно не обязательно содержат данные в том же виде, в каком они хранятся в памяти. Ну то-есть дату нам удобнее вводить как 10-5-2012, а вот хранить её надо как 2012-05-10. Также возможно объединение полей – когда например отдельно вводятся год и выбирается месяц-день (3 поля ввода), а хранится всё в одной ячейке date в формате как в примере выше.

Получается, что у нас есть три функции отображения данных в памяти на поля ввода (назовём их getter_n – нижний индекс это “номер” поля), три функции отображения обратно (setter_n) и три валидатора полей ввода (ok_n). Валидаторы или передают полученное на вход дальше, или останавливают вычисления с ошибкой.

Задача звучит так: как в общем случае, имея только эти функции и валидаторы-ограничители, проверить корректность данных в памяти. То-есть, как имея функцию отображения и результат, определить, мог ли быть получен такой результат из этой функции.

Она, задачка эта, неожиданно – а я давно над ней думаю – решается в одно соображение.

В общем случае данные верны, если они являются неподвижной точкой для цепочки отображений setter_n(ok_n(getter_n())) по всему графу зависимостей, развёрнутому в дерево ограниченной глубины.

По-русски это так. Если проделать все вызовы в той же очерёдности, включая зависимости, по той же схеме, что их делает jQuery.my, данные после всех вычислений должны совпасть с исходными данными и ни одно вычисление не должно вернуть ошибку.

С точки зрения практической реализации здесь куча технических моментов и пограничных случаев, но они все преодолимы.

Есть проблема и покруче – нужно обеспечить идентичный scope для функций на клиенте и на сервере. Эта задача в лоб неразрешима в принципе в общем случае, так что тут надо исхитряться и её ослаблять-переформулировать.

Наилучшая переформулировка – как обеспечить создание таких форм, в которых валидаторы и байндеры работают в контролируемом scope (не лезут там в глобальные переменные, не пытаются провалидировать данные, сравнивая их с текущим временем и тп).

Эта задачка решаема – она административная, а не математическая.

Такое вот зауми псто, ога.

Comments

[rezkiy.livejournal.com]

замечу, что с косинусом у тебя не просто неподвижная точка, а устойчивая неподвижная точка.

[morfizm.livejournal.com]

Я думаю, эта задача в принципе не решаема, если ты не ограничишь очень строго domains (типы данных, скажем, тип "год" и допустимый интервал) и не ограничишь возможные преобразования для связанных ячеек каким-то конкретным и не очень большим набором функций.

Если между одной ячейкой (скажем, a="год" из множество годов A) и другой, скажем (b="полная дата" из множества дат B), установлены два соответствия: f: B x A -> B (пересчитывает полную дату, используя то, что там уже было плюс значение года), и g: A x B -> A, то, по сути, тебе хочется доказать, что если год успешно провадилирован, то после соответствующего изменения полной даты, и попытки обратно вычислить год, он не изменится. Т.е. ok(a) => g(f(a))=a.

Поди попробуй *автоматически* докажи это для произвольных функций, вроде "g(x) = число, составленное из подряд идущих десятичных цифр начиная с позиции 1000 из корня кубического из x, вплоть до ближайшей последовательности 1234, где x любое натуральное число".

Это даже не возможно автоматически протестировать, т.к. "x любое натуральное число". Причём за заумными примерами далеко ходить не надо, достаточно работать не с числами из ограниченного диапазона, а со строками, скажем, имя-фамилия, или кусочки адреса. Задолбаешься.

Если же ты будешь поддерживать сложные связанные вычисления (не-копирование) только очень ограниченного вида, вроде кусочек даты копируется в сборную дату, или строка копируется в подстроку в позициях таких-то, то это становится выполнимо.

[morfizm.livejournal.com]

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

[ermouth.livejournal.com]

Она неразрешима, потому что ты решаешь не ту задачу. Ты её даже формулируешь не совсем верно.

Ты пытаешься автоматически доказать вычислимость и, вообще говоря, остановку произвольно взятых функций (ну то-есть программ). Ни то, ни другое невозможно в общем случае.

Проблему остановки (например, прямое отображение меняет порядок букв в строке на обратный, а обратное просто копирует строку) я решаю ограничением возможной глубины рекурсии, это обозначено в условиях, так и формы работают.

Проблема вычислимости в моём случае редуцирована до "вычислимость за заранее определённое время" – это не совсем корректно, но это лучше чем ничего.

Моя задача – убедиться в том, что когда пользователь нажимал Send у него ничего там красным не горело. Ты решаешь задачу доказательства правильности программы – это невозможно просто.

[ermouth.livejournal.com]

о, сорри, не прочитал этот коммент.

[morfizm.livejournal.com]

Если тебе заранее дано, что форма корректна, то ты можешь добавить дополнительное условие для человека-дизайнера-форм:

1. В случае, если валидация ячейки прошла успешно, т.е. ok_n(form_value_n), то гарантируется, что все взаимосвязанные ячейки пересчитаются в некоторое корректное для них значение. Т.е. тебе не нужно полагаться на цепочку "необходимых, но, возможно, не достаточных" условий, а твои условия на каждое поле всегда "достаточные".

2. В случае ok_n(form_value_n), гарантируется, что getter_n(setter_n(form_value_n)) = form_value_n.

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

4. Не позволять убирать фокус с элемента, если значение в нём неправильное. Т.е. в любой момент времени неправильным может быть только одно значение, которое пользователь сейчас вводит.

С этими условиями, поддерживать корректность формы - тривиально: при вводе проверяешь ok_n(form_value_n), и если оно верно, пересчитываешь все взаимосвязи простым обходом дерева в глубину (граф тривиальным образом превращается в дерево - можно помнить уже посещённые вершины и не идти по рёбрам, которые создадут цикл).

Как видишь, никакими неподвижными точками заморачиваться не пришлось.
Send disabled если not ok() для поля в фокусе и enabled в другом случае.

Что ты думаешь?

[ermouth.livejournal.com]

1. Слабая посылка. Если ты уже ввёл год, но не ввёл месяц-день, год будет корректен, а месяц-день – нет, и угадать какими они должны быть никак не получится. То-есть твой подход очень сильно ограничит.

2. Гарантируется не на атомарном цикле вычислений, а после всех вычислений – почуствуй разницу. Чтобы понятнее – см п.1

3. ок

4. это делать нельзя, просто нельзя. во-первых, не для всех элементов существует понятие "фокус". Во-вторых, см п.1. В-третьих, это скотство с точки зрения ux в большинстве случаев, потому что в простонародье такой сценарий называется "квест" )

[ermouth.livejournal.com]

Я знаю, как такой дизайнер форм (валидатор) сконструировать – книжка про HoTT даёт весь набор необходимых и достаточных условий по допустимым структурам данных и определённым на них функциям.

Это не очень то жесткие ограничения оказались, напишу пост.