Функция, которая упрощает логические выражения - PullRequest
Новая
       7

Функция, которая упрощает логические выражения

0 голосов
/ 03 декабря 2018

Я имею дело со следующей грамматикой, которую я реализовал в виде типа Haskell data. 

    bool ::=   tt   |   ff   |   bool ∧ bool   |   var        
    var  ::=   letter{letter|digit}*

Мой вопрос, я хотел бы написать функцию simplify :: bool → bool, котораяупрощает логические выражения обычным способом (при этом ничего не делая с переменными).Например, я бы хотел 

    simplify(tt ∧ ff) = ff
    simplify(tt ∧ x) =  x
    simplify(x ∧ (y ∧ z)) = x ∧ y ∧ z

, где буквы x , y и z обозначают переменные (var).

Мне кажется, что естественным определением является следующее (псевдокод с сопоставлением с образцом) 

    simplify(tt) = tt
    simplify(ff) = ff
    simplify(x)  = x
    simplify(tt ∧ b) = simplify(b)
    simplify(b ∧ tt) = simplify(b)
    simplify(b₁ ∧ b₂) = simplify(b₁) ∧ simplify(b₂)                (†)

, где b , b₁ и b₂ обозначает bool с, а x обозначает var .

Это определение прекрасно работает для всех приведенных выше примеров.Проблема с такими выражениями, как (tt ∧ tt) ∧ (tt ∧ tt).Действительно, применяя определение, мы имеем 

    simplify((tt ∧ tt) ∧ (tt ∧ tt)) = simplify(tt ∧ tt) ∧ simplify(tt ∧ tt) 
                                    = simplify(tt) ∧ simplify(tt) 
                                    = tt ∧ tt

, который мы должны еще больше упростить до tt.

Таким образом, возможно, изменение строки определения (†) на 

    simplify(b₁ ∧ b₂) = simplify(simplify(b₁) ∧ simplify(b₂))

решит проблему, поскольку упрощает результаты соединений, что на самом деле работает!Но затем он ломается, когда у нас есть переменные (фактически, он входит в бесконечный цикл): 

    simplify(x ∧ y) = simplify(simplify(x) ∧ simplify(y))   
                    = simplify(x ∧ y)       
                    = ...

Таким образом, моя идея состояла в том, чтобы сохранить старое определение, но затем фактически упростить, найдя фиксированные точки.В самом деле, функция simplify' :: bool → bool, написанная на Хаскеле ниже, ведет себя так, как нужно: 

simplify' :: BoolExpr -> BoolExpr
simplify' f 
    | (simplify f) == f   = f
    | otherwise           = simplify' (simplify f)

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

Ответы [ 2 ]

0 голосов
/ 03 декабря 2018 
simplify(b₁ ∧ b₂) = simplify(simplify(b₁) ∧ simplify(b₂))

решит проблему, так как упрощает результаты соединений, что на самом деле работает!Но затем он ломается, когда у нас есть переменные (фактически, он входит в бесконечный цикл):

Вы действительно хотите рекурсировать более simplify(b₁) ∧ simplify(b₂)?Может быть, вы хотите simplify(b₁) и simplify(b₂), а затем просто управлять ими.Например, 

data B = T | F | V | B :&: B deriving Show

s :: B -> B
s T = T
s F = F
s V = V
s (b1 :&: b2) = opAND (s b1) (s b2) 

opAND F _ = F
opAND _ F = F 
opAND T b = b
opAND b T = b
opAND a b = a :&: b

Функция упрощения s существенно сворачивает ваше синтаксическое дерево, на каждом шаге гарантируя, что вы сохраняете свойство, что упрощенное выражение является либо атомарным, либо не содержит ни того, ни другого Fни T.

0 голосов
/ 03 декабря 2018

Фундаментальная проблема заключается в том, что вы проводите тест simplify(tt ∧ b) для не упрощенных выражений.

Логика, которую вы ищете, будет больше похожа на: 

simplify(a ^ b) | simplify(a) == tt = simplify b

, которая можетбыть эффективно реализованным путем упрощения обоих до упрощающего сопоставления с образцом: 

simplify(b₁ ∧ b₂) =
  case (simplify(b₁), simplify(b₂)) of
    (tt, x) -> x
    (x, tt) -> x
    ...
...