> We do take a —work-dir to specify the relative position of .stack-work. > Due to limitations in Cabal, we cannot make this an absolute directory.

Помогите найти статью в вики. Ищу теорему/утверждение о том, что ленивая стратегия вычислений и тотальность функций помогают в анализе програм (завершимости?). Надеюсь не очень переврал.

Помогите найти статью в вики. Ищу теорему/утверждение о том, что ленивая стратегия вычислений и тотальность функций помогают в анализе програм (завершимости?). Надеюсь не очень переврал.

Ленивость никак не помогает в анализе завершимости

а тотальность функций и завершимость программ — это одно и то же

Уфф, нашел, переврал конечно, не помню в каком контексте я делал подобные выводы, но искал это https://en.wikipedia.org/wiki/Walther_recursion

а тотальность функций и завершимость программ — это одно и то же

Точно, спасибо )

разве что в Liquid Haskell тотальность означает, что функция готова принять любое значение аргумента, но не завершимость, а завершимость как-то ещё названа

А если ограничить завершимость практически -- например, 1 млрд вызовов функций от main при размере входа в X попугаев, эта-то задача разрешима?

А если ограничить завершимость практически -- например, 1 млрд вызовов функций от main при размере входа в X попугаев, эта-то задача разрешима?

По-моему, была идея в использовании Walther_recursion и последовательной аппроксимации для решения вопроса о завершимости, для практического использования

да, за 1 млрд шагов разрешима

Ну с помощью методов суперкомпиляции можно часть шагов свернуть

можно и не свернуть. нет гарантии

По-моему, была идея в использовании Walther_recursion и последовательной аппроксимации для решения вопроса о завершимости, для практического использования

Спасибо, почитаю. Хотя, имхуется мне, об диагональный метод и эту штуку можно поломать.

Ну ок, дадим проверяльщику 1 час времени, грубо говоря. Много ли есть такого практического кода, который бы он не успел за это время проверить?

Просто проблема завершимости кажется какой-то теоретической, как будто не применимой к обычным оперденям.

да. любой код, работающий больше 1 часа

в оперденях да, а на бэкенде вполне могут быть задачи на несколько часов

да, за 1 млрд шагов разрешима

поправка: не менее чем за 1 млрд в худшем случае

кроме того, не очень понятно, зачем тебе знание о завершимости только для одного набора входных данных

кроме того, не очень понятно, зачем тебе знание о завершимости только для одного набора входных данных, причём после того, как программа для этого набора уже отработала

ответ на вопрос о разрешимости интересен до запуска

Так я про один набор не говорил. Я про все возможные, ограниченные некоей длиной N.

Так я про один набор не говорил. Я про все возможные, ограниченные некоей длиной N.

значит, умножь на e^N

Дак зачем на всех наборах проверять? Это худший случай, когда не удалось внутри всё посворачивать.

пока человечество научилось решать проблему останова только для специально ограниченных нетьюринговых машин (языков)

Суперкомпиляторы ж как-то более-менее сворачивают программки?

Суперкомпиляторы ж как-то более-менее сворачивают программки?

не всегда. как повезёт

Ну невезение -- оно постоянно? Или только время от времени встречается?

понимаешь разницу между ∃ и ∀?

Ну немного

И что?

Я ж пишу про ограниченный вход и ограниченное время проверки.

Отставить токсичность! Меня вот, например и нетьюринговые устраивают

не всегда. как повезёт

Тут интересно распределение невезения.

проверить останов некоторых МТ можно. проверить останов всех МТ — вообще всех возможных — нельзя

Отставить токсичность! Меня вот, например и нетьюринговые устраивают

го на dhall прогать

Да я и не хочу проверять все МТ

Тут интересно распределение невезения.

при любом распределении проблема останова не разрешима

Да я и не хочу проверять все МТ

а какие хочешь?

Ну ладно, упрощу вопрос. Можете привести примеры, скажем так, "практических функций", например, из стандартной библиотеки Хаскеля, на которой проверяльщик зациклится?

Т.е., если я пишу очередную опердень, насколько вероятно, что её нельзя будет проверить проверяльщиком завершённости?

(предположим, что библиотеки и фреймворки, которые я при этом использую, каким-то образом верифицированы)

