Logic simplification in sml

Question

I'm creating logic simplification program in sml. But I have a problem for this input:

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

And it's in an infinite loop.

Here is my code:

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);

Answer 1

There are three cases which are really suspicious:

| 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)))

Basically, if x and y couldn't be simplified further, Simplify x and Simplify y will return x and y. So you will invoke Simplify with the same input as before (Or(x, y), And(x, y) or Not x). You can test that your function doesn't terminate with some examples such as: And(And(Var "x", Var "y"), Var "z") and Not(And(Var "x", Var "y").

The idea of simplification is that you have True or False in an inner clause, you want to propagate it to outer levels. Note that you will not try to simplify if x and y are irreducible.

UPDATE:

Your function could be fixed as follows:

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'

UPDATE 2:

I think you tried to use top-down approach which is not really appropriate. I rewrite the function using bottom-up approach to make it shorter and more readable:

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')))