Python nested lists and recursion problem

Question

Hi guys,

I'm trying to process a first order logic formula represented as nested lists and strings in python so that that its in disjunctive normal form,

i.e ['&', ['|', 'a', 'b'], ['|', 'c', 'd']]

turns into

['|' ['&', ['&', 'a', 'c'], ['&', 'b', 'c']], ['&', ['&', 'a', 'd'], ['&', 'b', 'd']]]

where | is 'or' and & is 'and'.

currently im using a recursive implementation which does several passes over a formula until it can't find any nested 'or' symbols inside a list argument for 'ands'.

This is my implementation, performDNF(form) is the entry point. Right now it performs a single pass over the formula but then the while loop checking function finds no '|'s inside of '&'s and terminates, help anyone this is driving me mad.

def dnfDistributivity(self, form):
    if isinstance(form, type([])):
        if len(form) == 3:
            if form[0] == '&':
                if form[1][0] == '|':
                    form = ['|', ['&', form[2], form[1][1]], ['&', form[2], form[1][2]]]
                elif form[2][0] == '|':
                    form = ['|', ['&', form[1], form[2][1]], ['&', form[1], form[2][2]]]
            form[1] = self.dnfDistributivity(form[1])
            form[2] = self.dnfDistributivity(form[2])
        elif len(form) == 2:
            form[1] = self.dnfDistributivity(form[1])
    return form

def checkDistributivity(self, form, result = 0):
    if isinstance(form, type([])):
        if len(form) == 3:
            if form[0] == '&':
                print "found &"
                if isinstance(form[1], type([])):
                    if form[1][0] == '|':
                        return 1
                elif isinstance(form[2], type([])):
                    if form[2][0] == '|':
                        return 1
                else:
                    result = self.checkDistributivity(form[1], result)
                    print result
                    if result != 1:
                        result = self.checkDistributivity(form[2], result)
                        print result
        elif len(form) == 2:
            result = self.checkDistributivity(form[1], result)
            print result
    return result

def performDNF(self, form):
    while self.checkDistributivity(form):
        form = self.dnfDistributivity(self.dnfDistributivity(form))
    return form

Answer 1

I didn't really try to understand your solution, sorry. I think it is way too difficult to read and probably the approach is too cumbersome.

If you have a DNF, all you need to do is find all combinations of atoms, taking one out of each sublist. This pretty much boils down to this problem ... from each OR-subclause you need to take one atom, and combine all those with AND.

The OR-combination of all those possible AND-clauses yields your desired result. Right?

Answer 2

Okay, here is an actual solution that seems to work.

I do not understand your code, and I hadn't heard of DNF, so I started out by studying the problem some more.

The Wikipedia page on DNF was very helpful. It included a grammar that describes DNF.

Based on that, I wrote a simple set of recursive functions that I believe correctly recognize DNF in the format you require. My code includes some simple test cases.

Then I realized that the binary tree nature of your data representation makes it relatively simple to apply DeMorgan's laws to simplify the 'not' case, by writing a function called negate() that recursively negates, and the rest fell into place.

I have included test cases. It seems to work.

I have no further plans to work on this. If someone finds a bug, please provide a test case and I'll look at it.

This code should run on any Python version 2.4 or newer. You could even port it to older Python versions by replacing the frozenset with a simple list of characters. I tested with Python 3.x, and found the exception syntax has changed, so you will need to change the raise lines if you want to run it under Python 3; the important parts all work.

In the question, you did not mention what character you use for not; given your use of & for and and | for or, I assumed you likely use ! for not and wrote the code accordingly. This is one of the things that puzzles me about your code: don't you ever expect to find not in your input?

I had some fun working on this. It's not as pointless as a sudoku puzzle.

import sys


ch_and = '&'
ch_not = '!'
ch_or = '|'

def echo(*args):
    # like print() in Python 3 but works in 2.x or in 3
    sys.stdout.write(" ".join(str(x) for x in args) + "\n")

try:
    symbols = frozenset([ch_and, ch_not, ch_or])
except NameError:
    raise Exception, "sorry, your Python is too old for this code"

try:
    __str_type = basestring
except NameError:
    __str_type = str