Ну ладно, упрощу вопрос. Можете привести примеры, скажем так, "практических функций", например, из стандартной библиотеки Хаскеля, на которой проверяльщик зациклится?

какой проверяльщик?

универсального проверяльщика нет, и не может быть, как известно

если опердень — веб-сервер, то она по ТЗ должна работать вечно, то есть точно не завершается

при любом распределении проблема останова не разрешима

На 100% нет, а скажем на 90% — уже практически полезно, 99% — отлично

Да

Ну вот нашёл инструменты: http://termination-portal.org/wiki/Category:Tools

Ну и сам сайт интересный, кажется.

если опердень — веб-сервер, то она по ТЗ должна работать вечно, то есть точно не завершается

Можно её вечную работу свести к запуску функций по событиям.

из стандартной библиотеки, например, map не завершимая

Ну всё довольно просто же. Есть разнообразные классы алгоритмов, для каждого из которых есть более сложная функция (не входящая в этот класс процедур), и соответсвующая ей очень сложная синтаксическая структура. Чем более широкий класс процедур рассматриваем, тем сложнее синтаксическая структура.

из стандартной библиотеки, например, map не завершимая

Потому что у неё вход бесконечный?

У большинства функций вход бесконечный

Потому что у неё вход бесконечный?

да, в худшем случае

На практике функции из конечных множеств в конечные множества никому не нужны

Если вы не свойства группы монстра изучаете

На практике у нас все множества конечные

На 100% нет, а скажем на 90% — уже практически полезно, 99% — отлично

Я вообще вот именно про это говорил. Сделаем проверяльщик. Да, он не тотален. Будем натравливать его на программы и давать ему, к примеру, час времени. Если справился за час -- значит, ставим на программу шильдик "проверена". Вот и всё. Спрашивается, насколько он будет полезен? Если он за час сможет проверять кучу полезных программ, то и пусть себе будет нетотальным.

На практике у нас все множества конечные

На практике все множества бесконечные

???

На практике функции из конечных множеств в конечные множества никому не нужны

ну почему же? в БД конечно таблиц, в таблицах конечно колонок, типы колонок ограничены, например 64 битами или 4096 символами. вполне реальная ситуация

Что угодно Double → Double

Вполне конечные множества

А потом кто-то доставляет памяти в сервер и всё падает

да, все Double за час не переберёшь

Бесконечность это возможность к расширению и всё

Да зачем их все-то перебирать?

Бесконечность это возможность к расширению и всё

Куда Double расширять? В quad precision?

Да зачем их все-то перебирать?

как иначе программу проверить?

Куда Double расширять? В quad precision?

arbitrary precision float

Куда Double расширять? В quad precision?

Запустить программу на компе с 128'битами?

arbitrary precision float

Это уже совсем другой зверь с другими алгоритмами

Разбор частных случаев. Ну вот есть программа bug :: Double -> Double ; bug x = if x = 2 then bug 2 else 1 / x. Тут всё множество поделится на (-inf, 0), 0, (0, 2), 2, (2, inf). Для случая 2 есть рекурсивный вызов без изменения аргумента, следовательно -- это явный цикл. Для 0 -- деление, типа, тоже программа завершается. остальные значения обрабатываются.

Запустить программу на компе с 128'битами?

Т.е. в quad precision? Но чтобы реализовать его вероятно придётся переделывать код, т.к. вполне может быть привязан к свойтсвам IEEE754

Разбор частных случаев. Ну вот есть программа bug :: Double -> Double ; bug x = if x = 2 then bug 2 else 1 / x. Тут всё множество поделится на (-inf, 0), 0, (0, 2), 2, (2, inf). Для случая 2 есть рекурсивный вызов без изменения аргумента, следовательно -- это явный цикл. Для 0 -- деление, типа, тоже программа завершается. остальные значения обрабатываются.

И NaN

И бесконечности, и отрицательный ноль

Ну да, я, кажется, начинаю понимать... Всё-таки множество таких разбиений может сильно вырасти, что будет почти эквивалентно полному перебору.

Ладно, надо матчасть подтягивать по завершителям

Ах да, для 32 бит есть ещё excess precision, так что нет гарнтий, что равенство будет работать как ожидается