1
2
3
4
5
6
7
8
9
10 """
11 This module provides data structures for representing first-order
12 models.
13 """
14
15 from nltk_lite.semantics import logic
16
17 from pprint import pformat
18
19 -class Error(Exception): pass
20
22
24 """
25 A dictionary which represents a curryed characteristic function.
26 """
27
33
34
36 """Check whether a set represents a relation (of any arity)."""
37
38 assert isinstance(s, set), "Argument is not a set"
39 if len(s) == 0:
40 return True
41 elif not isinstance(max(s),tuple) or len(max(s))==len(min(s)):
42 return True
43 else:
44 raise ValueError, "Set contains sequences of different lengths"
45
47 """
48 Given an input such as the triple ('a', 'b', 'c'), return the L{CharFun}
49 {'c': {'b': {'a' : True}}}
50
51 @return: A characteristic function corresponding to the input.
52 @rtype: L{CharFun}
53 @param item: a literal or a tuple
54 """
55
56 chf = {}
57 if isinstance(item, tuple):
58
59 l = list(item)
60 l.reverse()
61 item = tuple(l)
62 if len(item)==1:
63 chf[item[0]] = True
64 elif len(item) > 1:
65 chf[item[0]] = self._item2dict(item[1:])
66 else:
67 chf[item] = True
68 return chf
69
71 k = chf2.keys()[0]
72 if k not in chf1:
73 chf1.update(chf2)
74 else:
75 self._merge(chf1[k], chf2[k])
76 return chf1
77
79 """
80 Convert an M{n}-ary relation into its corresponding characteristic function.
81 @rtype: L{CharFun}
82 @type s: set
83 """
84
85 assert isrel(s)
86
87 charfuns = []
88 for item in s:
89 charfuns.append(self._item2dict(item))
90
91 chf = reduce(self._merge, charfuns, {})
92 self.update(chf)
93
95 """
96 Convert a L{CharFun} back into a set of tuples.
97
98 Given an input such as the L{CharFun} {'c': {'b': {'a': True}}},
99 return set([('a', 'b', 'c')])
100 """
101 n = depth(self)
102 if n == 1:
103 tuples = self.domain
104 elif n == 2:
105 tuples = [(k2, k1) for k1 in self.keys() for k2 in self[k1].keys()]
106 elif n == 3:
107 tuples = [(k3, k2, k1) for k1 in self.keys() for k2 in self[k1].keys() for k3 in self[k1][k2].keys()]
108 else:
109 raise Error, "Only defined for CharFuns of depth <= 3"
110 result = set(tuples)
111 return result
112
113
114
115
116
117 - def _getDomain(self):
119
120 domain = property(_getDomain, doc='Set-theoretic domain of a curried function')
121
122
124 """
125 Check whether a set represents a relation (of any arity).
126
127 @param s: a set containing tuples
128 @type s: set
129 """
130
131 assert isinstance(s, set), "Argument is not a set"
132 if len(s) == 0:
133 return True
134 elif not isinstance(max(s),tuple) or len(max(s))==len(min(s)):
135 return True
136 else:
137 raise ValueError, "Set contains sequences of different lengths"
138
140 """
141 @return: The set of keys of a L{CharFun} instance.
142 @rtype: set
143 @type d: dict
144 """
145 flat = []
146 try:
147 flat.extend(d.keys())
148 for v in d.values():
149 if isinstance(v, dict):
150 flat.extend(flatten(v))
151 else:
152 flat.append(v)
153 except AttributeError:
154 flat.append(d)
155 result = set(flat)
156 result.discard(True)
157 return result
158
159
161 """
162 Calculate the depth of a L{CharFun}.
163
164 @rtype: C{int}
165 @type cf: L{CharFun}
166 """
167 if True in cf.values():
168 return 1
169 else:
170 key = cf.keys()[0]
171 return 1+depth(cf[key])
172
173
175 """
176 A dictionary which represents a model-theoretic Valuation of non-logical constants.
177
178
179 An attempt to initialize a L{Valuation} with an individual
180 variable expression (e.g., 'x3') will raise an error, as will an
181 attemp to read a list containing an individual variable
182 expression.
183
184 An instance of L{Valuation} will raise a KeyError exception (i.e.,
185 just behave like a standard dictionary) if indexed with an expression that
186 is not in its list of symbols.
187 """
189 dict.__init__(self)
190 if valuation:
191 for k in valuation.keys():
192 if logic.is_indvar(k):
193 raise Error, "This looks like an individual variable: '%s'" % k
194
195 if isinstance(valuation[k], bool):
196 self[k] = valuation[k]
197 else:
198 try:
199 cf = CharFun(valuation[k])
200 self[k] = cf
201 except (TypeError, ValueError):
202 self[k] = valuation[k]
203
209
210 - def read(self, seq):
211 """
212 Parse a list such as C{[('j', 'b1'), ('girl', set(['g1', 'g2']))]} into a L{Valuation}.
213 @rtype: L{Valuation}
214 @param seq: A list of tuples of the form (I{constant}, I{relation}), where I{relation} is a set of tuples.
215 """
216 d = dict(seq)
217 for k in d.keys():
218 if logic.is_indvar(k):
219 raise Error, "This looks like an individual variable: '%s'" % k
220 val = d[k]
221 if isinstance(val, str):
222 pass
223 else:
224 cf = CharFun()
225 cf.read(d[k])
226 d[k] = cf
227 self.update(d)
228
231
232 - def _getDomain(self):
233 dom = set()
234 for v in self.values():
235 flat = flatten(v)
236 dom = dom.union(flat)
237 return dom
238
239 domain = property(_getDomain,
240 doc='Set-theoretic domain of the value-space of a Valuation.')
241
244
245 symbols = property(_getSymbols,
246 doc='The non-logical constants which the Valuation recognizes.')
247
248
250 """
251 A dictionary which represents an assignment of values to variables.
252
253 An assigment can only assign values from its domain.
254
255 If an unknown expression M{a} is passed to a model M{M}'s
256 interpretation function M{i}, M{i} will first check whether M{M}'s
257 valuation assigns an interpretation to M{a} as a constant, and if
258 this fails, M{i} will delegate the interpretation of M{a} to
259 M{g}. M{g} only assigns values to individual variables (i.e.,
260 members of the class L{IndVariableExpression} in the L{logic}
261 module. If a variable is not assigned a value by M{g}, it will raise
262 an C{Undefined} exception.
263 """
264 - def __init__(self, domain, assignment=None):
265 dict.__init__(self)
266 self.domain = domain
267 if assignment:
268 for var in assignment.keys():
269 val = assignment[var]
270 assert val in self.domain,\
271 "'%s' is not in the domain: %s" % (val, self.domain)
272 assert logic.is_indvar(var),\
273 "Wrong format for an Individual Variable: '%s'" % var
274 self.update(assignment)
275 self._addvariant()
276
282
287
288 - def purge(self, var=None):
289 """
290 Remove one or all keys (i.e. logic variables) from an
291 assignment, and update C{self.variant}.
292
293 @param var: a Variable acting as a key for the assignment.
294 """
295 if var:
296 val = self[var]
297 del self[var]
298 else:
299 self.clear()
300 self._addvariant()
301 return None
302
304 """
305 Pretty printing for assignments. {'x', 'u'} appears as 'g[u/x]'
306 """
307 gstring = "g"
308 for (val, var) in self.variant:
309 gstring = gstring + "[" + str(val) + "/" + str(var) + "]"
310 return gstring
311
313 """
314 Create a more pretty-printable version of the assignment.
315 """
316 list = []
317 for item in self.items():
318 pair = (item[1], item[0])
319 list.append(pair)
320 self.variant = list
321 return None
322
323 - def add(self, val, var):
324 """
325 Add a new variable-value pair to the assignment, and update
326 C{self.variant}.
327
328 We write the arguments in the order 'val, var' by analogy with the
329 notation 'g[u/x]'.
330 """
331 assert val in self.domain,\
332 "%s is not in the domain %s" % (val, self.domain)
333 assert logic.is_indvar(var),\
334 "Wrong format for an Individual Variable: '%s'" % var
335 self[var] = val
336 self._addvariant()
337 return self
338
339
341 """
342 A first order model is a domain M{D} of discourse and a valuation M{V}.
343
344 A domain M{D} is a set, and a valuation M{V} is a map that associates
345 expressions with values in the model.
346 The domain of M{V} should be a subset of M{D}.
347
348
349 """
350
351 - def __init__(self, domain, valuation, prop=None):
352 """
353 Construct a new L{Model}.
354
355 @type domain: C{set}
356 @param domain: A set of entities representing the domain of discourse of the model.
357 @type valuation: L{Valuation}
358 @param valuation: the valuation of the model.
359 @param prop: If this is set, then we are building a propositional\
360 model and don't require the domain of M{V} to be subset of M{D}.
361 """
362 assert isinstance(domain, set)
363 self.domain = domain
364 self.valuation = valuation
365 if prop is None:
366 if not domain.issuperset(valuation.domain):
367 raise Error,\
368 "The valuation domain, %s, must be a subset of the model's domain, %s"\
369 % (valuation.domain, domain)
370
371
373 return "(%r, %r)" % (self.domain, self.valuation)
374
376 return "Domain = %s,\nValuation = \n%s" % (self.domain, self.valuation)
377
378 - def app(self, fun, arg):
379 """
380 Wrapper for handling KeyErrors and TypeErrors raised by
381 function application.
382
383 This constrains instances of L{CharFun} to return C{False} in
384 the right circumstances.
385
386 @param fun: an instance of L{CharFun}.
387 @param arg: an arbitrary semantic object
388 @return: If C{arg} is in C{fun}'s domain, then returns C{fun[arg]},\
389 else if C{arg} is in C{self.domain}, returns C{False},\
390 else raises C{Undefined} error.
391 """
392
393 try:
394 return fun[arg]
395 except KeyError:
396 if arg in self.domain:
397 return False
398 else:
399 raise Undefined,\
400 "%s can't be applied as a function to '%s'" % (fun, arg)
401 except TypeError:
402 if fun == False:
403 return False
404 else:
405 raise Undefined,\
406 "%s can't be applied as a function to %s" % (fun, arg)
407
408
409
410 NOT = {True: False, False: True}
411 AND = {True: {True: True, False: False},
412 False: {True: False, False: False}}
413 OR = {True: {True: True, False: True},
414 False: {True: True, False: False}}
415 IMPLIES = {True: {True: True, False: False},
416 False: {True: True, False: True}}
417 IFF = {True: {True: True, False: False},
418 False: {True: False, False: True}}
419
420 OPS = {'and': AND,
421 'or': OR,
422 'implies': IMPLIES,
423 'iff': IFF}
424
425 - def evaluate(self, expr, g, trace=None):
426 """
427 Provides a handler for L{satisfy}
428 that blocks further propagation of C{Undefined} error.
429 @param expr: An C{Expression} of L{logic}.
430 @type g: L{Assignment}
431 @param g: an assignment to individual variables.
432 @rtype: C{bool} or 'Undefined'
433 """
434 try:
435 value = self.satisfy(expr, g, trace=trace)
436 if trace:
437 print "'%s' evaluates to %s under M, %s" % (expr, value, g)
438 return value
439 except Undefined:
440 return 'Undefined'
441
442
443
444 - def satisfy(self, expr, g, trace=None):
445 """
446 Recursive interpretation function for a formula of first-order logic.
447
448 Raises an C{Undefined} error when C{expr} is an atomic string
449 but is not a symbol or an individual variable.
450
451 @return: Returns a truth value or C{Undefined} if C{expr} is\
452 complex, and calls the interpretation function C{i} if C{expr}\
453 is atomic.
454
455 @param expr: An expression of L{logic}.
456 @type g: L{Assignment}
457 @param g: an assignment to individual variables.
458 """
459
460 OPS = Model.OPS
461
462
463
464
465
466
467
468 try:
469 parsed = self.decompose(expr)
470
471 if isinstance(parsed, str):
472 return self.i(expr, g, trace)
473
474 else:
475 first, second = parsed
476
477 phi = second[0]
478 try:
479 psi = second[1]
480
481 except IndexError:
482 pass
483
484 if first == 'not':
485 if trace:
486 print " '%s' evaluates to %s under M, %s." % (phi, self.satisfy(phi, g), g)
487 return not self.satisfy(phi, g, trace)
488
489 elif first in OPS:
490 value = OPS[first][self.satisfy(phi, g, trace)][self.satisfy(psi, g, trace)]
491 if trace:
492 print " '%s' evaluates to %s under M, %s" % (phi, self.satisfy(phi, g, trace), g)
493 print " '%s' evaluates to %s under M, %s" % (psi, self.satisfy(psi, g, trace), g)
494 return value
495
496 elif first == '=':
497 value = (self.satisfy(phi, g, trace) == self.satisfy(psi, g, trace))
498 if trace:
499 print " '%s' evaluates to %s under M, %s" % (phi, self.satisfy(phi, g, trace), g)
500 print " '%s' evaluates to %s under M, %s" % (psi, self.satisfy(psi, g, trace), g)
501 return value
502
503
504
505 elif first[0] == '\\':
506 var = first[1]
507 phi = second
508 cf = CharFun()
509 for u in self.domain:
510 val = self.satisfy(phi, g.add(u, var), trace)
511 if val:
512 cf[u] = val
513
514 if trace:
515 print " '%s' evaluates to %s under M, %s" % (expr, cf, g)
516 return cf
517
518
519 elif first[0] == 'some':
520 var = first[1]
521 phi = second
522
523 seq = self.satisfiers(phi, var, g, trace, nesting=1)
524
525 value = self.any(seq)
526 if trace:
527 if value:
528 print " '%s' evaluates to %s under M, %s" % (phi, value, g)
529 if trace > 1:
530 print " satisfiers of %s under %s are %s" % (phi, g, sat)
531 else:
532 print " '%s' evaluates to %s under M, %s" % (phi, value, g)
533 if trace > 1:
534 print " satisfiers of %s under %s are %s" % (phi, g, sat)
535 return value
536
537 elif first[0] == 'all':
538 var = first[1]
539 phi = second
540 sat = self.satisfiers(phi, var, g, trace, nesting=1)
541
542 value = self.domain.issubset(sat)
543 if trace:
544 if value:
545 print " '%s' evaluates to %s under M, %s" % (phi, self.satisfy(phi, g, trace), g)
546 else:
547 notphi = '(not %s)' % phi
548 witness = self.satisfiers(notphi, var, g).pop()
549 g.add(witness, var)
550 print " '%s' evaluates to %s under M, %s" % (phi, self.satisfy(phi, g, trace), g)
551
552 return value
553
554
555 else:
556 try:
557 funval = self.satisfy(first, g, trace)
558 argval = self.satisfy(second, g, trace)
559 app = self.app(funval, argval)
560 if trace > 1:
561 print "'%s': %s applied to %s yields %s"\
562 % (expr, funval, argval, app)
563 return app
564
565 except TypeError:
566 print "The interpretation of %s cannot be applied to the interpretation of %s"\
567 % (first, second)
568 print "'%s': %s applied to %s yields %s"\
569 % (expr, funval, argval, app)
570 raise
571
572 except ValueError:
573 raise Undefined, "Cannot parse %s", expr
574
575
576
577 - def i(self, expr, g, trace=False):
578 """
579 An interpretation function.
580
581 Assuming that C{expr} is atomic:
582
583 - if C{expr} is a non-logical constant, calls the valuation M{V}
584 - else if C{expr} is an individual variable, calls assignment M{g}
585 - else returns C{Undefined}.
586
587
588 @param expr: an C{Expression} of L{logic}.
589 @type g: L{Assignment}
590 @param g: an assignment to individual variables.
591 @return: a semantic value
592 """
593 try:
594 if trace > 1:
595 print " i, %s('%s') = %s" % (g, expr, self.valuation[expr])
596
597 return self.valuation[expr]
598 except Undefined:
599 if trace > 1:
600 print " (checking whether '%s' is an individual variable)" % expr
601
602
603 return g[expr]
604
605
606
608 """
609 Is C{var} one of the free variables in C{expr}?
610
611 @type var: an C{Indvar} of L{logic}
612 @param var: the variable to test for.
613 @param expr: an C{Expression} of L{logic}.
614 @rtype: C{bool}
615 """
616 parsed = logic.Parser().parse(expr)
617 variable = logic.Variable(var)
618 return variable in parsed.free()
619
620 - def satisfiers(self, expr, var, g, trace=False, nesting=0):
621 """
622 Generate the entities from the model's domain that satisfy an open formula.
623
624 @param expr: the open formula
625 @param var: the relevant free variable in C{expr}.
626 @param g: the variable assignment
627 @return: an iterator over the entities that satisfy C{expr}.
628 """
629
630 spacer = ' '
631 indent = spacer + (spacer * nesting)
632 candidates = []
633
634 if self.freevar(var, expr):
635 if trace:
636 print
637 print (spacer * nesting) + "Open formula is '%s' with assignment %s" % (expr, g)
638 for u in self.domain:
639 new_g = g.copy()
640 new_g.add(u, var)
641 if trace > 1:
642 lowtrace = trace-1
643 else:
644 lowtrace = 0
645 value = self.satisfy(expr, new_g, lowtrace)
646
647 if trace:
648 print indent + "(trying assignment %s)" % new_g
649
650
651 if value == False:
652 if trace:
653 print indent + "value of '%s' under %s is False" % (expr, new_g)
654
655
656
657 else:
658 candidates.append(u)
659 if trace:
660 print indent + "value of '%s' under %s is %s" % (expr, new_g, value)
661
662 result = (c for c in candidates)
663
664 else:
665 raise Undefined, "%s is not free in %s" % (var, expr)
666
667 return result
668
669
671 """
672 Function to communicate with a first-order functional language.
673
674 This function tries to make weak assumptions about the parse structure
675 provided by the logic module. It makes the assumption that an expression
676 can be broken down into a pair of subexpressions:
677
678 - The C{(binder, body)} pair is for decomposing quantified formulae.
679 - The C{(op, args)} pair is for decomposing formulae with a boolean operator.
680 - The C{(fun, args)} pair should catch other relevant cases.
681
682 @param expr: A string representation of a first-order formula.
683 """
684
685 try:
686 parsed = logic.Parser(constants=self.valuation.symbols).parse(expr)
687 except TypeError:
688 print "Cannot parse %s" % expr
689
690 try:
691 first, second = parsed.binder, parsed.body
692
693 return (first, second)
694 except AttributeError:
695 pass
696 try:
697 first, second = parsed.op, parsed.args
698
699 return (first, second)
700 except AttributeError:
701 pass
702 try:
703 first, second = str(parsed.first), str(parsed.second)
704
705 return (first, second)
706 except (AttributeError, TypeError):
707 return expr
708
709 - def any(self, seq):
710 """
711 Returns True if there is at least one element in the iterable.
712
713 @param seq: an iterator
714 @rtype: C{bool}
715 """
716 for elem in seq:
717 return True
718 return False
719
720
721
722
723
724
725
726 mult = 30
727
729 """Example of a propositional model."""
730
731 global val1, dom1, m1, g1
732 val1 = Valuation({'p': True, 'q': True, 'r': False})
733 dom1 = set([])
734 m1 = Model(dom1, val1, prop=True)
735 g1 = Assignment(dom1)
736
737 print
738 print '*' * mult
739 print "Propositional Formulas Demo"
740 print '*' * mult
741 print "Model m1:\n", m1
742 print '*' * mult
743
744 sentences = [
745 '(p and q)',
746 '(p and r)',
747 '(not p)',
748 '(not r)',
749 '(not (not p))',
750 '(not (p and r))',
751 '(p or r)',
752 '(r or p)',
753 '(r or r)',
754 '((not p) or r))',
755 '(p or (not p))',
756 '(p implies q)',
757 '(p implies r)',
758 '(r implies p)',
759 '(p iff p)',
760 '(r iff r)',
761 '(p iff r)',
762 ]
763
764 for sent in sentences:
765 if trace:
766 print
767 m1.evaluate(sent, g1, trace)
768 else:
769 print "The value of '%s' is: %s" % (sent, m1.evaluate(sent, g1))
770
772 """Example of a first-order model."""
773
774 global val2, v2, dom2, m2, g2
775 val2 = Valuation()
776 v2 = [('adam', 'b1'), ('betty', 'g1'), ('fido', 'd1'),\
777 ('girl', set(['g1', 'g2'])), ('boy', set(['b1', 'b2'])), ('dog', set(['d1'])),
778 ('love', set([('b1', 'g1'), ('b2', 'g2'), ('g1', 'b1'), ('g2', 'b1')]))]
779 val2.read(v2)
780 dom2 = val2.domain
781 m2 = Model(dom2, val2)
782 g2 = Assignment(dom2, {'x': 'b1', 'y': 'g2'})
783
784 if trace:
785 print "*" * mult
786 print "Model m2\n", m2
787 print "*" * mult
788
789 symbols = ['adam', 'girl', 'love', 'walks', 'x', 'y', 'z']
790
791 if trace:
792 for s in symbols:
793 try:
794 print "The interpretation of '%s' in m2 is %s" % (s, m2.i(s, g2))
795 except Undefined:
796 print "The interpretation of '%s' in m2 is Undefined" % s
797
799 """Interpretation of closed expressions in a first-order model."""
800 folmodel()
801
802 print
803 print '*' * mult
804 print "FOL Formulas Demo"
805 print '*' * mult
806
807 formulas = [
808 '(love adam betty)',
809 '(adam = mia)',
810 '\\x. ((boy x) or (girl x))',
811 '\\x y. ((boy x) and (love y x))',
812 '\\x. some y. ((boy x) and (love y x))',
813 'some z1. (boy z1)',
814 'some x. ((boy x) and (not (x = adam)))',
815 'some x. ((boy x) and all y. (love x y))',
816 'all x. ((boy x) or (girl x))',
817 'all x. ((girl x) implies some y. (boy y) and (love y x))',
818 'some x. ((boy x) and all y. ((girl y) implies (love x y)))',
819 'some x. ((boy x) and all y. ((girl y) implies (love y x)))',
820 'all x. ((dog x) implies (not (girl x)))',
821 'some x. some y. ((love y x) and (love y x))'
822 ]
823
824
825 for fmla in formulas:
826 g2.purge()
827 if trace:
828 print
829 m2.evaluate(fmla, g2, trace)
830 else:
831 print "The value of '%s' is: %s" % (fmla, m2.evaluate(fmla, g2))
832
833
835 """Satisfiers of an open formula in a first order model."""
836
837 print
838 print '*' * mult
839 print "Satisfiers Demo"
840 print '*' * mult
841
842 folmodel()
843
844 formulas = [
845 '(boy x)',
846 '(x = x)',
847 '((boy x) or (girl x))',
848 '((boy x) and (girl x))',
849 '(love x adam)',
850 '(love adam x)',
851 '(not (x = adam))',
852 'some z22. (love z22 x)',
853 'some y. (love x y)',
854 'all y. ((girl y) implies (love y x))',
855 'all y. ((girl y) implies (love x y))',
856 'all y. ((girl y) implies ((boy x) and (love x y)))',
857 '((boy x) and all y. ((girl y) implies (love y x)))',
858 '((boy x) and all y. ((girl y) implies (love x y)))',
859 '((boy x) and some y. ((girl y) and (love x y)))',
860 '((girl x) implies (dog x))',
861 'all y. ((dog y) implies (x = y))',
862 '(not some y. (love x y))',
863 'some y. ((love y adam) and (love x y))'
864 ]
865
866 if trace:
867 print m2
868
869 for fmla in formulas:
870 g2.purge()
871 print "The satisfiers of '%s' are: %s" % (fmla, list(m2.satisfiers(fmla, 'x', g2, trace)))
872
873
874 -def demo(num, trace=None):
875 """
876 Run some demos.
877
878 - num = 1: propositional logic demo
879 - num = 2: first order model demo (only if trace is set)
880 - num = 3: first order sentences demo
881 - num = 4: satisfaction of open formulas demo
882 - any other value: run all the demos
883
884 @param trace: trace = 1, or trace = 2 for more verbose tracing
885 """
886 demos = {1: propdemo,
887 2: folmodel,
888 3: foldemo,
889 4: satdemo}
890
891
892 try:
893 demos[num](trace=trace)
894 except KeyError:
895 for num in demos.keys():
896 demos[num](trace=trace)
897
898
899
900 if __name__ == "__main__":
901 demo(5, trace=0)
902