Упрощение логики в sml - PullRequest
Новая
       30

Упрощение логики в sml

2 голосов
/ 02 декабря 2011

Я создаю программу упрощения логики в sml. Но у меня есть проблема для этого ввода: 

- Or(Or(Var"x", Var"y"), Var"z");
val it = Or (Or (Var #,Var #),Var "z") : formula
 - Simplify it;

И это в бесконечном цикле.

Вот мой код: 

fun Simplify (Or(True, _)) = True
| Simplify (Or(_, True)) = True
| Simplify (Or(False, False)) = False
| Simplify (Or(x, False)) = (Simplify x)
| Simplify (Or(False, x)) = (Simplify x)
| Simplify (Or (Var (x), Var (y))) = Or (Var (x), Var (y))
| Simplify (Or (x, y)) = (Simplify (Or (Simplify x, Simplify y)))

| Simplify (And(_, False)) = False
| Simplify (And(False, _)) = False
| Simplify (And(True, True)) = True
| Simplify (And(True, x)) = (Simplify x)
| Simplify (And(x, True)) = (Simplify x)
| Simplify (And(Var (x), Var(y))) = And (Var (x), Var (y))
| Simplify (And (x, y)) = (Simplify (And (Simplify x, Simplify y)))

| Simplify (Not(Not(x))) = (Simplify x)
| Simplify (Not(True)) = False
| Simplify (Not(False)) = True
| Simplify (Not(Var (x))) = (Not (Var x))
| Simplify (Not(x)) = (Simplify (Not (Simplify x)))

| Simplify True = True
| Simplify False = False
| Simplify (Var(x)) = Var(x);

1 Ответ

3 голосов
/ 03 декабря 2011

Есть три случая, которые действительно подозрительны: 

| Simplify (Or (x, y)) = (Simplify (Or (Simplify x, Simplify y)))

| Simplify (And (x, y)) = (Simplify (And (Simplify x, Simplify y)))

| Simplify (Not(x)) = (Simplify (Not (Simplify x)))

В принципе, если x и y не могут быть упрощены в дальнейшем, Simplify x и Simplify y вернут x и y,Таким образом, вы будете вызывать Simplify с тем же вводом, что и раньше (Or(x, y), And(x, y) или Not x).Вы можете проверить, что ваша функция не заканчивается некоторыми примерами, такими как: And(And(Var "x", Var "y"), Var "z") и Not(And(Var "x", Var "y").

Идея упрощения заключается в том, что у вас есть True или False во внутреннем предложении,Вы хотите распространить это на внешние уровни.Обратите внимание, что вы не будете пытаться упростить, если x и y неприводимы.

ОБНОВЛЕНИЕ:

Ваша функция может быть исправлена ​​следующим образом: 

fun Simplify (Or(True, _)) = True
    | ... (* Keep other cases as before *)
    | Simplify (Or (x, y)) = (case Simplify x of
                                True => True
                              | False => Simplify y
                              | x' => (case Simplify y of
                                         True => True
                                       | False => x'
                                       | y' => Or(x', y')))

    | Simplify (And (x, y)) = (case Simplify x of
                                 False => False
                               | True => Simplify y
                               | x' => (case Simplify y of
                                          False => False
                                        | True => x'
                                        | y' => And(x', y')))
    | Simplify (Not x) = case Simplify x of
                             True => False
                           | False => True
                           | x' => Not x'

ОБНОВЛЕНИЕ 2:

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

fun Simplify True = True
 | Simplify False = False
 | Simplify (Var x) = Var x
 | Simplify (Not x) = (case Simplify x of
                         True => False
                       | False => True
                       | x' => Not x')
 | Simplify (And(x, y)) = (case Simplify x of
                             False => False
                           | True => Simplify y
                           | x' => (case Simplify y of
                                      False => False
                                    | True => x'
                                    | y' => And(x', y')))
 | Simplify (Or(x, y)) = (case Simplify x of
                            True => True
                          | False => Simplify y
                          | x' => (case Simplify y of
                                     True => True
                                   | False => x'
                                   | y' => Or(x', y')))
...