В этом упражнении вам предлагается провести подобную оптимизацию для логических значений. У
нас есть абстрактное синтаксическое дерево:
data Log
= True
| False
| Not Log
| Or
Log Log
| And Log Log
Напишите функцию, которая оптимизирует выражение Log. Эта функция приводит Log к конъюнктив-
ной нормальной форме (КНФ). Дерево в КНФ обладает такими свойствами: все узлы с Or находятся
ближе к корню чем узлы с And и все узлы с And находятся ближе к корню чем узлы с Not. В КНФ выра-
жения имеют вид:
(True ‘And‘ Not False ‘And‘ True) ‘Or‘ True ‘Or‘ (True ‘And‘ False)
(True ‘And‘ True ‘And‘ False) ‘Or‘ True
Как бы мы не шли от корня к листу сначала нам будут встречаться только операции Or, затем только
операции And, затем только Not.
КНФ замечательна тем, что её вычисление может пройти досрочно. КНФ можно представить так:
data Or’
a = Or’
[a]
data And’ a = And’ [a]
data Not’ a = Not’
a
data Lit
= True’ | False’
type CNF = Or’ (And’ (Not’ Lit))
Сначала идёт список выражений разделённых конструктором Or (вычислять весь список не нужно, нам
нужно найти первый элемент, который вернёт True). Затем идёт список выражений, разделённых And
(опять же его не надо вычислять целиком, нам нужно найти первое выражение, которое вернёт False).
В самом конце стоят отрицания.
В нашем случае приведение к КНФ состоит из двух этапов:
– Сначала построим выражение, в котором все конструкторы Or и And стоят ближе к корню чем
конструктор Not. Для этого необходимо воспользоваться такими правилами:
-- удаление двойного отрицания
Not (Not a)
==> a
-- правила де Моргана
Not (And a b) ==> Or
(Not a) (Not b)
Not (Or
a b) ==> And (Not a) (Not b)
124 | Глава 7: Функторы и монады: примеры
– Делаем так чтобы все конструкторы Or были бы ближе к корню чем конструкторы And. Для этого
мы воспользуемся правилом дистрибутивности:
And a (Or b c)
==> Or (And a b) (And a c)
При этом мы будем учитывать коммутативность And и Or:
And a b