b
если ты можешь доказать что все компоненты твоей программы будут выполняться за полиномиальное время, то ты знаешь что твоя программа будет выполняться полиномиальное время
Size: a a a
2020 October 30
p
погоди ты доказал что у этой функции такая сигнатура? или ээм
Я доказал что для всех n выполняется равенство myfunc n = n + 10
SP
а че оно делает то
p
forall n. myfunc(n) = n + 10
p
Понял?
SP
неТ )
p
а че оно делает то
= это тип данных. У него есть конструктор Refl: x -> x = x
p
Понял?
SP
окей погоди у теюя есть функция myfunc которая добавляет к инту 10. разве это не самоочевидно что она это делает?
p
окей погоди у теюя есть функция myfunc которая добавляет к инту 10. разве это не самоочевидно что она это делает?
Да, очевидно. Я в качестве примера привел.
p
Для теста мы пишем myfunc 10 = 20
p
Для пруфа мы пишем forall n. myfunc n = n + 10
SP
т.е. это получается такой тест на множестве?
p
т.е. это получается такой тест на множестве?
Да, на множестве всего типа
p
Это первый вид доказательств: пишешь лемму в сигнатуре и в теле доказываешь ее
SP
хмм. тело доказательства тут примерно такое же как тело функции кек
EG
хмм. тело доказательства тут примерно такое же как тело функции кек
А это с любыми проверками так
SP
Это первый вид доказательств: пишешь лемму в сигнатуре и в теле доказываешь ее
хитро
EG
Тесты тоже регулярно от такого страдают
p
хмм. тело доказательства тут примерно такое же как тело функции кек
Ну Идрис умеет пруфать тривиальные проверки сам