def is_symbol(x):
    if not isinstance(x, __str_type) or len(x) == 0:
        return False
    return x[0] in symbols

def is_and(x):
    if not isinstance(x, __str_type) or len(x) == 0:
        return False
    return x[0] == ch_and

def is_or(x):
    if not isinstance(x, __str_type) or len(x) == 0:
        return False
    return x[0] == ch_or

def is_not(x):
    if not isinstance(x, __str_type) or len(x) == 0:
        return False
    return x[0] == ch_not

def is_literal_char(x):
    if not isinstance(x, __str_type) or len(x) == 0:
        return False
    return x[0] not in symbols

def is_list(x, n):
    return isinstance(x, list) and len(x) == n


def is_literal(x):
    """\
True if x is a literal char, or a 'not' followed by a literal char."""
    if is_literal_char(x):
        return True
    return is_list(x, 2) and is_not(x[0]) and is_literal_char(x[1])


def is_conjunct(x):
    """\
True if x is a literal, or 'and' followed by two conjuctions."""
    if is_literal(x):
        return True
    return (is_list(x, 3) and
            is_and(x[0]) and is_conjunct(x[1]) and is_conjunct(x[2]))


def is_disjunct(x):
    """\
True if x is a conjunction, or 'or' followed by two disjuctions."""
    if is_conjunct(x):
        return True
    return (is_list(x, 3) and
            is_or(x[0]) and is_disjunct(x[1]) and is_disjunct(x[2]))



def is_dnf(x):
    return is_disjunct(x)

def is_wf(x):
    """returns True if x is a well-formed list"""
    if is_literal(x):
        return True
    elif not isinstance(x, list):
        raise TypeError, "only lists allowed"
    elif len(x) == 2 and is_not(x[0]) and is_wf(x[1]):
        return True
    else:
        return (is_list(x, 3) and (is_and(x[0]) or is_or(x[0])) and
                is_wf(x[1]) and is_wf(x[2]))

def negate(x):
    # trivial: negate a returns !a
    if is_literal_char(x):
        return [ch_not, x]

    # trivial: negate !a returns a
    if is_list(x, 2) and is_not(x[0]):
        return x[1]

    # DeMorgan's law:  negate (a && b) returns (!a || !b)
    if is_list(x, 3) and is_and(x[0]):
        return [ch_or, negate(x[1]), negate(x[2])]

    # DeMorgan's law:  negate (a || b) returns (!a && !b)
    if is_list(x, 3) and is_or(x[0]):
        return [ch_and, negate(x[1]), negate(x[2])]

    raise ValueError, "negate() only works on well-formed values."

def __rewrite(x):
    # handle all dnf, which includes simple literals.
    if is_dnf(x):
        # basis case. no work to do, return unchanged.
        return x

    if len(x) == 2 and is_not(x[0]):
        x1 = x[1]
        if is_list(x1, 2) and is_not(x1[0]):
            # double negative!  throw away the 'not' 'not' and keep rewriting.
            return __rewrite(x1[1])
        assert is_list(x1, 3)
        # handle non-inner 'not'
        return __rewrite(negate(x1))

    # handle 'and' with 'or' inside it
    assert is_list(x, 3) and is_and(x[0]) or is_or(x[0])
    if len(x) == 3 and is_and(x[0]):
        x1, x2 = x[1], x[2]
        if ((is_list(x1, 3) and is_or(x1[0])) and
                (is_list(x2, 3) and is_or(x2[0]))):
# (a || b) && (c || d) -- (a && c) || (b && c) || (a && d) || (b && d)
            lst_ac = [ch_and, x1[1], x2[1]]
            lst_bc = [ch_and, x1[2], x2[1]]
            lst_ad = [ch_and, x1[1], x2[2]]
            lst_bd = [ch_and, x1[2], x2[2]]
            new_x = [ch_or, [ch_or, lst_ac, lst_bc], [ch_or, lst_ad, lst_bd]]
            return __rewrite(new_x)

        if (is_list(x2, 3) and is_or(x2[0])):
# a && (b || c)  -- (a && b) || (a && c)
            lst_ab = [ch_and, x1, x2[1]]
            lst_ac = [ch_and, x1, x2[2]]
            new_x = [ch_or, lst_ab, lst_ac]
            return __rewrite(new_x)

        if (is_list(x1, 3) and is_or(x1[0])):
