nltk.sem.logic

1 # Natural Language Toolkit: Logic 2 # 3 # Author: Daniel H. Garrette <[email protected]> 4 # 5 # URL: <http://www.nltk.org> 6 # For license information, see LICENSE.TXT 7 8 """ 9 A version of first order predicate logic, built on 10 top of the untyped lambda calculus. 11 """ 12 13 from nltk.internals import Counter 14 from nltk.tokenize.simple import WhitespaceTokenizer 15 16 _counter = Counter() 17

18 -class Tokens:

19 # Syntaxes 20 OLD_NLTK = 0 21 NEW_NLTK = 1 22 PROVER9 = 2 23 24 25 LAMBDA = ['\\', '\\', '\\'] 26 27 #Quantifiers 28 EXISTS = ['some', 'exists', 'exists'] 29 ALL = ['all', 'all', 'all'] 30 31 #Punctuation 32 DOT = ['.', '.', ' '] 33 OPEN = '(' 34 CLOSE = ')' 35 COMMA = ',' 36 37 #Operations 38 NOT = ['not', '-', '-'] 39 AND = ['and', '&', '&'] 40 OR = ['or', '|', '|'] 41 IMP = ['implies', '->', '->'] 42 IFF = ['iff', '<->', '<->'] 43 EQ = ['=', '=', '='] 44 NEQ = ['!=', '!=', '!='] 45 46 #Collection of tokens 47 BINOPS = AND + OR + IMP + IFF 48 QUANTS = EXISTS + ALL 49 PUNCT = [DOT[0], OPEN, CLOSE, COMMA] 50 51 TOKENS = BINOPS + EQ + NEQ + QUANTS + LAMBDA + PUNCT + NOT 52 53 #Special 54 SYMBOLS = LAMBDA + PUNCT + [AND[1], OR[1], NOT[1], IMP[1], IFF[1]] +\ 55 EQ + NEQ

56 57

58 -class Variable(object):

59 - def __init__(self, name):

60 """ 61 @param name: the name of the variable 62 """ 63 self.name = name

64

65 - def __eq__(self, other):

66 return self.__class__ == other.__class__ and self.name == other.name

67

68 - def __cmp__(self, other):

69 assert isinstance(other, Variable) 70 if self.name == other.name: 71 return 0 72 elif self.name < other.name: 73 return -1 74 else: 75 return 1

76

77 - def substitute_bindings(self, bindings):

78 return bindings.get(self, self)

79

80 - def __hash__(self):

81 return hash(self.name)

82

83 - def __str__(self):

84 return self.name

85

86 - def __repr__(self):

87 return 'Variable(\'' + self.name + '\')'

88

89 -def unique_variable():

90 return Variable('z' + str(_counter.get()))

91 92

93 -class SubstituteBindingsI(object):

94 """ 95 An interface for classes that can perform substitutions for 96 variables. 97 """

98 - def substitute_bindings(self, bindings):

99 """ 100 @return: The object that is obtained by replacing 101 each variable bound by C{bindings} with its values. 102 Aliases are already resolved. (maybe?) 103 @rtype: (any) 104 """ 105 raise NotImplementedError()

106

107 - def variables(self):

108 """ 109 @return: A list of all variables in this object. 110 """ 111 raise NotImplementedError()

112

113 -class Expression(SubstituteBindingsI):

114 """This is the base abstract object for all logical expressions"""

115 - def __call__(self, other, *additional):

116 accum = self.applyto(other) 117 for a in additional: 118 accum = accum(a) 119 return accum

120

121 - def applyto(self, other):

122 return ApplicationExpression(self, other)

123

124 - def __neg__(self):

125 return NegatedExpression(self)

126

127 - def negate(self):

128 return -self

129

130 - def __and__(self, other):

131 assert isinstance(other, Expression) 132 return AndExpression(self, other)

133

134 - def __or__(self, other):

135 assert isinstance(other, Expression) 136 return OrExpression(self, other)

137

138 - def __gt__(self, other):

