AK
Модель может опускать некие мелкие подробности реализации, не влияющие на конечный результат. Если же бесконечность памяти вписана в само определение, то игнорировать ее нельзя и это было бы нарушением спецификации
Size: a a a
2020 January 27
AT
мы это точно знаем?
Конечность пространства и энергии? Да, вполне точно. Особенно доступных - их вообще очень-очень мало по сравнению со вселенной.
AK
Ну а про модель сферического коня в вакууме все знают
M
Yaroslav Schekin
Все DFA останавливаются, очевидно.
В теории. Это если у нас бесконечно памяти и времени. Надеюсь про ReDoS вы слышали?
AT
MaxGraey
В теории. Это если у нас бесконечно памяти и времени. Надеюсь про ReDoS вы слышали?
DFA работают в константной памяти и за конечное время. ReDoS - это про экспоненциальные PCRE, которые на самом деле не регулярные.
AG
Тотальное подмножество, очевидно, не полное. Я не смотрел, используются ли в компиляторе Idris 2 нетотальные функции. По идее, должно быть можно обойтись без них. @clayrat что там на самом деле в кодовой базе?
да, там много где стоит
%default covering, т.е. только проверка на исчерпывающий патматAT
да, там много где стоит
%default covering, т.е. только проверка на исчерпывающий патматА там есть что-то принципиально не-тотальное, или это просто для удобства (поленились)?
AG
ну там у Брэди идея написать скорее быстрый компилятор, чем корректный
YS
MaxGraey
В теории. Это если у нас бесконечно памяти и времени. Надеюсь про ReDoS вы слышали?
Вот именно, в теории DFA (все они!) всегда останавливаются.
Поэтому я и посоветовал Вам эту теорию повторить. ;)
Поэтому я и посоветовал Вам эту теорию повторить. ;)
AG
сложно сказать, думаю он просто срезал углы где мог
AT
сложно сказать, думаю он просто срезал углы где мог
Трудно его в этом винить. 😊
M
Yaroslav Schekin
Вот именно, в теории DFA (все они!) всегда останавливаются.
Поэтому я и посоветовал Вам эту теорию повторить. ;)
Поэтому я и посоветовал Вам эту теорию повторить. ;)
Соглашусь DFA был плохим примером, как насчет функции Аккермана?
K
Так и она останавливается
K
За время меньше бесконечного при конечных инпутах
AT
MaxGraey
Соглашусь DFA был плохим примером, как насчет функции Аккермана?
Так Вы какой пример пытаетесь привести? Если модель, способную вычислить любую функцию, то она автоматически будет эквивалентна МТ (равно как и лямбда-исчислению, нормальным алгорифмам Маркова, Brainfuck, etc.), а следовательно, подвержена проблеме останова. 🤷♀️
M
Так Вы какой пример пытаетесь привести? Если модель, способную вычислить любую функцию, то она автоматически будет эквивалентна МТ (равно как и лямбда-исчислению, нормальным алгорифмам Маркова, Brainfuck, etc.), а следовательно, подвержена проблеме останова. 🤷♀️
Да, привести пример не тьюринг полной модели с проблемой останова
M
Изначально вопрос был в том, если какая то очевидная прямая и обратная связь между полнотой по тьюрингу и проблемой останова. Вот собственно это пытаемся выяснить
А⚙
Тьюринг не требует бесконечность. он требует бесконечность ИЛИ возможность добавлять память, когда понадобится
Я бы не сказал, что эти две возможности принципиально отличаются на практике
МБ
Все современные ЯП и так полны по Тьюрингу
Вроде не все. Есть же тотальные языки: Idris, Sixten