Могут ли быть строгие ФП языки тьюринг-полными.

О, виртуалы таки закончились?

А ви с какой целью интересуетесь?

не совсем

На практике тьюринг-полнота для таких языков не такая уж и большая проблема. Ограничения таких языков не фатальны.

Насколько я понял, там утверждается, что нетотальность идентифицируется исполнителем как побочный эффект. И в рамках чего-то там, это выполняется под капотом бла-бла-бла. Однако же побочные эффекты выходят за рамки, непосредственно семантики языка.

Эти язычки имеют одно интересное свойство — проверку на завершаемость. Например, нельзя бесконечную рекурсию.

А вот Хачкель — «строгий ФП язык»? У меня на нём-таки получилось:

f x = f x
main = putStrLn $ f 1

Нет

Что такое «строгий ФП язык»?

Ну это мое определение, я не нашел в русском эквивалента англ totality

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

Что такое «строгий ФП язык»?

Total functional programming (also known as strong functional programming, to be contrasted with ordinary, or weak functional programming) is a programming paradigm that restricts the range of programs to those that are provably terminating.

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

там утверждается, что Тьюринг-полнота не влечёт за собой нетотальность. в примере из предыдущего треда Brainfuck на Agda реализован без отключения termination checker'а

А может наоборот это означает, что тьюринг-полнота противоречива? Что не может ее существовать?

Начнем с того, что существует проблема останова. Мы не можем сказать заранее, остановится ли произвольный алгоритм или нет. Это неотъемлемое свойство МТ и любой вычислительной модели эквивалентной ей. Если вычислительная модель не обладает таким свойством, значит она не является частным случаем, и она тьринг-неполна, ибо ограничена: ее вычислительной мощности не хватает для того, чтобы реализовать любую вычислимую функцию. В множество вычислимых функцй входит подмножество тех, о которых неизвестно заранее, терминируются они или нет.

Собственно, изначально ясно, что все эти тезисы Тьюринга — это лажа. Алгоритм вообще никогда не знает «о себе» остановиться он или нет, и где он остановиться. Это знает программист, который задает его, а не функция, которая вычисляется. Поэтому, да, никакой Тьюринг-полноты не существует. И более того, нет никакой вычислимости.

там утверждается, что Тьюринг-полнота не влечёт за собой нетотальность. в примере из предыдущего треда Brainfuck на Agda реализован без отключения termination checker'а

Как я понимаю, там просто строится ф-я nat -> состояния-интерпретатора-брейнфака-на-шаге-n. Ф-я, естественно, тотальна - ведь каждом конкретном шаге n у нас вполне вычислимое состояние. И никакого противоречия тут нет. Но в самом брейнфаке мы можем попытаться вычислить эту ф-ю от бесконечности, а в агде - не можем.

Поэтому, да, никакой Тьюринг-полноты не существует. И более того, нет никакой вычислимости.

«Движенья нет, сказал мудрец брадатый...»

Ну, скажем так, есть вычислимость с точки зрения человека, в том смысле, что X предположительно вычислиться. Но не абсолютное.

Например, нельзя бесконечную рекурсию

Можно бесконечную корекурсию. Типы с бесконечными развёртками — коиндуктивно.

event-loop получается, тоже нереализуем на них?

Аналогично, корекурсивно — реализуем.

А можно попроще объяснить, что это значит на практике? Это значит ты пишешь программу while(true) 1,компилируешь без ermination check запускаешь, и она выполняется, пока ты ее принудительно не остановишь?

Это значит — пишешь такую программу, компилируешь с termination checker-ом (который умеет различать рекурсию/корекурсию и индукцию/коиндукцию, которые не интерферируют как-то плохо и не ломают свойств системы типов завязанных на тотальность), программа чудесным или не очень образом превращается во что там её компилируют (хаскель, например, ТП язык), запускаешь, она выполняется пока ты ее принудительно не остановишь.

http://www.cse.chalmers.se/~nad/publications/danielsson-altenkirch-mixing.html

http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-...

http://github.com/agda/agda-stdlib/blob/master/src/Category/Monad/Partiality....

http://github.com/agda/agda-stdlib/blob/master/src/IO.agda

http://github.com/agda/agda-system-io/blob/master/src/System/IO/Primitive.agda

А зачем так много буков? Вас спросили, можно ли написать такую программу. Ваш ответ — можно. Только, непонятно, в таком случае, что там в языке вообще делает termination checker? И в чем отличие total-FP от НЕ total.