139 assert isinstance(other, Expression) 140 return ImpExpression(self, other)

141

142 - def __lt__(self, other):

143 assert isinstance(other, Expression) 144 return IffExpression(self, other)

145

146 - def __eq__(self, other):

147 raise NotImplementedError()

148

149 - def tp_equals(self, other, prover_name='tableau'):

150 """Pass the expression (self <-> other) to the theorem prover. 151 If the prover says it is valid, then the self and other are equal.""" 152 assert isinstance(other, Expression) 153 154 from nltk.inference import inference 155 bicond = IffExpression(self.simplify(), other.simplify()) 156 prover = inference.get_prover(bicond, prover_name=prover_name) 157 return prover.prove()

158

159 - def __hash__(self):

160 return hash(repr(self))

161

162 - def substitute_bindings(self, bindings):

163 expr = self 164 for var in expr.variables(): 165 if var in bindings: 166 val = bindings[var] 167 if isinstance(val, Variable): 168 val = VariableExpression(val) 169 elif not isinstance(val, Expression): 170 raise ValueError('Can not substitute a non-expresion ' 171 'value into an expression: %r' % val) 172 # Substitute bindings in the target value. 173 val = val.substitute_bindings(bindings) 174 # Replace var w/ the target value. 175 expr = expr.replace(var, val) 176 return expr.simplify()

177

178 - def __repr__(self):

179 return '<' + self.__class__.__name__ + ' ' + str(self) + '>'

180

181 - def __str__(self):

182 return self.str()

183

184 - def variables(self):

185 """ 186 Return a set of all the variables that are available to be replaced. 187 This includes free (non-bound) variables as well as predicates. 188 @return: C{set} of C{Variable}s 189 """ 190 raise NotImplementedError()

191

192 - def free(self, indvar_only=True):

193 """ 194 Return a set of all the free (non-bound) variables in self. Variables 195 serving as predicates are no included. 196 @param indvar_only: C{boolean} only return individual variables? 197 @return: C{set} of C{Variable}s 198 """ 199 raise NotImplementedError()

200

201 -class ApplicationExpression(Expression):

202 r""" 203 This class is used to represent two related types of logical expressions. 204 205 The first is a Predicate Expression, such as "P(x,y)". A predicate 206 expression is comprised of a VariableExpression as the predicate and a list 207 of Expressions as the arguments. 208 209 The second is a an application of one expression to another, such as 210 "(\x.dog(x))(fido)". 211 212 The reason Predicate Expressions are treated as Application Expressions is 213 that the VariableExpression predicate of the expression may be replaced with 214 another Expression, such as a LambdaExpression, which would mean that the 215 Predicate should be thought of as being applied to the arguments. 216 217 The LogicParser will always curry arguments in a application expression. 218 So, "\x y.see(x,y)(john,mary)" will be represented internally as 219 "((\x y.(see(x))(y))(john))(mary)". This simplifies the internals since 220 there will always be exactly one argument in an application. 221 222 The str() method will usually print the curried forms of application 223 expressions. The one exception is when the the application expression is 224 really a predicate expression (ie, underlying function is a 225 VariableExpression). This means that the example from above will be 226 returned as "(\x y.see(x,y)(john))(mary)". 227 """

228 - def __init__(self, function, argument):

229 """ 230 @param function: C{Expression}, for the function expression 231 @param argument: C{Expression}, for the argument 232 """ 233 self.function = function 234 self.argument = argument

235

236 - def simplify(self):

237 function = self.function.simplify() 238 argument = self.argument.simplify() 239 if isinstance(function, LambdaExpression): 240 return function.term.replace(function.variable, argument).simplify() 241 else: 242 return self.__class__(function, argument)

243

244 - def replace(self, variable, expression, replace_bound=False):

245 """ 246 Replace every instance of 'variable' with 'expression' 247 @param variable: C{Variable} The variable to replace 248 @param expression: C{Expression} The expression with which to replace it 249 @param replace_bound: C{boolean} Should bound variables be replaced? 250 """ 251 function = self.function.replace(variable, expression, replace_bound) 252 argument = self.argument.replace(variable, expression, replace_bound) 253 return self.__class__(function, argument)

