Так я про один набор не говорил. Я про все возможные, ограниченные некоей длиной 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, так что нет гарнтий, что равенство будет работать как ожидается

Интересно, а в Лаборатории Касперского уже сталкивались с такими программами, про которые не удавалось за конечное время сказать, что они точно вирусы или не вирусы?

@cblp_su ^ ;)

*шутка про макось и бэкдоры*

Я думаю что спустя конечное время на них натравливают вирусологов

Интересно, а в Лаборатории Касперского уже сталкивались с такими программами, про которые не удавалось за конечное время сказать, что они точно вирусы или не вирусы?

я не в курсе, я в другом отделе работаю. но элементарная математика говорит, что очевидно да

задача любого вируса — не быть распознанным как вирус

Задача максимум

раз в несколько лет такое случается

компьютеры не всесильны

"Такое" -- что?

простите. вернёмся к Хаскелю и машинам Тьюринга

"Такое" -- что?

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

пишите опердень на Coq/Agda/Idris, чтобы она завершалась

Будем стараться!

Главное, самим при этом завершаться

http://aprove.informatik.rwth-aachen.de/eval/Haskell/

Библиотека хаскеля более-менее завершается ;)

пишите опердень на Coq/Agda/Idris, чтобы она завершалась

Жестокий ты человек

есть анализ завершимости для Хаскеля в Liquid Haskell. работает примерно так же, как в тотальных языках. грубо говоря, если функция имеет известную структуру для тотальных функций, то она тотальна, иначе — завершимость не доказана

Жестокий ты человек

это самое доброе, что можно предложить

жестокий предложил бы ATS

пишите опердень на Coq/Agda/Idris, чтобы она завершалась

Добавляем в петлю параметр типа Nat, уменьшаем на единицу каждый проход, изначально суём 2^10000. На наше век завершимости хватит.

Добавляем в петлю параметр типа Nat, уменьшаем на единицу каждый проход, изначально суём 2^10000. На наше век завершимости хватит.

Замечательно же, можно теоретизировать, а можно пытаться делать полезные вещи http://aprove.informatik.rwth-aachen.de/index.asp?subform=termination_proofs.html

Я правильно понимаю, что Control.Category не предназначен для описания категорий с объектами-объектами?

то есть он чисто для объектов-типов?

и если не прездназначен, то есть ли либа чтобы сразу получить много полезных функций?

Всем привет! решил ФП попробовать и haskell в частности) Пока еще ничего не писал, только читаю чат да статьи разные про хаскел, окамл, дизайн в фп стиле и тп, и даже много чего на удивление понятно) Но это как с иностранным - читаешь- понимаешь - но сам написать еще не можешь. В целом код в разных хело-ворд примерах понятен (вроде бы :) ) - на монады, трансоформеры, линзы, сервантовские type-level "шткуки" , free-монады. Но вот как бы это все сложить вместе в конкретном случае непонятно. Поэтому решил на практике сделать какойто микросервис и походу разбираться. Есть 2 вопроса (на самом деле больше) edit - Вопросы отдельными сообщиниями сделал

1) Есть ли в каком то из фреймворков (пока рассматриваю только scotty или servant) возможность отдавать статические файлы? Но так, чтобы range header правильно обрабатывать и прочие стандарты соблюдать и не делать все самому. Знаю, что есть stream servant-а, но он не соблюдает все эти стандарты и надо самому все это делать - не подходит. Как вариант еще предлагают мидлварь из wai "заворачивать" в сервантовский Raw - но мне тоже не подходит, так как по условию задачи файл нужно отдавать только при соблюдении ряда условий, проверяемых внутри хендлера (разного рода авторизация закачек) - поэтому нужно как бы динамически "подсовывать" статик-хендлер , в противном случае отдавать 404. А в wai просто статичный роут на папку и все.

2) Есть ли какой-то сайт с задачками на "комбинаторы" ?) Типа, хитро скомбинировать zip'ы, fold-ы, map-ы, "совы" , аппликативы, bind и тп, чтобы поинт фри запись не вызывала стопор на 5 минут )

Всем привет! решил ФП попробовать и haskell в частности) Пока еще ничего не писал, только читаю чат да статьи разные про хаскел, окамл, дизайн в фп стиле и тп, и даже много чего на удивление понятно) Но это как с иностранным - читаешь- понимаешь - но сам написать еще не можешь. В целом код в разных хело-ворд примерах понятен (вроде бы :) ) - на монады, трансоформеры, линзы, сервантовские type-level "шткуки" , free-монады. Но вот как бы это все сложить вместе в конкретном случае непонятно. Поэтому решил на практике сделать какойто микросервис и походу разбираться. Есть 2 вопроса (на самом деле больше) edit - Вопросы отдельными сообщиниями сделал

Напиши бота, который из группы выделяет полезные сообщения (все сообщения с ссылками и сообщения ответы на сообщения с ссылками, а также все сообщения от админов - последнее опционально, т/к например не работает в этой группе)

Напиши бота, который из группы выделяет полезные сообщения (все сообщения с ссылками и сообщения ответы на сообщения с ссылками, а также все сообщения от админов - последнее опционально, т/к например не работает в этой группе)

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

у нас аренда сервера CI стоит в 2 раза больше чем сервер прода, причем на CI даже свапфайл сделали от безнадеги :)

ради серванта ? или есть еще "известные" прожорливые пакеты?

1) Есть ли в каком то из фреймворков (пока рассматриваю только scotty или servant) возможность отдавать статические файлы? Но так, чтобы range header правильно обрабатывать и прочие стандарты соблюдать и не делать все самому. Знаю, что есть stream servant-а, но он не соблюдает все эти стандарты и надо самому все это делать - не подходит. Как вариант еще предлагают мидлварь из wai "заворачивать" в сервантовский Raw - но мне тоже не подходит, так как по условию задачи файл нужно отдавать только при соблюдении ряда условий, проверяемых внутри хендлера (разного рода авторизация закачек) - поэтому нужно как бы динамически "подсовывать" статик-хендлер , в противном случае отдавать 404. А в wai просто статичный роут на папку и все.

статические файлы через wai middleware

статические файлы через wai middleware

тоесть я смогу динамически подсовывать middlware ? допустим нужно сходить на другой сервер, проверить ссылку и если ОК - тогда "отдать" через мидлварь ?

2) Есть ли какой-то сайт с задачками на "комбинаторы" ?) Типа, хитро скомбинировать zip'ы, fold-ы, map-ы, "совы" , аппликативы, bind и тп, чтобы поинт фри запись не вызывала стопор на 5 минут )

99 Haskell problems, hackerrank, codewars

тоесть я смогу динамически подсовывать middlware ? допустим нужно сходить на другой сервер, проверить ссылку и если ОК - тогда "отдать" через мидлварь ?

можно

99 Haskell problems, hackerrank, codewars

спасибо, буду смотреть

можно

а можно еще одну подсказку? - тут нужен этот пакет wai-app-static? а то я все время про этот wai-middleware-static говорил, и он вроде не подходит

а можно еще одну подсказку? - тут нужен этот пакет wai-app-static? а то я все время про этот wai-middleware-static говорил, и он вроде не подходит

да и в правду я их часто путаю и каждый раз гуглю заново