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