254

255 - def variables(self):

256 """ 257 @see: Expression.variables() 258 """ 259 return self.function.variables() | self.argument.variables()

260

261 - def free(self, indvar_only=True):

262 """ 263 @see: Expression.free() 264 """ 265 if isinstance(self.function, VariableExpression): 266 return self.argument.free(indvar_only) 267 else: 268 return self.function.free(indvar_only) | self.argument.free(indvar_only)

269

270 - def __eq__(self, other):

271 return self.__class__ == other.__class__ and \ 272 self.function == other.function and \ 273 self.argument == other.argument

274

275 - def str(self, syntax=Tokens.NEW_NLTK):

276 # uncurry the arguments and find the base function 277 function, args = self.uncurry() 278 if isinstance(function, VariableExpression): 279 #It's a predicate expression ("P(x,y)"), so uncurry arguments 280 arg_str = ','.join([arg.str(syntax) for arg in args]) 281 else: 282 #Leave arguments curried 283 function = self.function 284 arg_str = self.argument.str(syntax) 285 286 function_str = function.str(syntax) 287 parenthesize_function = False 288 if isinstance(function, LambdaExpression): 289 if isinstance(function.term, ApplicationExpression): 290 if not isinstance(function.term.function, VariableExpression): 291 parenthesize_function = True 292 elif not isinstance(function.term, BooleanExpression): 293 parenthesize_function = True 294 elif isinstance(function, ApplicationExpression): 295 parenthesize_function = True 296 297 if parenthesize_function: 298 function_str = Tokens.OPEN + function_str + Tokens.CLOSE 299 300 return function_str + Tokens.OPEN + arg_str + Tokens.CLOSE

301

302 - def uncurry(self):

303 """ 304 return: A tuple (base-function, arg-list) 305 """ 306 function = self.function 307 args = [self.argument] 308 while isinstance(function, ApplicationExpression): 309 #(\x.\y.sees(x,y)(john))(mary) 310 args.insert(0, function.argument) 311 function = function.function 312 return (function, args)

313

314 -class VariableExpression(Expression):

315 """This class represents a variable to be used as a predicate or entity"""

316 - def __init__(self, variable):

317 """ 318 @param variable: C{Variable}, for the variable 319 """ 320 self.variable = variable

321

322 - def simplify(self):

323 return self

324

325 - def replace(self, variable, expression, replace_bound=False):

326 """ 327 Replace every instance of 'variable' with 'expression' 328 @param variable: C{Variable} The variable to replace 329 @param expression: C{Expression} The expression with which to replace it 330 @param replace_bound: C{boolean} Should bound variables be replaced? 331 """ 332 if self.variable == variable: 333 return expression 334 else: 335 return self

336

337 - def variables(self):

338 """ 339 @see: Expression.variables() 340 """ 341 return set([self.variable])

342

343 - def free(self, indvar_only=True):

344 """ 345 @see: Expression.free() 346 """ 347 if not indvar_only: 348 return set([self.variable]) 349 else: 350 return set()

351

352 - def __eq__(self, other):

353 """Allow equality between instances of C{VariableExpression} and 354 C{IndividualVariableExpression}.""" 355 return isinstance(other, VariableExpression) and \ 356 self.variable == other.variable

357

358 - def str(self, syntax=Tokens.NEW_NLTK):

359 return str(self.variable)

360

361 -class IndividualVariableExpression(VariableExpression):

362 """This class represents variables that take the form of a single lowercase 363 character followed by zero or more digits."""

364 - def free(self, indvar_only=True):

365 """ 366 @see: Expression.free() 367 """ 368 return set([self.variable])

369

370 -class VariableBinderExpression(Expression):

371 """This an abstract class for any Expression that binds a variable in an 372 Expression. This includes LambdaExpressions and Quanitifed Expressions"""