# (a || b) && c  -- (a && c) || (b && c)
            lst_ac = [ch_and, x1[1], x2]
            lst_bc = [ch_and, x1[2], x2]
            new_x = [ch_or, lst_ac, lst_bc]
            return __rewrite(new_x)

    return [x[0], __rewrite(x[1]), __rewrite(x[2])]
    #return x

def rewrite(x):
    if not is_wf(x):
        raise ValueError, "can only rewrite well-formed lists"
    while not is_dnf(x):
        x = __rewrite(x)
    return x


#### self-test code ####

__failed = False
__verbose = True
def test_not_wf(x):
    global __failed
    if is_wf(x):
        echo("is_wf() returned True for:", x)
        __failed = True

def test_dnf(x):
    global __failed
    if not is_wf(x):
        echo("is_wf() returned False for:", x)
        __failed = True
    elif not is_dnf(x):
        echo("is_dnf() returned False for:", x)
        __failed = True

def test_not_dnf(x):
    global __failed
    if not is_wf(x):
        echo("is_wf() returned False for:", x)
        __failed = True
    elif is_dnf(x):
        echo("is_dnf() returned True for:", x)
        __failed = True
    else:
        xr = rewrite(x)
        if not is_wf(xr):
            echo("rewrite produced non-well-formed for:", x)
            echo("result was:", xr)
            __failed = True
        elif not is_dnf(xr):
            echo("rewrite failed for:", x)
            echo("result was:", xr)
            __failed = True
        else:
            if __verbose:
                echo("original:", x)
                echo("rewritten:", xr)
                echo()

def self_test():
    a, b, c, d = 'a', 'b', 'c', 'd'
    test_dnf(a)
    test_dnf(b)
    test_dnf(c)
    test_dnf(d)

    lstna = [ch_not, a]
    test_dnf(lstna)

    lstnb = [ch_not, b]
    test_dnf(lstnb)

    lsta = [ch_and, a, b]
    test_dnf(lsta)

    lsto = [ch_or, a, b]
    test_dnf(lsto)

    test_dnf([ch_and, lsta, lsta])

    test_dnf([ch_or, lsta, lsta])

    lstnn = [ch_not, [ch_not, a]]
    test_not_dnf(lstnn)

    test_not_dnf([ch_and, lstnn, lstnn])

    # test 'and'/'or' inside 'not'
    test_not_dnf([ch_not, lsta])
    test_not_dnf([ch_not, lsto])

    # test 'or' inside of 'and'
    # a&(b|c) --> (a&b)|(b&c)
    test_not_dnf([ch_and, a, [ch_or, b, c]])
    # (a|b)&c --> (a&c)|(b&c)
    test_not_dnf([ch_and, [ch_or, a, b], c])
    # (a|b)&(c|d) --> ((a&c)|(b&c))|((a&d)|(b&d))
    test_not_dnf([ch_and, [ch_or, a, b], [ch_or, c, d]])

    # a&a&a&(b|c) --> a&a&(a&b|b&c) --> a&(a&a&b|a&b&c) --> (a&a&a&b|a&a&b&c)
    test_not_dnf([ch_and, a, [ch_and, a, [ch_and, a, [ch_or, b, c]]]])

    if __failed:
        echo("one or more tests failed")

self_test()

Now, I'm sorry to say this, but the more I think about it, the more I think you probably just got me to do your homework for you. So, I just wrote an improved version of this code, but I'm not planning to share it here; I'll leave it as an exercise for you. You should be able to do it easily, after I describe it.

It's a horrible hack that I have a while loop repeatedly calling __rewrite(). The rewrite() function should be able to rewrite the tree structure with a single call to __rewrite(). With just a few simple changes, you can get rid of the while loop; I did it, and tested it, and it works. You want __rewrite() to walk the tree down and then rewrite stuff on the way back up, and it will work in one pass. You could also modify __rewrite() to return an error if the list isn't well-formed, and get rid of the call to is_wf(); that's also easy.

I suspect your teacher would dock you points for the while loop, so you should be motivated to try this. I hope you have fun doing it, and I hope you learned something useful from my code.