Каково математическое значение "все (==1) [1,1..] "не прекращается?

Интуитивно я ожидал бы, что "математический" ответ на all (==1) [1,1..] будет True, потому что все элементы в списке, который содержит только 1, равны 1. Однако я понимаю ,что" вычислительно "процесс вычисления бесконечного списка, чтобы проверить, что каждый элемент действительно равен 1, никогда не закончится,поэтому выражение вместо этого "вычисляет" до дна или ⊥.

Я нахожу этот результат противоестественным и немного нервирующим. Думаю, дело в том, что список является бесконечным один запутывает вопрос как математически, так и вычислительно, и я хотел бы услышать от любого, кто имеет некоторое понимание и опыт в этой области Мой вопрос в том, какой ответ является наиболее математически правильным? ⊥ или True? Было бы также весьма полезно уточнить, почему один ответ является более правильным, чем другой.

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

3 10
haskell data-structures computer-science

3 ответа:

Значение 

all (==1) [1,1..]

- наименьшая верхняя граница последовательности 

all (==1) (⊥)
all (==1) (1 : ⊥)
all (==1) (1 : 1 : ⊥)
...

И все члены этой последовательности являются ⊥, поэтому наименьшая верхняя граница также является ⊥. (Все функции Хаскелла непрерывны: сохраняют наименьшие верхние границы.)

Это использование денотационной семантики для Хаскелла и не зависит (напрямую) от выбора какой-либо конкретной стратегии оценки.

23

В программировании мы используем не классическую логику, а интуитивистскую (конструктивную) логику. Мы все еще можем интерпретировать типы как теоремы, но нас не волнует истинность этих теорем; вместо этого мы говорим о том, являются ли они конструктивно доказуемыми . Хотя all (== 1) [1, 1 ..] является истинным , мы не можем доказать это в Хаскелле, поэтому мы получаем ⊥ (здесь, бесконечный цикл).

В конструктивной логике у нас нет ни закона исключенной середины, ни двойного отрицания. в результате. Функция Хаскелла типа all (== 1) :: [Int] -> Bool не представляет теорему [Int] → Bool, которая была бы полной функцией; она представляет теорему [Int] → Bool. Если all может доказать теорему, произведя результат, то этот результат будет иметь тип Bool; в противном случае результат будет нижним.
3

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

Конечно, теперь было бы хорошо для понимания бесконечного списка как-то сказать all, что это бесконечный список единиц. Но... вот что там написано " by быть такой ценностью". Наличие немного более общих метаданных о повторяющейся последовательности было бы более успешным для целей оптимизации, но я думаю, что простота будет уменьшена, а сложность введена.
2