373 - def __init__(self, variable, term):

374 """ 375 @param variable: C{Variable}, for the variable 376 @param term: C{Expression}, for the term 377 """ 378 self.variable = variable 379 self.term = term

380

381 - def simplify(self):

382 return self.__class__(self.variable, self.term.simplify())

383

384 - def replace(self, variable, expression, replace_bound=False):

385 """ 386 Replace every instance of 'variable' with 'expression' 387 @param variable: C{Variable} The variable to replace 388 @param expression: C{Expression} The expression with which to replace it 389 @param replace_bound: C{boolean} Should bound variables be replaced? 390 """ 391 #if the bound variable is the thing being replaced 392 if self.variable == variable: 393 if replace_bound: 394 return self.__class__(expression, 395 self.term.replace(variable, expression, 396 True)) 397 else: 398 return self 399 else: 400 # if the bound variable appears in the expression, then it must 401 # be alpha converted to avoid a conflict 402 if self.variable in expression.free(): 403 self = self.alpha_convert(unique_variable()) 404 405 #replace in the term 406 return self.__class__(self.variable, 407 self.term.replace(variable, expression, 408 replace_bound))

409

410 - def alpha_convert(self, newvar):

411 """Rename all occurrences of the variable introduced by this variable 412 binder in the expression to @C{newvar}. 413 @param newvar: C{Variable}, for the new variable 414 """ 415 return self.__class__(newvar, self.term.replace(self.variable, 416 VariableExpression(newvar), True))

417

418 - def variables(self):

419 """ 420 @see: Expression.variables() 421 """ 422 return self.term.variables() - set([self.variable])

423

424 - def free(self, indvar_only=True):

425 """ 426 @see: Expression.free() 427 """ 428 return self.term.free(indvar_only) - set([self.variable])

429

430 - def __eq__(self, other):

431 r"""Defines equality modulo alphabetic variance. If we are comparing 432 \x.M and \y.N, then check equality of M and N[x/y].""" 433 if self.__class__ == other.__class__: 434 if self.variable == other.variable: 435 return self.term == other.term 436 else: 437 # Comparing \x.M and \y.N. Relabel y in N with x and continue. 438 if is_indvar(self.variable.name): 439 varex = IndividualVariableExpression(self.variable) 440 else: 441 varex = VariableExpression(self.variable) 442 return self.term == other.term.replace(other.variable, varex) 443 else: 444 return False

445

446 -class LambdaExpression(VariableBinderExpression):

447 - def str(self, syntax=Tokens.NEW_NLTK):

448 return Tokens.LAMBDA[syntax] + str(self.variable) + \ 449 Tokens.DOT[syntax] + self.term.str(syntax)

450

451 -class QuantifiedExpression(VariableBinderExpression):

452 - def str(self, syntax=Tokens.NEW_NLTK):

453 return self.getQuantifier(syntax) + ' ' + str(self.variable) + \ 454 Tokens.DOT[syntax] + self.term.str(syntax)

455

456 -class ExistsExpression(QuantifiedExpression):

457 - def getQuantifier(self, syntax=Tokens.NEW_NLTK):

458 return Tokens.EXISTS[syntax]

459

460 -class AllExpression(QuantifiedExpression):

461 - def getQuantifier(self, syntax=Tokens.NEW_NLTK):

462 return Tokens.ALL[syntax]

463

464 -class NegatedExpression(Expression):

465 - def __init__(self, term):

466 self.term = term

467

468 - def simplify(self):

469 return self.__class__(self.term.simplify())

470

471 - def replace(self, variable, expression, replace_bound=False):

472 """ 473 Replace every instance of 'variable' with 'expression' 474 @param variable: C{Variable} The variable to replace 475 @param expression: C{Expression} The expression with which to replace it 476 @param replace_bound: C{boolean} Should bound variables be replaced? 477 """ 478 return self.__class__(self.term.replace(variable, expression, 479 replace_bound))

480

481 - def variables(self):

482 """ 483 @see: Expression.variables() 484 """ 485 return self.term.variables()