А зачем так много буков?

Потому что тебе «непонятно».

что там в языке вообще делает termination checker?

Проверяет завершимость программ, ака тотальность. В языке такого типа программы вычисляются во время проверки типов, так что им зависать не вариант. В языке такого типа это нужно для обеспечения непротиворечивости системы (в смысле Карри-Говарда), а то иначе зависающие программы смогут населять пустые типы — ложные утверждения станет возможно доказывать.

И в чем отличие total-FP от НЕ total.

«FP», «total-FP» и т.п. это ты сам себе придумал базвордов.

Завершимость рекурсивных программ проверяет TC, корекурсивным он даёт возможность быть в своей естественной незавершимой форме, «не интерферируют» и «не ломают» — что «непонятно»?

ложные утверждения станет возможно доказывать.

Так это же противоречит Геделю. Значит система неполна?

корекурсивным он даёт возможность быть в своей естественной незавершимой форме, «не интерферируют» и «не ломают» — что «непонятно»?

Вот это и не понятно. Но я не в курсе, что такое корекурсия и «интерферируют», поэтому, мне не понять, наверное.

То есть, он их не вычисляет, а просто запирает, типа, с «пометкой» бесконечные?

Так это же противоречит Геделю. Значит система неполна?

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

Но я не в курсе, что такое корекурсия и «интерферируют»

Что такое corecursion, coinduction, mixed induction/coinduction, partiality monad и какое отношение к Тьюринг-полноте написано в публикациях по теме.

А чтобы понять как оно не «интерферирует» в агде или ещё где-то — нужно использовать их по назначению (это же касается любых вопросов про хаскели и прочие ЯП, кстати).

То есть, он их не вычисляет, а просто запирает, типа, с «пометкой» бесконечные?

Termination checker ничего не вычисляет, он проверяет — с его точки зрения

f x = f x

не тотально-рекурсивна (и правильно), но

f x = corec (f x)

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

Можно бесконечную корекурсию.

Можно сделать бесконечно рекурсивную ф-ю, но нельзя ее вычислить. Не путай.

Аналогично, корекурсивно — реализуем.

Можно написать ф-ю, которая возвращает евент-луп. Но нельзя написать ф-ю, которая этот евент-луп запустит.

Это значит ты пишешь программу while(true) 1,компилируешь без ermination check запускаешь, и она выполняется

И она падает. В тотальном языке нельзя написать while(true) 1

Именно так. Как в примере с брейнфаком на агде - ф-я run интерпретатора возвращает пару из первого шага вычисления (что понятно вычислимо и тотально) и из функции, которая (если ее запустить) вычислит второй шаг третий и так далее рекурсивно. Но если ты например напишешь ф-ю, которая попытается вычислить весь трейс, или допустим попытаешься посчитать количество шагов в трейсе:

count Stop = 0 count Step x thunk = 1 + count (run thunk)

уже не чекнется. По сути, корекурсивный тип - та же жопа.

корекурсивный тип - та же жопа.

Статикобляди вообще мастера в заметании проблем под ковер. Замели - и значит проблемы как-то нет. Что жопы-корекурсии, что ИО.

Да всё можно — пишешь свою бесконечную функцию / евентлуп, чекаешь, компилируешь, запускаешь и оно работает сколько угодно долго.

«программа чудесным или не очень образом превращается во что там её компилируют» — «чудесным» будет компиляция каких-то выделенных IO и коиндуктивных примитивов реализацией, а если их выделенных нет, то этим нужно заниматься на самой агде, тогда http://github.com/agda/agda-stdlib/blob/fa10c180aaa2f39e25236519c9d44336139b8....

http://arxiv.org/abs/cs/0505037

То есть если общей рекурсии ... -> A нет, то просто делаем монадку Жопа на коиндукции, ... -> Жопа(A), типа как с IO, и пишем всё что нам вздумается тьюринг-полного в этом монаде. Дальше остаётся только тупняк с «термами ИО», «отсутствием семантики» и т.п.

Да всё можно — пишешь свою бесконечную функцию / евентлуп, чекаешь, компилируешь, запускаешь и оно работает сколько угодно долго.

Она не чекнется. А если чекнется - значит язык не тотальный. В тотальном языке можно написать тотальную ф-ю, которая вернет нетотальную ф-ю. Но _запустить_ нетотальную ф-ю (а евентлуп всегда нетотален) уже будет нельзя.