haskell - 简化 boolean 表达式的函数

Question

我正在处理以下语法，它以 Haskell data 类型的形式实现。

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

我的问题是，我想编写一个函数 simplify::bool → bool ，它以通常的方式简化 boolean 表达式(而不对变量执行任何操作)。例如，我想要

    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₁ 和 b2 表示 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)       
                    = ...

因此，我的想法是保留旧的定义，但实际上通过找到固定点来简化。事实上，下面用 Haskell 编写的函数 simplify'::bool → bool 的行为符合预期:

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

这感觉像是一个不优雅的问题解决方案，因为它不断重复运行一个函数，感觉，如果定义正确，只需要运行一次。我很感激任何反馈。

Answer 1

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

will solve the problem, since it simplifies the results of conjunctions, which does actually work! But then it breaks when we have variables (it goes into an infinite loop in fact):

你真的想递归simplify(b₁)∧simplify(b2)吗？也许您想要simplify(b₁)和simplify(b2)，然后简单地操作它们。如，

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。