486

487 - def free(self, indvar_only=True):

488 """ 489 @see: Expression.free() 490 """ 491 return self.term.free(indvar_only)

492

493 - def __eq__(self, other):

494 return self.__class__ == other.__class__ and self.term == other.term

495

496 - def str(self, syntax=Tokens.NEW_NLTK):

497 if syntax == Tokens.PROVER9: 498 return Tokens.NOT[syntax] + Tokens.OPEN + self.term.str(syntax) +\ 499 Tokens.CLOSE 500 else: 501 return Tokens.NOT[syntax] + self.term.str(syntax)

502

503 -class BooleanExpression(Expression):

504 - def __init__(self, first, second):

505 self.first = first 506 self.second = second

507

508 - def simplify(self):

509 return self.__class__(self.first.simplify(), self.second.simplify())

510

511 - def replace(self, variable, expression, replace_bound=False):

512 """ 513 Replace every instance of 'variable' with 'expression' 514 @param variable: C{Variable} The variable to replace 515 @param expression: C{Expression} The expression with which to replace it 516 @param replace_bound: C{boolean} Should bound variables be replaced? 517 """ 518 return self.__class__(self.first.replace(variable, expression, 519 replace_bound), 520 self.second.replace(variable, expression, 521 replace_bound))

522

523 - def variables(self):

524 """ 525 @see: Expression.variables() 526 """ 527 return self.first.variables() | self.second.variables()

528

529 - def free(self, indvar_only=True):

530 """ 531 @see: Expression.free() 532 """ 533 return self.first.free(indvar_only) | self.second.free(indvar_only)

534

535 - def __eq__(self, other):

536 return self.__class__ == other.__class__ \ 537 and self.first == other.first and self.second == other.second

538

539 - def str(self, syntax=Tokens.NEW_NLTK):

540 return Tokens.OPEN + self.first.str(syntax) + ' ' + self.getOp(syntax) \ 541 + ' ' + self.second.str(syntax) + Tokens.CLOSE

542

543 -class AndExpression(BooleanExpression):

544 """This class represents conjunctions"""

545 - def getOp(self, syntax=Tokens.NEW_NLTK):

546 return Tokens.AND[syntax]

547

548 -class OrExpression(BooleanExpression):

549 """This class represents disjunctions"""

550 - def getOp(self, syntax=Tokens.NEW_NLTK):

551 return Tokens.OR[syntax]

552

553 -class ImpExpression(BooleanExpression):

554 """This class represents implications"""

555 - def getOp(self, syntax=Tokens.NEW_NLTK):

556 return Tokens.IMP[syntax]

557

558 -class IffExpression(BooleanExpression):

559 """This class represents biconditionals"""

560 - def getOp(self, syntax=Tokens.NEW_NLTK):

561 return Tokens.IFF[syntax]

562

563 -class EqualityExpression(BooleanExpression):

564 """This class represents equality expressions like "(x = y)"."""

565 - def getOp(self, syntax=Tokens.NEW_NLTK):

566 return Tokens.EQ[syntax]

567 568

569 -class LogicParser:

570 """A lambda calculus expression parser.""" 571

572 - def __init__(self):

573 self._currentIndex = 0 574 self._buffer = []

575

576 - def parse(self, data):

577 """ 578 Parse the expression. 579 580 @param data: C{str} for the input to be parsed 581 @returns: a parsed Expression 582 """ 583 self._currentIndex = 0 584 self._buffer = self.process(data).split() 585 result = self.parse_Expression() 586 if self.inRange(0): 587 raise UnexpectedTokenException(self.token(0)) 588 return result

589

590 - def process(self, data):

591 """Put whitespace between symbols to make parsing easier""" 592 out = '' 593 tokenTrie = StringTrie(self.get_all_symbols()) 594 while data: 595 st = tokenTrie 596 c = data[0] 597 token = '' 598 while c in st: 599 token += c 600 st = st[c] 601 if len(data) > len(token): 602 c = data[len(token)] 603 else: 604 break 605 if token: 606 out += ' '+token+' ' 607 data = data[len(token):] 608 else: 609 out += c 610 data = data[1:] 611 return out

