简化布尔表达式的函数 [英] A Function which Simplifying Boolean Expressions

问题描述

我正在处理以下语法，这些语法已以Haskell data类型的形式实现.

I am dealing with the following grammar, which I have implemented in the form of a Haskell data type.

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

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

My question is, I would like to write a function simplify :: bool → bool which simplifies boolean expressions in the usual way (while doing nothing to variables). For example, I would like

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

其中字母 x ， y 和 z 表示变量(var).

where the letters x, y and z are denoting variables (var).

我认为自然定义如下(具有模式匹配的伪代码)

I feel that the natural definition is the following (pseudocode with pattern matching)

    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 .

where b, b₁ and b₂ denote bools, and x denotes a var.

该定义适用于上面所有给定的示例.问题出在诸如(tt ∧ tt) ∧ (tt ∧ tt)之类的表达式上.确实，应用定义，我们有

This definition works fine for all the given examples above. The problem is with expressions such as (tt ∧ tt) ∧ (tt ∧ tt). Indeed, applying the definition, we have

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

，我们应该能够进一步简化为tt.

which we should be able to further simplify as simply tt.

因此可能将定义线(†)更改为

Thus maybe changing the definition line (†) to

    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(x ∧ y) = simplify(simplify(x) ∧ simplify(y))   
                    = simplify(x ∧ y)       
                    = ...

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

Thus my idea was to retain the old definition, but then actually simplify by finding fixed points. Indeed, the function simplify' :: bool → bool written in Haskell below, behaves as desired:

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

感觉就像是对问题的不完美解决方案，因为它不断地重复运行感觉(如果定义正确)仅需要运行一次的功能.感谢您的反馈.

It just feels like an inelegant solution to the problem, since it keeps repeatedly running a function which feels like, if defined correctly, needs to be run only once. I appreciate any feedback.

推荐答案

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(b₂)吗?也许您想要simplify(b₁)和simplify(b₂)，然后简单地操作它们.就像

Do you really want to recurse over simplify(b₁) ∧ simplify(b₂)? Maybe you want to simplify(b₁) and simplify(b₂) and then simply operate them. As in,

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都不出现的属性.

The simplify function s essentially folds your syntax tree, at each step guaranteeing that you preserve the property that the simplified expression is either atomic, or contains no occurrences of neither F nor T.

这篇关于简化布尔表达式的函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！