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

Question

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

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

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

Answer 1

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

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

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

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

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

Answer 2

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

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

Answer 3

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

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

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

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

---

(позднего добавление) Смотри, например, the speculation package - "Основа для безопасной, программируемой, спекулятивной параллельности".

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

Answer 4

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

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