modal_logic: sml.py@b7480b2e8fd2

     1 """

     2 Name: sml - Simple Modal Logic Lib.

     3 Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.

     4 Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>

     5 """

     6 import re

     8 def main():

     9     # edit your formulae here

    10     p = Variable(["p"])

    11     q = Variable(["q"])

    12     r = Variable(["r"])

    13     formula1 = Imp([Eq([p, q]), r])

    14     formula2 = Not([Or([p, q])])

    15     formula3 = Not([Not([p])])

    16     formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])])

    17     formula = formula4 # choose your formula here

    19     args = parse_arguments()

    20     if (args.formula):

    21         scanner = Scanner(TOKENS)

    22         parser = Parser(SYNTAX, scanner)

    23         (accepted, out, tree_nodes) = parser.parse(args.formula)

    24         if not accepted:

    25             print EXCUSE

    26             return

    27         tree = SyntaxTree(out, tree_nodes)

    28         formula = tree.root

    30     print "formula: \t\t\t%s (%i)" % (formula, formula.depth())

    31     formula = expand_imp_eq(formula)

    32     print "expanded -> and <->: \t\t%s (%i)" % (formula, formula.depth())

    33     formula = de_morgan(formula)

    34     print "reduced ~: \t\t\t%s (%i)" % (formula, formula.depth())

    35     formula = reduce_iter(formula)

    36     print "reduced iterated modalities: \t%s (%i)" % (formula, formula.depth())

    37     formula = reduce_iter(dist_mod((formula)))

    38     print "distributed modalities+: \t%s (%i)" % (formula, formula.depth())

    39     formula = mcnf(formula)

    40     print "alpha mcnf: \t\t\t%s (%i)" % (formula, formula.depth())

    42 def values(fun, f):

    43     return [fun(v) for v in f.values]

    45 def expand_imp_eq(formula):

    46     expmap = {IMP: lambda (a, b): Or([Not([a]), b]),

    47               EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}

    48     if not isinstance(formula, Operator):

    49         return formula

    50     if formula.id in expmap:

    51         return expmap[formula.id](values(expand_imp_eq, formula))

    52     return formula.__class__(values(expand_imp_eq, formula))

    54 def de_morgan(formula):

    55     negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),

    56               OR: lambda (a, b): And([negate(a), negate(b)]),

    57               BOX: lambda (a,): Diamond([negate(a)]),

    58               DIAMOND: lambda (a,): Box([negate(a)]),

    59               VARIABLE: lambda (a,): Not([Variable([a])]),

    60               NOT: lambda (a,): a}

    61     def negate(f):

    62         return negmap[f.id](f.values)

    63     if not isinstance(formula, Operator):

    64         return formula

    65     if formula.id == NOT:

    66         return negate(formula.values[0])

    67     return formula.__class__(values(de_morgan, formula))

    69 def reduce_iter(formula):

    70     redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))

    71     if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):

    72         return formula

    73     ids = (formula.id, formula.values[0].id)

    74     if ids in redset:

    75         return reduce_iter(formula.values[0])

    76     return formula.__class__(values(reduce_iter, formula))

    78 def dist_mod(formula):

    79     distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),

    80                (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),

    81                (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))

    82                and Or([Box([a]), Box([b])]) or Box([Or([a, b])]),

    83                (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))

    84                and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])}

    85     if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):

    86         return formula

    87     ids = (formula.id, formula.values[0].id)

    88     if ids in distmap:

    89         return distmap[ids](values(dist_mod, formula.values[0]))

    90     return formula.__class__(values(dist_mod, formula))

    92 def mcnf(formula):

    93     if formula.id == OR:

    94         conj_id = int(formula.values[1].id == AND)

    95         return And([Or([formula.values[conj_id].values[0], formula.values[1 - conj_id]]),

    96                     Or([formula.values[conj_id].values[1], formula.values[1 - conj_id]])]);

    98 NOT = "~"

    99 AND = "&"

   100 OR = "|"

   101 IMP = "->"

   102 EQ = "<->"

   103 BOX = "[]"

   104 DIAMOND = "<>"

   105 VARIABLE = "VAR"

   106 LB = "("

   107 RB = ")"

   109 class Operator(object):

   110     def __init__(self, id, arity, values):

   111         self.id = id

   112         self.arity = arity

   113         self.values = values

   114     def depth(self):

   115         if self.arity == 0:

   116             return 0

   117         if self.id in (BOX, DIAMOND):

   118             return 1 + self.values[0].depth()

   119         if self.id == NOT:

   120             return self.values[0].depth()

   121         return max(self.values[0].depth(), self.values[1].depth())

   122     def __str__(self):

   123         out = self.id

   124         if self.arity == 0:

   125             out = str(self.values[0])

   126         if self.arity == 1:

   127             out = self.id + str(self.values[0])

   128         elif self.arity  == 2:

   129             out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"

   130         return out

   132 class Not(Operator):

   133     arity = 1

   134     def __init__(self, values):

   135         Operator.__init__(self, NOT, Not.arity, values)

   136     def __call__(self):

   137         pass

   139 class And(Operator):

   140     arity = 2

   141     def __init__(self, values):

   142         Operator.__init__(self, AND, And.arity, values)

   144 class Or(Operator):

   145     arity = 2

   146     def __init__(self, values):

   147         Operator.__init__(self, OR, Or.arity, values)

   149 class Imp(Operator):

   150     arity = 2

   151     def __init__(self, values):

   152         Operator.__init__(self, IMP, Imp.arity, values)

   154 class Eq(Operator):

   155     arity = 2

   156     def __init__(self, values):

   157         Operator.__init__(self, EQ, Eq.arity, values)

   159 class Box(Operator):

   160     arity = 1

   161     def __init__(self, values):

   162         Operator.__init__(self, BOX, Box.arity, values)

   164 class Diamond(Operator):

   165     arity = 1

   166     def __init__(self, values):

   167         Operator.__init__(self, DIAMOND, Diamond.arity, values)

   169 class Variable(Operator):

   170     arity = 0

   171     def __init__(self, values):

   172         Operator.__init__(self, VARIABLE, Variable.arity, values)

   174 class Lb(Operator):

   175     arity = -1

   176     def __init__(self, values):

   177         Operator.__init__(self, LB, Lb.arity, values)

   179 class Rb(Operator):

   180     arity = -1

   181     def __init__(self, values):

   182         Operator.__init__(self, RB, Rb.arity, values)

   184 class Formula(object):

   185     def __init__(self):

   186         pass

   188 TOKENS = {re.compile("\("): Lb,

   189           re.compile("\)"): Rb,

   190           re.compile("~"): Not,

   191           re.compile("&"): And,

   192           re.compile("\|"): Or,

   193           re.compile("->"): Imp,

   194           re.compile("<->"): Eq,

   195           re.compile("\[\]"): Box,

   196           re.compile("<>"): Diamond,

   197           re.compile("[a-z]+"): Variable}

   199 class Scanner(object):

   200     def __init__(self, tokens, source=None):

   201         self.tokens = tokens

   202         self.reset(source)

   203     def next(self):

   204         while self.i < len(self.source):

   205             re.purge()

   206             for p, token in self.tokens.iteritems():

   207                 m = p.match(self.source[self.i:])

   208                 if m:

   209                     self.i += m.end(0)

   210                     value = m.group(0)

   211                     return (token, value)

   212             self.i += 1

   213         return (None, None)

   214     def reset(self, source):

   215         self.i = 0

   216         self.source = source

   218 S = Formula

   219 A = "A"

   220 #0 S: (Variable,),

   221 #1 S: (Not, S),

   222 #2 S: (Lb, A, Rb),

   223 #3 S: (Box, S),

   224 #4 S: (Diamond, S),

   225 #5 A: (S, And, S),

   226 #6 A: (S, Or, S),

   227 #7 A: (S, Imp, S),

   228 #8 A: (S, Eq, S)

   229 SYNTAX = ((Variable,),

   230           (Not, S),

   231           (Lb, A, Rb),

   232           (Box, S),

   233           (Diamond, S),

   234           (S, And, S),

   235           (S, Or, S),

   236           (S, Imp, S),

   237           (S, Eq, S))

   239 class Node(object):

   240     def __init__(self, parent, value):

   241         self.parent = parent

   242         self.value = value

   243         self.children = []

   244     def addChild(self, value):

   245         self.children.append(self, node)

   247 class Parser(object):

   248     def __init__(self, syntax, scanner):

   249         self.syntax = syntax

   250         self.scanner = scanner

   251     def parse(self, source):

   252         table = {(S, Variable): 0,

   253                  (S, Not): 1,

   254                  (S, Lb): 2,

   255                  (S, Box): 3,

   256                  (S, Diamond): 4,

   257                  (A, S, And): 5,

   258                  (A, S, Or): 6,

   259                  (A, S, Imp): 7,

   260                  (A, S, Eq): 8,

   261                  (A, Variable, And): 5,

   262                  (A, Variable, Or): 6,

   263                  (A, Variable, Imp): 7,

   264                  (A, Variable, Eq): 8,

   265                  (A, Not, Variable, And): 5,

   266                  (A, Not, Variable, Or): 6,

   267                  (A, Not, Variable, Imp): 7,

   268                  (A, Not, Variable, Eq): 8}

   269         stack = [S]

   270         tree_nodes = []

   271         tree = None

   272         out = []

   273         self.scanner.reset(source)

   274         (token, value) = self.scanner.next()

   275         (lookahead, la_value) = self.scanner.next()

   276         (lookahead2, la2_value) = self.scanner.next()

   277         accepted = True

   278         while token and len(stack):

   279             top = stack[-1]

   280             if top == token:

   281                 tree_nodes.append((token, value))

   282                 stack.pop()

   283                 #tree_nodes.append((stack.pop(), value))

   284                 (token, value) = (lookahead, la_value)

   285                 (lookahead, la_value) = (lookahead2, la2_value)

   286                 #(lookahead, _) = self.scanner.next()

   287                 (lookahead2, la2_value) = self.scanner.next()

   288             else:

   289                 action = None

   290                 if (top, token) in table:

   291                     action = table[(top, token)]

   292                 elif (top, token, lookahead) in table:

   293                     action = table[(top, token, lookahead)]

   294                 elif (top, token, lookahead, lookahead2) in table:

   295                     action = table[(top, token, lookahead, lookahead2)]

   296                 if action is None:

   297                     accepted = False

   298                     break

   300                 out.append(action)

   301                 stack.pop()

   302                 stack.extend(reversed(self.syntax[action]))

   303         accepted = accepted and not len(stack)

   304         return (accepted, out, tree_nodes)

   306 class SyntaxTree(object):

   307     def __init__(self, seq, tree_nodes):

   308         seq.reverse()

   309         tree_nodes.reverse()

   310         self.root = self.compile(seq, tree_nodes)[0]

   311     def compile(self, seq, tree_nodes):

   312         stack = []

   313         while len(seq):

   314             s = seq.pop()

   315             if s == 0:

   316                 c, v = tree_nodes.pop()

   317                 while c != Variable:

   318                     c, v = tree_nodes.pop()

   319                 stack.append(Variable(v))

   320             elif s == 1:

   321                 stack.append(Not(self.compile(seq, tree_nodes)))

   322             elif s == 2:

   323                 stack.extend(self.compile(seq, tree_nodes))

   324             elif s == 3:

   325                 stack.append(Box(self.compile(seq, tree_nodes)))

   326             elif s == 4:

   327                 stack.append(Diamond(self.compile(seq, tree_nodes)))

   328             elif s == 5:

   329                 stack.append(And(self.compile(seq, tree_nodes)))

   330             elif s == 6:

   331                 stack.append(Or(self.compile(seq, tree_nodes)))

   332             elif s == 7:

   333                 stack.append(Imp(self.compile(seq, tree_nodes)))

   334             elif s == 8:

   335                 stack.append(Eq(self.compile(seq, tree_nodes)))

   336         return stack

   338 from argparse import ArgumentParser

   340 def parse_arguments():

   341     parser = ArgumentParser(description="Parses simple modal logic syntax.")

   342     parser.add_argument("-f", "--formula", help="your formula")

   343     return parser.parse_args()

   345 EXCUSE = """The formula was not accepted by me, because I do not like you. It is not personal. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""

   347 if __name__ == "__main__":

   348     main()

author	Eugen Sawin <sawine@me73.com>
	Wed, 18 May 2011 03:51:08 +0200
changeset 21	b7480b2e8fd2
parent 20	1f97011ea795
child 22	53f84d131998
permissions	-rw-r--r--