IJ
если я правильно читаю: "Если есть любое доказательство правильности программы, то его можно модифицировать так, чтобы оно синтезировало программу"
Size: a a a
2020 March 16
IJ
Но да, это не говорит ничего о размере доказательства по отношению к самой программе
A
Оно говорит, что доказательство не может быть слишком коротким по отношению к самой короткой программе, решающей ту же задачу :)
RS
Нет такого, что доказательство обязательно в три раза длиннее программы. Как я понимаю, он говорит как раз об обратном, что доказательство можно сделать таким, что оно будет не более, чем в три раза длиннее, чем программа.
A
Программу можно сделать такой, что она будет не более, чем в три раза длиннее, чем доказательство
Поскольку программа обычно короче доказательства, это не особо помогает
Поскольку программа обычно короче доказательства, это не особо помогает
DS
Rifat S
Нет такого, что доказательство обязательно в три раза длиннее программы. Как я понимаю, он говорит как раз об обратном, что доказательство можно сделать таким, что оно будет не более, чем в три раза длиннее, чем программа.
Насколько я понял, увеличение длины здесь относится именно к первоначальному доказательству.
Т.е. можно из доказательства длины L, получить конструктивное доказательство длины < 3 * L
Т.е. можно из доказательства длины L, получить конструктивное доказательство длины < 3 * L
IJ
Оно говорит, что доказательство не может быть слишком коротким по отношению к самой короткой программе, решающей ту же задачу :)
Про самую короткую программу ничего не говорится же
IJ
Доказательство, которое синтезирует программу, совершенно не обязательно синтезирует её оптимальный с какой бы то ни было точки зрения вариант
A
Это следствие
2020 March 17
PS
Пример "доказательств в 0 строк" в контексте компиляторов: https://blog.regehr.org/archives/1722
E
хм.. есть у меня 32 байта памяти, которые нужно обнулить. Данные имеют неизвестный алайнмент (но как минимум 8 байт)
что лучше - обнулить через два 128битных ксора (sse) или один avx xor (256 бит) 🙄
интел мануал говорит что при неизвестном алайнменте авх ксор по сути каждый второй раз будет получать пенальти за пересечение кэшлайна
что лучше - обнулить через два 128битных ксора (sse) или один avx xor (256 бит) 🙄
интел мануал говорит что при неизвестном алайнменте авх ксор по сути каждый второй раз будет получать пенальти за пересечение кэшлайна
2020 March 18
C
wtf man🤨
C
Wait, maybe someone will answer your question.
BD
looks like homework
SM
Do you need just the solution? If so, we need the table as well
BD
Post the table then
2020 March 19
KR
Типы с уточнением ("refinement types") от такого спасают.
На F*:
На F*:
val subtract_proof: a: Int -> b: Int -> c: Int -> Lemma (ensures(с = a - b))(Синтаксис я немного забыл, но не суть)
let subtract_proof a b = admit()
Как человек, исправивший ошибку в самоучителе F* , не могу заставить себя поверить вам.
KR
Вот и вопрос: а должен ли я заставлять своего пользователя трудиться над этим? Оно понятное дело, что дело очень интересное. Но вот есть у меня друг - биолог, ему важнее пересчитать варианты (забыл научное название) кусочков форм вирусов уже сейчас, потому как через год уже будет другой штамм гриппа...
А я вот не понимаю, есть ли вообще надежда, что когда-нибудь с типами будет легко и просто доказываться всё. А ещё лучше, будут ли завтипы выводится? Или это вообще невозможный вариант?
А я вот не понимаю, есть ли вообще надежда, что когда-нибудь с типами будет легко и просто доказываться всё. А ещё лучше, будут ли завтипы выводится? Или это вообще невозможный вариант?
Для численных методов хорошо работают обычные физические размерности. Но они не реализуемы нормальным образом на современных яп. В смысле, функция pow или sqrt должна правильно обрабатывать размерности. И, соответственно, всякие композиции.
С другой стороны, в вычмат задачах почти нет ветвлений, поэтому там отлично пригождается питон и покрытие тестами - верификация методом монте-карло.
Ещё, кстати, кто-то улучшает это монте-карло с помощью AFL фаззера.
С другой стороны, в вычмат задачах почти нет ветвлений, поэтому там отлично пригождается питон и покрытие тестами - верификация методом монте-карло.
Ещё, кстати, кто-то улучшает это монте-карло с помощью AFL фаззера.
Т8
какие проблемы возникли у Страуструпа при добавлении исключений в Cfront?