Comments 20
Я с функциональщиной не особо знаком, поэтому извините за возможно тупой вопрос, но
Зачем ограничиваться симметричными функциями а не влепить f(a,b) = g(b,a) и разворот списка?
def fold_left(foo, init, arr):
foo2 = lambda a,b: foo(b,a)
return fold_right(foo2, reverse(arr), start)
В функциональных языках принято считать, что списки приходящие как аргументы функции могут быть бесконечные. Поэтому не получится развернуть бесконечный список.
Вы правы, в статье подразумевается конечный список. В Коке для работы с бесконечными списками используется ко-индукция (это есть в книге Adam Chlipala: CPDT там работают несколько другие правила).
Извините, что поздновато отвечаю.
Не имеем права мы так сделать, с точки зрения математики. Мы занимаемся формальной верификацией. У нас есть функция, написанная программистами. А мы должны доказывать ее свойства и характеристики для всех возможных входных данных (указанных программистами-авторами функции). Просто менять тело функции мы не можем. Это все равно, что написать
Теорема: для всех натуральных чисел N, 3 + N = 5.
Доказательств не требует. Принимать, как аксиому.
И опираясь на эту теорему пытаться дальше верифицировать код...
… кажется мы не понимаем друг друга
в статье вы написали, что если код написан через fold_right, то его доказывать легче и потратили много времени рассуждая как доказывать fold_left
я ж утверждаю, что fold_left по сути представим через fold_right и reverse — и можно применить уже известное решение
по сути всё как в анекдоте про математика, что выключает газ и выливает чайник — потому что приводится к предыдущей, уже решённой задаче
Ага! Я настроила уведомления и теперь отвечаю побыстрее!
Да! Вы правы! fold_left представим через fold_right. И я описала этот случай в статье, это самый простой случай. Когда сворачивающая функция внутри fold коммутативна.
Обратите внимание на приведенную в статье теорему из стандартной библиотеки
Theorem fold_symmetric : forall (A : Type) (f : A -> A -> A), (forall x y z : A, f x (f y z) =
f (f x y) z) ->
forall (a0 : A),
(forall y : A, f a0 y = f y a0) ->
forall (l : list A),
fold_left f l a0 = fold_right f a0 l.
То есть эта теорема и есть ваше (совершенно справедливое, но не для всех случаев верное) утверждение.
И эта теорема доказана и находится в стандартной библиотеке Coq и ее можно использовать. Но, видите, у этой теоремы есть предпосылка о внутренней сворачивающей функции. Что результат ее вычислений не изменится от перемены мест аргументов.
Далее, там, где я "потратила много времени, рассуждая как доказывать fold_left" я показывала, что делать в случаях, когда просто переписать fold_left на fold_right не получится. Не получится, потому, что сворачивающая функция внутри не коммутативна, то есть мы не имеем права переписать с точки зрения математики, результаты работы функций будут разные.
(3 + 2) все равно, что (2 + 3) - это коммутативная операция
Но (3 - 2) это не то же самое, что (2 - 3), понимаете?
А мы занимаемся формальной верификацией. Мы не можем изменять исходный код верифицируемых нами функций бездоказательно, так как нам удобно. Мы же в коде баги ищем. Мы для некоторых функций просто не сможем применить теорему fold_symmetric потому, что, чтобы ее применить нужно доказать потом еще, что внутренняя сворачивающая функция удовлетворяет требованию. А если это не так - это просто недоказуемо.
Но спасибо за вопрос, хороший вопрос (хоть ответ на него и есть в статье, а видно, сложновато написано).
А если обёртку меняющую аргументы местами вставить? Тогда коммутативность не нужна
Пусть а_б = б-а
(3-2) = (2_3)
(5-(3-2)) = ((2_3)_5)
Мы не можем изменять исходный код верифицируемых нами функций бездоказательно
так я и не меняю
я лишь представляю уже имеющийся как набор других компонент
На здоровье. Только если сможете свои утверждения доказать. Чтобы Coq позволил в конце "Qed" написать. Ч.Т.Д - по-нашему.
Можно еще некоторые вещи аксиоматизировать (объявлять аксиомами), а потом использовать их в доказательствах.
Но эдак далеко можно зайти... зайти далеко, а никуда не прийти.
Все утверждения, которые мы используем в доказательствах должны быть доказаны.
Блин, ну не понимаю я вас совершенно
В статье написали — fold_left фигню с аккумулятором творит, а вот fold_right молодец. Чтобы это решить… свяжем себе руки и выбросим нафиг часть функций.
Я конечно тоже могу сказать "На здоровье, выкидывайте. Ешьте свой кактус", но блин
Вот вам предлагают "обертка+разворот+fold_right == fold_left".
Ладно бы вы придрались к развороту. "Какой-нибудь функциональный закон нарушает"
Ладно бы придрались к обёртке. "Автоматическое доказывание через другую входную переменную не идёт"
Но ваши аргументы:
"нельзя переписывать код" — когда сами в статье fold_left через fold_right выражаете — и
"Как сможете доказать, тогда и будем обсуждать что не накладывать на функцию ограничение коммутативности вообще возможно" — вообще напоминает "как убьют — тогда и звоните"
Вон питоновский код в первом комменте. Вон пример с а_б.
Оба показывают как это работает. Приём работает.
Проблемы которые видите вы — я не вижу.
И поэтому я прошу Вас, великого мастера функциональщины, объяснить простому смертному Мне в чём проблема
Да что ж ты будешь делать... вы в каком часовом поясе?
Спасибо вам за питоновский код! Но на питоне, к сожалению, мы не можем ничего доказать (питон не является одним из интерактивных программных средств доказательства теорем).
Впрочем, я рада, что вас так заинтересовала формальная верификация.
У меня в тексте статьи приведен код на Coq. Это очень простой (как топор) пример, исключительно демонстративного характера.
Докажите, пожалуйста, лемму transformation вашим способом.
то бишь "обертка+разворот+fold_right == fold_left".
Видите, как я там мучаюсь, какое доказательство длинное вышло.
Код, пожалуйста, выложите на гитхаб и ссылочку мне пришлите, чтобы я могла скомпилировать на своей машине ваше решение.
А я завтра напишу вводную статью о формальной верификации. Что это вообще такое и зачем она нужна. По рукам?
Еще можно взять лист бумаги, ручку, ваше утверждение, и сформулировать как теорему. Мол, для всех f и для всех списков это равенство выполняется.
А потом подобрать такую функцию f и такой список, для которых ваше равенство выполняться не будет. То есть попытаться найти/подобрать опровержение.
Это прежде, чем формулировать это все на Coq. Это будет быстрее и проще. И должно занять не так много времени.
Написал сложное доказательство, в котором естественно возникают зависимые типы (некоторый тип данных естественным образом делится на "слои", индексированные натуральными числами). Итого, есть типы B и A n, где n:nat. Хочу доказать, что B есть сумма всех A n. Строю функции
foo (n:nat) (a: A n) : B
rang (b:B) : nat
bar (b:B) : A (rang b)
Доказываю
forall (b:B), foo (rang b) (bar b) = b
forall (n:nat) (a: A n), rang (foo n a) = n
Но когда выписываю теорему
forall (n:nat) (a: A n), bar (foo n a) = a
получаю
"The term bar (foo n a) has type A (rang (foo n a)) while it is expected to have type A n".
Спрашиваю на форуме, отвечают -- надо присобачить тип равенства. Прикидываю, как его присобачить, понимаю, что доказательство (и без того сложное) станет сложнее в два раза, бросаю Coq нафиг. Хотя, сделан Coq хорошо, это я такой хитроумный.
А вы пробовали выложить код на гитхаб, чтобы его можно было быстренько скачать и скомпилировать и задать свои вопросы тут: https://coq.zulipchat.com/
Сообщество кок отвечает моментально, очень помогают и поддерживают друг друга. Вероятно потому, что их популяция очень мала (редки как бенгальские тигры или белоснежные барсы).
Она есть и в Haskell, и в OCaml и в Rust. Используется чаще, чем
fold_right, вероятно потому, что с ее помощью проще писать эффективный код.
Мне казалось, что foldr используют чаще, чем foldl, потому что она работает быстрее и меньше жрет памяти. Ну по крайней мере так в Haskell, потому что там эти функции ленивые и foldl порождает много отложенных вычислений. Про другие языки не скажу.
Если операция свёртки энергичная (как в набившем оскомину примере суммы списка через свёртку), то левая свёртка эффективнее, потому что не плодит thunk-и.
Точно! Спасибо за замечание. Я ее верифицировала для языка OCaml, вот почему я написала "чаще". А OCaml не ленивый (ленность там отдельно подключать нужно). Кто чаще ее использует зависит от того, какой язык используется - ленивый нет. Можно я статью исправлю с вашим уточнением.
COQ: верификация функций, содержащих fold_left