612

613 - def get_all_symbols(self):

614 """This method exists to be overridden""" 615 return Tokens.SYMBOLS

616

617 - def inRange(self, location):

618 """Return TRUE if the given location is within the buffer""" 619 return self._currentIndex+location < len(self._buffer)

620

621 - def token(self, location=None):

622 """Get the next waiting token. If a location is given, then 623 return the token at currentIndex+location without advancing 624 currentIndex; setting it gives lookahead/lookback capability.""" 625 try: 626 if location == None: 627 tok = self._buffer[self._currentIndex] 628 self._currentIndex += 1 629 else: 630 tok = self._buffer[self._currentIndex+location] 631 return tok 632 except IndexError: 633 raise UnexpectedTokenException, 'The given location is out of range'

634

635 - def isvariable(self, tok):

636 return tok not in Tokens.TOKENS

637

638 - def parse_Expression(self, allow_adjuncts=True):

639 """Parse the next complete expression from the stream and return it.""" 640 tok = self.token() 641 642 accum = self.handle(tok) 643 644 if not accum: 645 raise UnexpectedTokenException(tok) 646 647 if allow_adjuncts: 648 accum = self.attempt_ApplicationExpression(accum) 649 accum = self.attempt_BooleanExpression(accum) 650 651 return accum

652

653 - def handle(self, tok):

654 """This method is intended to be overridden for logics that 655 use different operators or expressions""" 656 if self.isvariable(tok): 657 return self.handle_variable(tok) 658 659 elif tok in Tokens.NOT: 660 return self.handle_negation() 661 662 elif tok in Tokens.LAMBDA: 663 return self.handle_lambda(tok) 664 665 elif tok in Tokens.QUANTS: 666 return self.handle_quant(tok) 667 668 elif tok == Tokens.OPEN: 669 return self.handle_open(tok)

670

671 - def handle_negation(self):

672 return self.make_NegatedExpression(self.parse_Expression(False))

673

674 - def make_NegatedExpression(self, expression):

675 return NegatedExpression(expression)

676

677 - def handle_variable(self, tok):

678 #It's either: 1) a predicate expression: sees(x,y) 679 # 2) an application expression: P(x) 680 # 3) a solo variable: john OR x 681 accum = self.make_VariableExpression(tok) 682 if self.inRange(0) and self.token(0) == Tokens.OPEN: 683 #The predicate has arguments 684 if is_indvar(tok): 685 raise ParseException('\'%s\' is an illegal variable name. ' 686 'Predicate variables may not be ' 687 'individual variables' % tok) 688 self.token() #swallow the Open Paren 689 690 #curry the arguments 691 accum = self.make_ApplicationExpression(accum, 692 self.parse_Expression()) 693 while self.token(0) == Tokens.COMMA: 694 self.token() #swallow the comma 695 accum = self.make_ApplicationExpression(accum, 696 self.parse_Expression()) 697 self.assertToken(self.token(), Tokens.CLOSE) 698 return self.attempt_EqualityExpression(accum)

699

700 - def handle_lambda(self, tok):

701 # Expression is a lambda expression 702 vars = [Variable(self.token())] 703 while self.isvariable(self.token(0)): 704 # Support expressions like: \x y.M == \x.\y.M 705 vars.append(Variable(self.token())) 706 self.assertToken(self.token(), Tokens.DOT) 707 708 accum = self.parse_Expression(False) 709 while vars: 710 accum = self.make_LambdaExpression(vars.pop(), accum) 711 return accum

712

713 - def get_QuantifiedExpression_factory(self, tok):

714 """This method serves as a hook for other logic parsers that 715 have different quantifiers""" 716 factory = None 717 if tok in Tokens.EXISTS: 718 factory = ExistsExpression 719 elif tok in Tokens.ALL: 720 factory = AllExpression 721 else: 722 self.assertToken(tok, Tokens.QUANTS) 723 return factory

