Конечное понимание бесконечного списка

Я набрал следующее в ghci, считая, что произойдет одна из двух вещей: 1) интерпретатор зависает, просматривая каждый член бесконечного списка для совпадений с предикатом; или 2) через занавес Haskell jujitsu, интерпретатор каким-то образом выяснит, что последовательность заканчивается на 4 и останавливается там.

[x | x <- [1..],5>x]

Результат 1 произошел. Теперь, результат 2 был много, чтобы просить. Но так как человек может доказать, что последовательность заканчивается на 4, может ли быть способ заставить интерпретатора сделать это? Может ли это быть переписано таким образом, что оно прекратится? На самом деле, есть ли когда-нибудь предикат, который делает конечное понимание из бесконечного списка?

Ответ 1

Но так как человек может доказать, что последовательность заканчивается на 4, может ли быть способ заставить интерпретатора сделать это?

В этом простом случае да. Но не существует общего алгоритма для определения того, является ли выражение истинным или ложным для всех натуральных чисел >n для некоторого n, потому что Haskell является завершающим Turing, поэтому невозможно доказать, что выражение даже представляет собой завершающую программу для все натуральные числа.

Даже если ваше выражение было ограничено основной целочисленной арифметикой, его истина все равно была бы неразрешимой в общем случае.

Может ли это быть переписано таким образом, что оно завершается?

Как писал Мог в комментарии, он takeWhile (< 5) [1..].

Ответ 2

takewhile - это правильное решение для вашей конкретной проблемы, как упоминалось выше.

Однако это происходит только потому, что в вашем случае все допустимые аргументы выходят перед всеми неприемлемыми аргументами, а общее понимание списка не подчиняется этому ограничению. Разумеется, можно было бы добавить символическое объяснение интерпретатору, чтобы оно могло доказать, что никакие другие элементы не будут приемлемыми, а затем прекратятся. (На самом деле, сложная система типов в Haskell была бы весьма полезна при реализации таких рассуждений.) Но было бы бессмысленно добавлять это к стандартному оператору [|], так как детектору пришлось бы работать во всех списках, которые оценивали и очень часто не вносили ничего, кроме гораздо больших затрат на вычисления.

Ответ 3

"Но так как человек может доказать, что последовательность заканчивается на 4, может есть ли способ заставить интерпретатора сделать это?"

Хороший вопрос. Трудная вещь - не доказательство того, что она заканчивается на уровне 4, но идея о том, что она может закончиться на 4, а затем понять, что это действительно так.

Ответ 4

Это проблема пользовательского интерфейса.

В Prolog есть оператор cut; в Haskell мы можем заранее указать, сколько решений мы ожидаем. Как и в вашем сложном примере (в комментариях), take 5 $ map f [1..] будет работать, но take 6 ... все равно перейдет в цикл. Чтобы преодолеть это, нам понадобится система времени выполнения, которая является доказательством теоремы (как говорили другие) и/или оптимизирующим во времени многопоточным ~~оптимистичным~~ спекулятивным частичным оценщиком, который откроет живые "ответ-боксы" для каждого пользовательского запроса. Это повлечет за собой возможность пометки вычислений с использованием значения приоритета (также на уровне языка).

Я думаю, что это было бы очень практично во всех смыслах. Это позволило бы нам уйти от написания интуитивно понятного простого кода, который в любом случае был первоначальным обещанием эквационального рассуждения. Первоначально код запускался бы в обычном режиме Haskell, но затем анализатор заходил бы за отставание вычислений.

Переводчики в большинстве случаев простаивают. Компьютеры тоже, в основном.

(позднее добавление) См., например, пакет спекуляции - "Рамка для безопасного, программируемого, спекулятивного parallelism".

И, конечно, V8, где "скомпилированный код дополнительно оптимизирован (и повторно оптимизирован) динамически во время выполнения на основе эвристики профиля выполнения кода".