logic.mac

/* vim: ft=maxima
*/

/* generate a list of the 2^n different length n lists whose elements
 * are true or false
 */
tf(n) := if n=0 then [[]] else append(maplist(lambda([x], cons(true, x)), tf(n - 1)), maplist(lambda([x], cons(false, x)), tf(n - 1)));

/* prepare a list of the form [x=a, y=b, ...] where varlist = [x, y, ...] and vallist = [a, b, ...]
 * in stack this is 
 * zip_with(lambda([var, val], var = val),varlist,vallist)
 * but we don't have zip in vanilla maxima
 */
subst_list(varlist, vallist) := block([out, i],
    out : [],
    for i : 1 thru length(varlist) do (
        out : cons(varlist[i] = vallist[i], out)
    ),
    out
);

/* given a list of variables vars = [p, q, r, ...] and a
 * boolean function fn = fn(p, q, r, ... ) of n variables and an expr ex
 * in those variables, does the expression induce the same boolean
 * function?  return [true or false, list of counterexamples]
 */
log_equiv(ex, fn, vars) := block([is_equiv, counterex, n, tfs, subs],
    is_equiv : true,
    counterex : [],
    n : length(vars),
    tfs : tf(n),
    for assignment in tfs do (
        /* build the substitution */
        subs : subst_list(vars, assignment),
        /* do the substitution */
        bool : subst(subs, ex),
        if not is(bool = apply(fn, assignment)) then (
            /* they are not logically equiv, and assignment witnesses this */
            is_equiv : false,
            counterex : cons(assignment, counterex)
        ) 
    ),
    [is_equiv, counterex]
);

/* like log_equiv but for two expressions in the same set of variables */
log_eq(ex1, ex2) := block([vars1, vars2, is_equiv, counterex, n, tfs, subs],
    vars1 : listofvars(ex1),
    vars2 : listofvars(ex2),
    vars : listify(setify(append(vars1, vars2))),
    is_equiv : true,
    counterex : [],
    n : length(vars),
    tfs : tf(n),
    for assignment in tfs do ( 
        /* build the substitution */
        subs : subst_list(vars, assignment),
        /* do the substitution */
        bool1 : subst(subs, ex1),
        bool2 : subst(subs, ex2),
        if not is(bool1 = bool2) then (
            /* they are not logically equiv, and assignment witnesses this */
            is_equiv : false,
            counterex : cons(assignment, counterex)
        ) 
    ),
    [is_equiv, counterex]
);