Symbolic Boolean Expressions

We define a simple variable type:

     type var == char;

We represent Boolean expressions by trees:

     infixrl IMPLIES: 1;
     infix   OR: 2;
     infix   AND: 3;

     data bexp ==    VAR var ++ bexp AND bexp ++ bexp OR bexp ++
                     NOT bexp ++ bexp IMPLIES bexp;

We define an assignment as a list assigning Boolean values to variables:

     type assignment == list(var # truval);

Now define a function to evaluate a Boolean expression with respect to an assignment of Boolean values to the variables it contains:

     dec lookup : alpha # list(alpha#beta) -> beta;
     --- lookup(a, (key, datum)::rest) <=
             if a = key then datum else lookup(a, rest);

     dec evaluate : bexp # assignment -> truval;
     --- evaluate(VAR v, a) <= lookup(v, a);
     --- evaluate(e1 AND e2, a) <= evaluate(e1, a) and evaluate(e2, a);
     --- evaluate(e1 OR e2, a) <= evaluate(e1, a) or evaluate(e2, a);
     --- evaluate(NOT e, a) <= not(evaluate(e, a));
     --- evaluate(e1 IMPLIES e2, a) <=
             not(evaluate(e1, a)) or evaluate(e2, a);

     evaluate (VAR 'a' AND VAR 'b' OR VAR 'c',
               [('a', false), ('b', true), ('c', false)]);

     evaluate (VAR 'a' AND VAR 'b' OR VAR 'c',
               [('a', true), ('b', true), ('c', false)]);

We intend to use this function in a function to test whether any Boolean expression is a tautology, i.e. is true for any assignment of its variables. First, we need a function to extract the list of variables in an expression. The following function merges two ordered lists to form an ordered list without duplicates:

     dec merge : list alpha # list alpha -> list alpha;
     --- merge([], l) <= l;
     --- merge(l, []) <= l;
     --- merge(x1::l1, x2::l2) <=
             if x1 = x2 then x1::merge(l1, l2)
             else if x1 < x2 then x1::merge(l1, x2::l2)
                             else x2::merge(x1::l1, l2);

The next function returns the ordered list of variables in a Boolean expression, without duplicates:

     dec vars : bexp -> list var;
     --- vars(VAR v) <= [v];
     --- vars(e1 AND e2) <= merge(vars e1, vars e2);
     --- vars(e1 OR e2) <= merge(vars e1, vars e2);
     --- vars(NOT e) <= vars e;
     --- vars(e1 IMPLIES e2) <= merge(vars e1, vars e2);

     vars (VAR 'a' AND VAR 'b' OR VAR 'a');

     vars ((VAR 'a' IMPLIES VAR 'b' IMPLIES VAR 'c') IMPLIES
             (VAR 'a' IMPLIES VAR 'b') IMPLIES
             VAR 'a' IMPLIES VAR 'c');

Now we want to generate the the list of all possible assignments to a list of variables:

     uses list;

     dec interpretations: list var -> list assignment;
     --- interpretations [] <= [[]];
     --- interpretations(h::t) <=
             (map ((h, false)::) l <> map ((h, true)::) l)
             where l == interpretations t;

     interpretations "a";

     interpretations "ab";

     interpretations "abc";

Finally, we put all these together. An expression is a tautology if it evaluates to true for all possible assignments to the variables it contains:

     dec tautology: bexp -> truval;
     --- tautology e <=
             foldr(true, (and))
                     (map evaluate
                             (dist(e, interpretations(vars(e)))));

     tautology (VAR 'a' AND VAR 'b' OR VAR 'a');

     tautology ((VAR 'a' IMPLIES VAR 'b' IMPLIES VAR 'c') IMPLIES
                     (VAR 'a' IMPLIES VAR 'b') IMPLIES
                     VAR 'a' IMPLIES VAR 'c');