Можно ли реализовать эту функцию в Haskell?

На странице https://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Pattern_Matching есть следующее упражнение:

Рассмотрим функцию or двух логических аргументов со следующими свойствами:

  • or ⊥ ⊥ = ⊥
  • или Истина ⊥ = Истина
  • или ⊥ Верно = Верно
  • или Ложь y = y
  • или х Ложь = х

Эта функция — еще один пример совместной строгости, но гораздо более острый: результатом будет ⊥, только если оба аргумента равны (по крайней мере, когда мы ограничиваем аргументы True и ⊥). Можно ли реализовать такую ​​функцию на Haskell?

Функцию можно представить в виде следующей таблицы:

      |   ⊥   | False | True
------|-----------------------
  ⊥   |   ⊥   |   ⊥   | True
False |   ⊥   | False | True
True  | True  | True  | True

Эта функция является монотонной в соответствии с определением, данным в https://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Monotonicity, поэтому я не вижу причин исключать возможность реализации этой функции в Haskell. Тем не менее, я не вижу способа реализовать это.

Какой ответ на упражнение?

PS: я понимаю, что ответ нет, вы не можете. Я ищу строгое доказательство. Я чувствую, что упускаю какое-то важное ограничение на то, какие функции могут быть определены. Определенно не все монотонные функции.


lazy-evaluation haskell strictness
person Federico    schedule 28.11.2019    source источник
comment
Вы не можете реализовать это, если только не полагаетесь на параллелизм для параллельной оценки обоих выражений (или на некоторые небезопасные функции, скрывающие параллелизм). Он существует в библиотеке как por< /a> для параллельного или.   -  person chi    schedule 28.11.2019
comment
@chi Не могли бы вы поделиться доказательством?   -  person Federico    schedule 28.11.2019
comment
@Federico Это проблема с остановкой. Учитывая or x y, вы должны оценить один из них, по крайней мере, чтобы определить, следует ли возвращать True или False. Какой бы из x или y вы ни выбрали, у вас есть шанс, что это будет расходящееся вычисление, даже если другое нет. Параллелизм позволяет вам оценивать каждый из них понемногу, так что если есть не самое низкое значение, вы в конце концов найдете его.   -  person chepner    schedule 28.11.2019
comment
У меня нет быстрой справки, но вы можете попробовать поискать в Google por в лямбда-исчислении и связанной с ним неудачей полной абстракции денотационной семантики. Я думаю, что где-то есть несколько слайдов Winskel (?).   -  person chi    schedule 28.11.2019
comment
@chepner Большое спасибо! Я приму это как ответ, если вы не возражаете опубликовать его.   -  person Federico    schedule 28.11.2019
comment
@chepner Я бы не стал связывать это с проблемой остановки, поскольку ее можно решить с помощью параллелизма. Я думаю, что это может ввести в заблуждение - если бы эта проблема была неразрешима из-за HP, никакой параллелизм не помог бы. К счастью, нам не нужно выбирать HP на x или y для вычисления por x y, поскольку мы можем выполнять вычисления одновременно. На мой взгляд, это больше связано с отсутствием параллелизма в лямбда-исчислении.   -  person chi    schedule 28.11.2019
comment
Я понимаю, что параллелизм просто означает, что вы просто обходите проверку на завершение. Предполагая, что один поток завершается, вас больше не волнует, завершится в конечном итоге другой поток или нет; ты просто сдаешься.   -  person chepner    schedule 28.11.2019
comment
Перефразируй; Я не пытаюсь определить, будет ли поток будет завершен, я просто переключаюсь на другой поток, если я еще не завершил еще. Если ни один поток не завершится, то и я тоже.   -  person chepner    schedule 28.11.2019

Ответы (2)


arrow_upward
7
arrow_downward

Предположим, вы попытаетесь оценить or x y. Для этого вам нужно выбрать тот или иной аргумент, чтобы увидеть, приведет ли его оценка к True или False. Если вы угадаете правильно, вы поймете, должен ли результат быть True или False, без необходимости оценивать другой аргумент (который может быть ⊥).

Однако если вы угадаете неправильно, вы никогда не закончите оценку аргумента; либо вы застрянете в бесконечном цикле, либо получите ошибку времени выполнения.

Параллелизм позволяет оценивать оба аргумента параллельно[1]. Если предположить, что один из двух аргументов оценивается как правильное Boolean, одна из двух ветвей успешно его найдет. Другая ветвь либо вызовет ошибку (в этом случае вы можете просто отбросить эту ветвь и проигнорировать ошибку), либо застрянет в цикле (который вы можете принудительно завершить, когда другая ветвь преуспеет). В любом случае, вы можете получить правильный ответ в конце концов.

Если оба аргумента приводят к ⊥, конечно, неявным результатом or все равно будет ⊥; вы не можете полностью обойти проблему остановки.

[1] Под «параллельным» я не обязательно подразумеваю разветвление другого процесса и их одновременную оценку. Вы можете оценить один аргумент для N шагов (для некоторого значения N и любого значения "шага"); если возникает ошибка, сдайтесь и попробуйте другой аргумент, а если вы еще не завершили работу, приостановите этот поток и попробуйте другой на N шагов. Продолжайте прыгать туда-сюда между ними, пока один из них не даст конкретное значение.

person chepner    schedule 28.11.2019

arrow_upward
6
arrow_downward

Пакет unamb использует параллелизм (и unsafePerformIO), как описано в ответе Чепнера, для реализации примитивов, с помощью которых можно определить параллельный or.

parOr :: Bool -> Bool -> Bool
parOr x y = (x || y) `unamb` (y || x)  -- unamb from Data.Unamb
person Li-yao Xia    schedule 28.11.2019