724

725 - def handle_quant(self, tok):

726 # Expression is a quantified expression: some x.M 727 factory = self.get_QuantifiedExpression_factory(tok) 728 729 vars = [self.token()] 730 while self.isvariable(self.token(0)): 731 # Support expressions like: some x y.M == some x.some y.M 732 vars.append(self.token()) 733 self.assertToken(self.token(), Tokens.DOT) 734 735 accum = self.parse_Expression(False) 736 while vars: 737 var = vars.pop() 738 if not is_indvar(var): 739 raise ParseException('\'%s\' is an illegal variable name. ' 740 'Quantifier variables must be individual ' 741 'variables' % var) 742 accum = factory(Variable(var), accum) 743 return accum

744

745 - def handle_open(self, tok):

746 #Expression is in parens 747 accum = self.parse_Expression() 748 self.assertToken(self.token(), Tokens.CLOSE) 749 return accum

750

751 - def attempt_EqualityExpression(self, expression):

752 """Attempt to make a boolean expression. If the next token is a boolean 753 operator, then a BooleanExpression will be returned. Otherwise, the 754 parameter will be returned.""" 755 if self.inRange(0) and self.token(0) in Tokens.EQ: 756 self.token() #swallow the "=" 757 return self.make_EqualityExpression(expression, 758 self.parse_Expression()) 759 elif self.inRange(0) and self.token(0) in Tokens.NEQ: 760 self.token() #swallow the "!=" 761 return self.make_NegatedExpression( 762 self.make_EqualityExpression(expression, 763 self.parse_Expression())) 764 return expression

765

766 - def make_EqualityExpression(self, first, second):

767 """This method serves as a hook for other logic parsers that 768 have different equality expression classes""" 769 return EqualityExpression(first, second)

770

771 - def attempt_BooleanExpression(self, expression):

772 """Attempt to make a boolean expression. If the next token is a boolean 773 operator, then a BooleanExpression will be returned. Otherwise, the 774 parameter will be returned.""" 775 if self.inRange(0): 776 factory = self.get_BooleanExpression_factory() 777 if factory: #if a factory was returned 778 self.token() #swallow the operator 779 return self.make_BooleanExpression(factory, expression, 780 self.parse_Expression()) 781 #otherwise, no boolean expression can be created 782 return expression

783

784 - def get_BooleanExpression_factory(self):

785 """This method serves as a hook for other logic parsers that 786 have different boolean operators""" 787 factory = None 788 op = self.token(0) 789 if op in Tokens.AND: 790 factory = AndExpression 791 elif op in Tokens.OR: 792 factory = OrExpression 793 elif op in Tokens.IMP: 794 factory = ImpExpression 795 elif op in Tokens.IFF: 796 factory = IffExpression 797 return factory

798

799 - def make_BooleanExpression(self, type, first, second):

800 """This method exists to be overridden by parsers 801 with more complex logic for creating BooleanExpressions""" 802 return type(first, second)

803

804 - def attempt_ApplicationExpression(self, expression):

805 """Attempt to make an application expression. The next tokens are 806 a list of arguments in parens, then the argument expression is a 807 function being applied to the arguments. Otherwise, return the 808 argument expression.""" 809 if self.inRange(0) and self.token(0) == Tokens.OPEN: 810 if not isinstance(expression, LambdaExpression) and \ 811 not isinstance(expression, ApplicationExpression): 812 raise ParseException("The function '" + str(expression) + 813 ' is not a Lambda Expression or an ' 814 'Application Expression, so it may not ' 815 'take arguments') 816 self.token() #swallow then open paren 817 #curry the arguments 818 accum = self.make_ApplicationExpression(expression, 819 self.parse_Expression()) 820 while self.token(0) == Tokens.COMMA: 821 self.token() #swallow the comma 822 accum = self.make_ApplicationExpression(accum, 823 self.parse_Expression()) 824 self.assertToken(self.token(), Tokens.CLOSE) 825 return self.attempt_ApplicationExpression(accum) 826 else: 827 return expression

