История изменений
Исправление quasimoto, (текущая версия) :
Откуда там верификация?
Верификация это проверка типов (* может быть проверкой типов).
Ошибочная программа корректно скомпилируется и будет некорректно работать.
В бедном языке. В достаточно выразительном — не скомпилируется.
Они разве эквивалентны?
С точки зрения денотационной семантики — да. С точки зрения операционной — нет. Вопрос ТС был про денотационную. В математике есть понятие о равенстве функций, называется экстенсиональное равенство (extensional equality). Вот разные fib и sort «равны» если дают одинаковые результаты — реализуют одну и ту же функцию (одна семантика, но разные программы, алгоритмы, сложности, операции).
И что это доказывает?
Что они эквивалентны modulo extensional equality? В математике есть понятие об отношении вообще и отношении эквивалентности в частности :)
они отлично влазят в uin64_t, не сложно это доказать
fib(100) > 2 ^ 64.
мне твоё доказательство, которое работает сто лет, нафиг не нужно
Ты о каком доказательстве сейчас говоришь?
А если у тебя N занимает всю память твоего компьютера, что ты будешь делать?
Извини, не сталкивался :)
Ну и всё относительно же — сколько там байт «хватит всем»?
Есть некое КОНЕЧНОЕ множество объектов(чисел), и свойства этого множества очень сильно отличаются от свойств бесконечного множества.
Ну это тоже «вещь». Я о том что любая непротиворечивая хрень, сколь бы странной она не была, имеет модель (теорема о _полноте_, кстати :)). Всегда можно проводить рассуждения, причём вполне эффективно — формально или нет (а то тебя смущают какие-то бесконечности, и какие-то доказательства по сто лет проверяются).
Ну и я так и не понял чем плохи бесконечные типы GMP и разных ЯВУ (понятно, что есть вопрос производительности).
Исходная версия quasimoto, :
Откуда там верификация?
Верификация это проверка типов (* может быть проверкой типов).
Ошибочная программа корректно скомпилируется и будет некорректно работать.
В бедном языке. В достаточно выразительном — не скомпилируется.
Они разве эквивалентны?
С точки зрения денотационной семантики — да. С точки зрения операционной — нет. Вопрос ТС был про денотационную. В математике есть понятие о равенстве функций, называется экстенсиональное равенство (extensional equality). Вот разные fib и sort «равны» если дают одинаковые результаты — реализуют одну и ту же функцию (одна семантика, но разные программы, алгоритмы, операции).
И что это доказывает?
Что они эквивалентны modulo extensional equality? В математике есть понятие об отношении вообще и отношении эквивалентности в частности :)
они отлично влазят в uin64_t, не сложно это доказать
fib(100) > 2 ^ 64.
мне твоё доказательство, которое работает сто лет, нафиг не нужно
Ты о каком доказательстве сейчас говоришь?
А если у тебя N занимает всю память твоего компьютера, что ты будешь делать?
Извини, не сталкивался :)
Ну и всё относительно же — сколько там байт «хватит всем»?
Есть некое КОНЕЧНОЕ множество объектов(чисел), и свойства этого множества очень сильно отличаются от свойств бесконечного множества.
Ну это тоже «вещь». Я о том что любая непротиворечивая хрень, сколь бы странной она не была, имеет модель (теорема о _полноте_, кстати :)). Всегда можно проводить рассуждения, причём вполне эффективно — формально или нет (а то тебя смущают какие-то бесконечности, и какие-то доказательства по сто лет проверяются).
Ну и я так и не понял чем плохи бесконечные типы GMP и разных ЯВУ (понятно, что есть вопрос производительности).