Package nltk_lite :: Package contrib :: Package mit :: Package six863 :: Package semantics :: Module logic
[hide private]
[frames] | no frames]

Source Code for Module nltk_lite.contrib.mit.six863.semantics.logic

  1  # Natural Language Toolkit: Logic 
  2  from nltk_lite.utilities import Counter 
  3  from featurelite import SubstituteBindingsMixin, FeatureI 
  4  from featurelite import Variable as FeatureVariable 
  5  _counter = Counter() 
  6   
7 -def unique_variable(counter=None):
8 if counter is None: counter = _counter 9 unique = counter.get() 10 return VariableExpression(Variable('x'+str(unique)))
11
12 -class Error(Exception): pass
13
14 -class Variable(object):
15 """A variable, either free or bound.""" 16
17 - def __init__(self, name):
18 """ 19 Create a new C{Variable}. 20 21 @type name: C{string} 22 @param name: The name of the variable. 23 """ 24 self.name = name
25
26 - def __eq__(self, other):
27 return self.equals(other)
28
29 - def __ne__(self, other):
30 return not self.equals(other)
31
32 - def equals(self, other):
33 """A comparison function.""" 34 if not isinstance(other, Variable): return False 35 return self.name == other.name
36
37 - def __str__(self): return self.name
38
39 - def __repr__(self): return "Variable('%s')" % self.name
40
41 - def __hash__(self): return hash(repr(self))
42
43 -class Constant:
44 """A nonlogical constant.""" 45
46 - def __init__(self, name):
47 """ 48 Create a new C{Constant}. 49 50 @type name: C{string} 51 @param name: The name of the constant. 52 """ 53 self.name = name
54
55 - def __eq__(self, other):
56 return self.equals(other)
57
58 - def __ne__(self, other):
59 return not self.equals(other)
60
61 - def equals(self, other):
62 """A comparison function.""" 63 assert isinstance(other, Constant) 64 return self.name == other.name
65
66 - def __str__(self): return self.name
67
68 - def __repr__(self): return "Constant('%s')" % self.name
69
70 - def __hash__(self): return hash(repr(self))
71
72 -class Expression(object):
73 """The abstract class of a lambda calculus expression."""
74 - def __init__(self):
75 if self.__class__ is Expression: 76 raise NotImplementedError
77
78 - def __eq__(self, other):
79 return self.equals(other)
80
81 - def __ne__(self, other):
82 return not self.equals(other)
83
84 - def equals(self, other):
85 """Are the two expressions equal, modulo alpha conversion?""" 86 return NotImplementedError
87
88 - def variables(self):
89 """Set of all variables.""" 90 raise NotImplementedError
91
92 - def free(self):
93 """Set of free variables.""" 94 raise NotImplementedError
95
96 - def subterms(self):
97 """Set of all subterms (including self).""" 98 raise NotImplementedError
99 100
101 - def replace(self, variable, expression, replace_bound=False):
102 """Replace all instances of variable v with expression E in self, 103 where v is free in self.""" 104 raise NotImplementedError
105
106 - def replace_unique(self, variable, counter=None, replace_bound=False):
107 """ 108 Replace a variable v with a new, uniquely-named variable. 109 """ 110 return self.replace(variable, unique_variable(counter), 111 replace_bound)
112
113 - def simplify(self):
114 """Evaluate the form by repeatedly applying applications.""" 115 raise NotImplementedError
116
117 - def skolemise(self):
118 """ 119 Perform a simple Skolemisation operation. Existential quantifiers are 120 simply dropped and all variables they introduce are renamed so that 121 they are unique. 122 """ 123 return self._skolemise(set(), Counter())
124 125 skolemize = skolemise 126
127 - def _skolemise(self, bound_vars, counter):
128 raise NotImplementedError
129
130 - def clauses(self):
131 return [self]
132
133 - def __str__(self):
134 raise NotImplementedError
135
136 - def __repr__(self):
137 raise NotImplementedError
138
139 - def __hash__(self):
140 raise NotImplementedError, self.__class__
141
142 - def normalize(self):
143 if hasattr(self, '_normalized'): return self._normalized 144 result = self 145 vars = self.variables() 146 counter = 0 147 for var in vars: 148 counter += 1 149 result = result.replace(var, Variable(str(counter)), replace_bound=True) 150 self._normalized = result 151 return result
152
153 -class VariableExpression(Expression):
154 """A variable expression which consists solely of a variable."""
155 - def __init__(self, variable):
156 Expression.__init__(self) 157 assert isinstance(variable, Variable) 158 self.variable = variable
159
160 - def equals(self, other):
161 """ 162 Allow equality between instances of C{VariableExpression} and 163 C{IndVariableExpression}. 164 """ 165 if isinstance(self, VariableExpression) and \ 166 isinstance(other, VariableExpression): 167 return self.variable.equals(other.variable) 168 else: 169 return False
170
171 - def variables(self):
172 return [self.variable]
173
174 - def free(self):
175 return set([self.variable])
176
177 - def subterms(self):
178 return set([self])
179
180 - def replace(self, variable, expression, replace_bound=False):
181 if self.variable.equals(variable): 182 if isinstance(expression, Variable): 183 return VariableExpression(expression) 184 else: 185 return expression 186 else: 187 return self
188
189 - def simplify(self):
190 return self
191
192 - def infixify(self):
193 return self
194
195 - def name(self):
196 return self.__str__()
197
198 - def _skolemise(self, bound_vars, counter):
199 return self
200
201 - def __str__(self): return '%s' % self.variable
202
203 - def __repr__(self): return "VariableExpression('%s')" % self.variable
204
205 - def __hash__(self): return hash(repr(self))
206 207
208 -def is_indvar(expr):
209 """ 210 Check whether an expression has the form of an individual variable. 211 212 An individual variable matches the following regex: 213 C{'^[wxyz](\d*)'}. 214 215 @rtype: Boolean 216 @param expr: String 217 """ 218 result = expr[0] in ['w', 'x', 'y', 'z'] 219 if len(expr) > 1: 220 return result and expr[1:].isdigit() 221 else: 222 return result
223
224 -class IndVariableExpression(VariableExpression):
225 """ 226 An individual variable expression, as determined by C{is_indvar()}. 227 """
228 - def __init__(self, variable):
229 Expression.__init__(self) 230 assert isinstance(variable, Variable), "Not a Variable: %s" % variable 231 assert is_indvar(str(variable)), "Wrong format for an Individual Variable: %s" % variable 232 self.variable = variable
233
234 - def __repr__(self): return "IndVariableExpression('%s')" % self.variable
235 236
237 -class ConstantExpression(Expression):
238 """A constant expression, consisting solely of a constant."""
239 - def __init__(self, constant):
240 Expression.__init__(self) 241 assert isinstance(constant, Constant) 242 self.constant = constant
243
244 - def equals(self, other):
245 if self.__class__ == other.__class__: 246 return self.constant.equals(other.constant) 247 else: 248 return False
249
250 - def variables(self):
251 return []
252
253 - def free(self):
254 return set()
255
256 - def subterms(self):
257 return set([self])
258
259 - def replace(self, variable, expression, replace_bound=False):
260 return self
261
262 - def simplify(self):
263 return self
264
265 - def infixify(self):
266 return self
267
268 - def name(self):
269 return self.__str__()
270
271 - def _skolemise(self, bound_vars, counter):
272 return self
273
274 - def __str__(self): return '%s' % self.constant
275
276 - def __repr__(self): return "ConstantExpression('%s')" % self.constant
277
278 - def __hash__(self): return hash(repr(self))
279 280
281 -class Operator(ConstantExpression):
282 """ 283 A boolean operator, such as 'not' or 'and', or the equality 284 relation ('='). 285 """
286 - def __init__(self, operator):
287 Expression.__init__(self) 288 assert operator in Parser.OPS 289 self.constant = operator 290 self.operator = operator
291
292 - def equals(self, other):
293 if self.__class__ == other.__class__: 294 return self.constant == other.constant 295 else: 296 return False
297
298 - def simplify(self):
299 return self
300
301 - def __str__(self): return '%s' % self.operator
302
303 - def __repr__(self): return "Operator('%s')" % self.operator
304 305 306
307 -class VariableBinderExpression(Expression):
308 """A variable binding expression: e.g. \\x.M.""" 309 310 # for generating "unique" variable names during alpha conversion. 311 _counter = Counter() 312
313 - def __init__(self, variable, term):
314 Expression.__init__(self) 315 assert isinstance(variable, Variable) 316 assert isinstance(term, Expression) 317 self.variable = variable 318 self.term = term 319 self.prefix = self.__class__.PREFIX.rstrip() 320 self.binder = (self.prefix, self.variable.name) 321 self.body = str(self.term)
322
323 - def equals(self, other):
324 r""" 325 Defines equality modulo alphabetic variance. 326 327 If we are comparing \x.M and \y.N, then 328 check equality of M and N[x/y]. 329 """ 330 if self.__class__ == other.__class__: 331 if self.variable == other.variable: 332 return self.term == other.term 333 else: 334 # Comparing \x.M and \y.N. 335 # Relabel y in N with x and continue. 336 relabeled = self._relabel(other) 337 return self.term == relabeled 338 else: 339 return False
340
341 - def _relabel(self, other):
342 """ 343 Relabel C{other}'s bound variables to be the same as C{self}'s 344 variable. 345 """ 346 var = VariableExpression(self.variable) 347 return other.term.replace(other.variable, var)
348
349 - def variables(self):
350 vars = [self.variable] 351 for var in self.term.variables(): 352 if var not in vars: vars.append(var) 353 return vars
354
355 - def free(self):
356 return self.term.free().difference(set([self.variable]))
357
358 - def subterms(self):
359 return self.term.subterms().union([self])
360
361 - def replace(self, variable, expression, replace_bound=False):
362 if self.variable == variable: 363 if not replace_bound: return self 364 else: return self.__class__(expression, 365 self.term.replace(variable, expression, True)) 366 if replace_bound or self.variable in expression.free(): 367 v = 'z' + str(self._counter.get()) 368 if not replace_bound: self = self.alpha_convert(Variable(v)) 369 return self.__class__(self.variable, 370 self.term.replace(variable, expression, replace_bound))
371
372 - def alpha_convert(self, newvar):
373 """ 374 Rename all occurrences of the variable introduced by this variable 375 binder in the expression to @C{newvar}. 376 """ 377 term = self.term.replace(self.variable, VariableExpression(newvar)) 378 return self.__class__(newvar, term)
379
380 - def simplify(self):
381 return self.__class__(self.variable, self.term.simplify())
382
383 - def infixify(self):
384 return self.__class__(self.variable, self.term.infixify())
385
386 - def __str__(self, continuation=0):
387 # Print \x.\y.M as \x y.M. 388 if continuation: 389 prefix = ' ' 390 else: 391 prefix = self.__class__.PREFIX 392 if self.term.__class__ == self.__class__: 393 return '%s%s%s' % (prefix, self.variable, self.term.__str__(1)) 394 else: 395 return '%s%s.%s' % (prefix, self.variable, self.term)
396
397 - def __hash__(self):
398 return hash(str(self.normalize()))
399
400 -class LambdaExpression(VariableBinderExpression):
401 """A lambda expression: \\x.M.""" 402 PREFIX = '\\' 403
404 - def _skolemise(self, bound_vars, counter):
405 bv = bound_vars.copy() 406 bv.add(self.variable) 407 return self.__class__(self.variable, self.term._skolemise(bv, counter))
408
409 - def __repr__(self):
410 return str(self)
411 #return "LambdaExpression('%s', '%s')" % (self.variable, self.term) 412
413 -class SomeExpression(VariableBinderExpression):
414 """An existential quantification expression: some x.M.""" 415 PREFIX = 'some ' 416
417 - def _skolemise(self, bound_vars, counter):
418 if self.variable in bound_vars: 419 var = Variable("_s" + str(counter.get())) 420 term = self.term.replace(self.variable, VariableExpression(var)) 421 else: 422 var = self.variable 423 term = self.term 424 bound_vars.add(var) 425 return term._skolemise(bound_vars, counter)
426
427 - def __repr__(self):
428 return str(self)
429 #return "SomeExpression('%s', '%s')" % (self.variable, self.term) 430 431
432 -class AllExpression(VariableBinderExpression):
433 """A universal quantification expression: all x.M.""" 434 PREFIX = 'all ' 435
436 - def _skolemise(self, bound_vars, counter):
437 bv = bound_vars.copy() 438 bv.add(self.variable) 439 return self.__class__(self.variable, self.term._skolemise(bv, counter))
440
441 - def __repr__(self):
442 return str(self)
443 #return "AllExpression('%s', '%s')" % (self.variable, self.term) 444 445 446
447 -class ApplicationExpression(Expression):
448 """An application expression: (M N)."""
449 - def __init__(self, first, second):
450 Expression.__init__(self) 451 assert isinstance(first, Expression) 452 assert isinstance(second, Expression) 453 self.first = first 454 self.second = second
455
456 - def equals(self, other):
457 if self.__class__ == other.__class__: 458 return self.first.equals(other.first) and \ 459 self.second.equals(other.second) 460 else: 461 return False
462
463 - def variables(self):
464 vars = self.first.variables() 465 for var in self.second.variables(): 466 if var not in vars: vars.append(var) 467 return vars
468
469 - def free(self):
470 return self.first.free().union(self.second.free())
471
472 - def _functor(self):
473 if isinstance(self.first, ApplicationExpression): 474 return self.first._functor() 475 else: 476 return self.first
477 478 fun = property(_functor, 479 doc="Every ApplicationExpression has a functor.") 480 481
482 - def _operator(self):
483 functor = self._functor() 484 if isinstance(functor, Operator): 485 return str(functor) 486 else: 487 raise AttributeError
488 489 op = property(_operator, 490 doc="Only some ApplicationExpressions have operators." ) 491
492 - def _arglist(self):
493 """Uncurry the argument list.""" 494 arglist = [str(self.second)] 495 if isinstance(self.first, ApplicationExpression): 496 arglist.extend(self.first._arglist()) 497 return arglist
498
499 - def _args(self):
500 arglist = self._arglist() 501 arglist.reverse() 502 return arglist
503 504 args = property(_args, 505 doc="Every ApplicationExpression has args.") 506
507 - def subterms(self):
508 first = self.first.subterms() 509 510 second = self.second.subterms() 511 return first.union(second).union(set([self]))
512
513 - def replace(self, variable, expression, replace_bound=False):
514 return self.__class__( 515 self.first.replace(variable, expression, replace_bound), 516 self.second.replace(variable, expression, replace_bound))
517
518 - def simplify(self):
519 first = self.first.simplify() 520 second = self.second.simplify() 521 if isinstance(first, LambdaExpression): 522 variable = first.variable 523 term = first.term 524 return term.replace(variable, second).simplify() 525 else: 526 return self.__class__(first, second)
527
528 - def infixify(self):
529 first = self.first.infixify() 530 second = self.second.infixify() 531 if isinstance(first, Operator) and not str(first) == 'not': 532 return self.__class__(second, first) 533 else: 534 return self.__class__(first, second)
535
536 - def _skolemise(self, bound_vars, counter):
537 first = self.first._skolemise(bound_vars, counter) 538 second = self.second._skolemise(bound_vars, counter) 539 return self.__class__(first, second)
540
541 - def clauses(self):
542 if isinstance(self.first, ApplicationExpression) and\ 543 isinstance(self.first.first, Operator) and\ 544 self.first.first.operator == 'and': 545 return self.first.second.clauses() + self.second.clauses() 546 else: return [self]
547 - def __str__(self):
548 # Print ((M N) P) as (M N P). 549 strFirst = str(self.first) 550 if isinstance(self.first, ApplicationExpression): 551 if not isinstance(self.second, Operator): 552 strFirst = strFirst[1:-1] 553 return '(%s %s)' % (strFirst, self.second)
554
555 - def __repr__(self):
556 return str(self)
557 #return "ApplicationExpression('%s', '%s')" % (self.first, self.second) 558
559 - def __hash__(self):
560 return hash(str(self.normalize()))
561
562 -class ApplicationExpressionSubst(ApplicationExpression, SubstituteBindingsMixin):
563 pass
564
565 -class LambdaExpressionSubst(LambdaExpression, SubstituteBindingsMixin):
566 pass
567
568 -class SomeExpressionSubst(SomeExpression, SubstituteBindingsMixin):
569 pass
570
571 -class AllExpressionSubst(AllExpression, SubstituteBindingsMixin):
572 pass
573
574 -class Parser:
575 """A lambda calculus expression parser.""" 576 577 578 # Tokens. 579 LAMBDA = '\\' 580 SOME = 'some' 581 ALL = 'all' 582 DOT = '.' 583 OPEN = '(' 584 CLOSE = ')' 585 BOOL = ['and', 'or', 'not', 'implies', 'iff'] 586 EQ = '=' 587 OPS = BOOL 588 OPS.append(EQ) 589
590 - def __init__(self, data=None, constants=None):
591 if data is not None: 592 self.buffer = data 593 self.process() 594 else: 595 self.buffer = '' 596 if constants is not None: 597 self.constants = constants 598 else: 599 self.constants = []
600 601
602 - def feed(self, data):
603 """Feed another batch of data to the parser.""" 604 self.buffer += data 605 self.process()
606
607 - def parse(self, data):
608 """ 609 Provides a method similar to other NLTK parsers. 610 611 @type data: str 612 @returns: a parsed Expression 613 """ 614 self.feed(data) 615 result = self.next() 616 return result
617
618 - def process(self):
619 """Process the waiting stream to make it trivial to parse.""" 620 self.buffer = self.buffer.replace('\t', ' ') 621 self.buffer = self.buffer.replace('\n', ' ') 622 self.buffer = self.buffer.replace('\\', ' \\ ') 623 self.buffer = self.buffer.replace('.', ' . ') 624 self.buffer = self.buffer.replace('(', ' ( ') 625 self.buffer = self.buffer.replace(')', ' ) ')
626
627 - def token(self, destructive=1):
628 """Get the next waiting token. The destructive flag indicates 629 whether the token will be removed from the buffer; setting it to 630 0 gives lookahead capability.""" 631 if self.buffer == '': 632 raise Error, "end of stream" 633 tok = None 634 buffer = self.buffer 635 while not tok: 636 seq = buffer.split(' ', 1) 637 if len(seq) == 1: 638 tok, buffer = seq[0], '' 639 else: 640 assert len(seq) == 2 641 tok, buffer = seq 642 if tok: 643 if destructive: 644 self.buffer = buffer 645 return tok 646 assert 0 # control never gets here 647 return None
648
649 - def isVariable(self, token):
650 """Is this token a variable (that is, not one of the other types)?""" 651 TOKENS = [Parser.LAMBDA, Parser.SOME, Parser.ALL, 652 Parser.DOT, Parser.OPEN, Parser.CLOSE, Parser.EQ] 653 TOKENS.extend(self.constants) 654 TOKENS.extend(Parser.BOOL) 655 return token not in TOKENS
656
657 - def next(self):
658 """Parse the next complete expression from the stream and return it.""" 659 tok = self.token() 660 661 if tok in [Parser.LAMBDA, Parser.SOME, Parser.ALL]: 662 # Expression is a lambda expression: \x.M 663 # or a some expression: some x.M 664 if tok == Parser.LAMBDA: 665 factory = self.make_LambdaExpression 666 elif tok == Parser.SOME: 667 factory = self.make_SomeExpression 668 elif tok == Parser.ALL: 669 factory = self.make_AllExpression 670 else: 671 raise ValueError(tok) 672 673 vars = [self.token()] 674 while self.isVariable(self.token(0)): 675 # Support expressions like: \x y.M == \x.\y.M 676 # and: some x y.M == some x.some y.M 677 vars.append(self.token()) 678 tok = self.token() 679 680 if tok != Parser.DOT: 681 raise Error, "parse error, unexpected token: %s" % tok 682 term = self.next() 683 accum = factory(Variable(vars.pop()), term) 684 while vars: 685 accum = factory(Variable(vars.pop()), accum) 686 return accum 687 688 elif tok == Parser.OPEN: 689 # Expression is an application expression: (M N) 690 first = self.next() 691 second = self.next() 692 exps = [] 693 while self.token(0) != Parser.CLOSE: 694 # Support expressions like: (M N P) == ((M N) P) 695 exps.append(self.next()) 696 tok = self.token() # swallow the close token 697 assert tok == Parser.CLOSE 698 if isinstance(second, Operator): 699 accum = self.make_ApplicationExpression(second, first) 700 else: 701 accum = self.make_ApplicationExpression(first, second) 702 while exps: 703 exp, exps = exps[0], exps[1:] 704 accum = self.make_ApplicationExpression(accum, exp) 705 return accum 706 707 elif tok in self.constants: 708 # Expression is a simple constant expression: a 709 return ConstantExpression(Constant(tok)) 710 711 elif tok in Parser.OPS: 712 # Expression is a boolean operator or the equality symbol 713 return Operator(tok) 714 715 elif is_indvar(tok): 716 # Expression is a boolean operator or the equality symbol 717 return IndVariableExpression(Variable(tok)) 718 719 else: 720 if self.isVariable(tok): 721 # Expression is a simple variable expression: x 722 return VariableExpression(Variable(tok)) 723 else: 724 raise Error, "parse error, unexpected token: %s" % tok
725 726 # This is intended to be overridden, so that you can derive a Parser class 727 # that constructs expressions using your subclasses. So far we only need 728 # to overridde ApplicationExpression, but the same thing could be done for 729 # other expression types.
730 - def make_ApplicationExpression(self, first, second):
731 return ApplicationExpression(first, second)
732 - def make_LambdaExpression(self, first, second):
733 return LambdaExpression(first, second)
734 - def make_SomeExpression(self, first, second):
735 return SomeExpression(first, second)
736 - def make_AllExpression(self, first, second):
737 return AllExpression(first, second)
738
739 -def expressions():
740 """Return a sequence of test expressions.""" 741 a = Variable('a') 742 x = Variable('x') 743 y = Variable('y') 744 z = Variable('z') 745 A = VariableExpression(a) 746 X = IndVariableExpression(x) 747 Y = IndVariableExpression(y) 748 Z = IndVariableExpression(z) 749 XA = ApplicationExpression(X, A) 750 XY = ApplicationExpression(X, Y) 751 XZ = ApplicationExpression(X, Z) 752 YZ = ApplicationExpression(Y, Z) 753 XYZ = ApplicationExpression(XY, Z) 754 I = LambdaExpression(x, X) 755 K = LambdaExpression(x, LambdaExpression(y, X)) 756 L = LambdaExpression(x, XY) 757 S = LambdaExpression(x, LambdaExpression(y, LambdaExpression(z, \ 758 ApplicationExpression(XZ, YZ)))) 759 B = LambdaExpression(x, LambdaExpression(y, LambdaExpression(z, \ 760 ApplicationExpression(X, YZ)))) 761 C = LambdaExpression(x, LambdaExpression(y, LambdaExpression(z, \ 762 ApplicationExpression(XZ, Y)))) 763 O = LambdaExpression(x, LambdaExpression(y, XY)) 764 N = ApplicationExpression(LambdaExpression(x, XA), I) 765 T = Parser('\\x y.(x y z)').next() 766 return [X, XZ, XYZ, I, K, L, S, B, C, O, N, T]
767
768 -def demo():
769 p = Variable('p') 770 q = Variable('q') 771 P = VariableExpression(p) 772 Q = VariableExpression(q) 773 for l in expressions(): 774 print "Expression:", l 775 print "Variables:", l.variables() 776 print "Free:", l.free() 777 print "Subterms:", l.subterms() 778 print "Simplify:",l.simplify() 779 la = ApplicationExpression(ApplicationExpression(l, P), Q) 780 las = la.simplify() 781 print "Apply and simplify: %s -> %s" % (la, las) 782 ll = Parser(str(l)).next() 783 print 'l is:', l 784 print 'll is:', ll 785 assert l.equals(ll) 786 print "Serialize and reparse: %s -> %s" % (l, ll) 787 print "Variables:", ll.variables() 788 print "Normalize: %s" % ll.normalize()
789 790 791 if __name__ == '__main__': 792 demo() 793