828

829 - def make_ApplicationExpression(self, function, argument):

830 return ApplicationExpression(function, argument)

831

832 - def make_VariableExpression(self, name):

833 if is_indvar(name): 834 return IndividualVariableExpression(Variable(name)) 835 else: 836 return VariableExpression(Variable(name))

837

838 - def make_LambdaExpression(self, variable, term):

839 return LambdaExpression(variable, term)

840

841 - def assertToken(self, tok, expected):

842 if isinstance(expected, list): 843 if tok not in expected: 844 raise UnexpectedTokenException(tok, expected) 845 else: 846 if tok != expected: 847 raise UnexpectedTokenException(tok, expected)

848

849 - def __repr__(self):

850 if self.inRange(0): 851 return 'Next token: ' + self.token(0) 852 else: 853 return 'No more tokens'

854 855

856 -class StringTrie(dict):

857 LEAF = "<leaf>" 858

859 - def __init__(self, strings=None):

860 if strings: 861 for string in strings: 862 self.insert(string)

863

864 - def insert(self, string):

865 if len(string): 866 k = string[0] 867 if k not in self: 868 self[k] = StringTrie() 869 self[k].insert(string[1:]) 870 else: 871 #mark the string is complete 872 self[StringTrie.LEAF] = None

873

874 -class ParseException(Exception):

875 - def __init__(self, message):

876 Exception.__init__(self, message)

877

878 -class UnexpectedTokenException(ParseException):

879 - def __init__(self, tok, expected=None):

880 if expected: 881 ParseException.__init__(self, "parse error, unexpected token: %s. " 882 "Expected token: %s" % (tok, expected)) 883 else: 884 ParseException.__init__(self, "parse error, unexpected token: %s" 885 % tok)

886 887

888 -def is_indvar(expr):

889 """ 890 An individual variable must be a single lowercase character followed by 891 zero or more digits. 892 893 @param expr: C{str} 894 @return: C{boolean} True if expr is of the correct form 895 """ 896 try: 897 return expr[0].isalpha() and expr[0].islower() and \ 898 (len(expr) == 1 or expr[1:].isdigit()) 899 except TypeError: 900 return False

901

902 -def demo():

903 lp = LogicParser() 904 print '='*20 + 'Test parser' + '='*20 905 print lp.parse(r'john') 906 print lp.parse(r'man(x)') 907 print lp.parse(r'-man(x)') 908 print lp.parse(r'(man(x) & tall(x) & walks(x))') 909 print lp.parse(r'exists x.(man(x) & tall(x))') 910 print lp.parse(r'\x.man(x)') 911 print lp.parse(r'\x.man(x)(john)') 912 print lp.parse(r'\x y.sees(x,y)') 913 print lp.parse(r'\x y.sees(x,y)(a,b)') 914 print lp.parse(r'(\x.exists y.walks(x,y))(x)') 915 print lp.parse(r'exists x.(x = john)') 916 print lp.parse(r'\P Q.exists x.(P(x) & Q(x))') 917 918 print '='*20 + 'Test simplify' + '='*20 919 print lp.parse(r'\x.\y.sees(x,y)(john)(mary)').simplify() 920 print lp.parse(r'\x.\y.sees(x,y)(john, mary)').simplify() 921 print lp.parse(r'exists x.(man(x) & (\x.exists y.walks(x,y))(x))').simplify() 922 print lp.parse(r'(\P.\Q.exists x.(P(x) & Q(x)))(\x.dog(x))(\x.bark(x))').simplify() 923 924 print '='*20 + 'Test alpha conversion and binder expression equality' + '='*20 925 e1 = lp.parse('exists x.P(x)') 926 print e1 927 e2 = e1.alpha_convert(VariableExpression('z')) 928 print e2 929 print e1 == e2

930 931 if __name__ == '__main__': 932 demo() 933

Source Code for Module nltk.sem.logic