Proof of my CNF converter

定义：
一个句子是一个变量或一个满足下列条件的list，至少有3个元素，第一个元素是连词AND或OR，其余元素是句子（递归定义），这些句子称作子句。没有NOT这种连词。
称一个句子是CNF的，若它是一个变量或满足下列条件的list。第一个元素是AND，其余元素是变量或满足下列条件的list。第一个元素是OR，其余元素是变量。（非递归定义）
对偶地可以定义DNF。
称一个句子是melt的，若任何一个子句的连词都不同于这个句子的连词。显然CNF和DNF是melt的
称两个句子等价，若他们用到的变量相同，且对于任何一种变量分配，他们表达式求值后同真同假。
任何句子可以转化成等价的melt形式，只需要将多余的连词合并即可。

命题：
如果句子x1,...,xn都是melt的，则melt(Op,x1,...,xn)=[Op]+trim(x1,Op)+...+trim(xn,Op)也是melt的，其中Op是AND或OR
其中，trim(x,Op)=x[1:]若Op是x的连词，否则trim(x,Op)=[x]
证明：显然

命题：
如果句子x1,...,xn都是CNF的，
那么melt(AND,x1,...,xn)也是CNF的
证明：显然

命题：
如果句子x1,...,xn都是CNF的，将他们的子句（n个列向量）的卡氏积写成一串n阶向量y1,...,ym，|yk|=n，
那么AND,OR(y1),...,OR(ym)也是CNF的
证明：反复应用交换律即可。

基于上述命题，可知昨天的递归算法正确。

按照定义验证也很直接，只需代入全部可能的变量分配即可。python可以帮你方便地对表达式求值。
import itertools

def is_leaf(x):
    return type(x)==type("")

def to_str(x):
    return is_leaf(x) and x or "(" + (" "+x[0]+" ").join(map(lambda e : to_str(e), x[1:])) + ")"

def _nfy(x, O1, O2):
    if is_leaf(x):   return x
    if x[0]==O1:  return melt([O1] + map(lambda e : _nfy(e, O1, O2), x[1:]))
    return [O1] + [[O2]+list(c) for c in itertools.product(*map(lambda e : is_leaf(e) and [e] or _nfy(e, O1, O2)[1:], x[1:]))]       

def cnfy(x): return _nfy(x, "and", "or")

def dnfy(x): return _nfy(x, "or", "and")

def melt(x):
    if is_leaf(x): return x
    ret = x[:1]
    for e in x[1:]:
        if not is_leaf(e) and e[0]==ret[0]:   ret+=melt(e)[1:]
        else:                                 ret.append(melt(e))
    return ret

def terms(x):
    ret = set()
    q=[x]
    while len(q)>0:
        head = q.pop(0)
        if is_leaf(head):
            ret.add(head)
        else:
            q+=head[1:]
    return ret

def eq(x, y):
    xterms = terms(x)
    yterms = terms(y)
    if xterms != yterms:
        return False
    xstr=to_str(x)
    ystr=to_str(y)
    termlist = list(xterms)
    for assignment in itertools.product(*([("True", "False")]*len(termlist))):
        x1=xstr
        y1=ystr
        for i, a in enumerate(assignment):
            x1=x1.replace(termlist[i], a)
            y1=y1.replace(termlist[i], a)
        if eval(x1) != eval(y1):
            return False
    return True
       
def main():
    x = ["or", "x1", ["and", ["or", "x2", ["and", "x3", "x4", ["or", ["and", "x5", "x6"], "x7", ["or", ["and", "x8", "x9"], "x10"]]]], "x11"]]
    print terms(x)
    print eq(x, x),
    print eq(x, cnfy(x)),
    print eq(x, dnfy(x))
   
main()

P.S.
修正了_nfy函数最后一行：用不着melt