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

Source Code for Module nltk_lite.semantics.logic

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