1
2
3
4
5
6
7
8
9
10
11
12
13
14
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
30 """A variable, either free or bound."""
31
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
43
45 return not self.equals(other)
46
48 """A comparison function."""
49 assert isinstance(other, Variable)
50 return self.name == other.name
51
53
55
57
59 """A nonlogical constant."""
60
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
72
74 return not self.equals(other)
75
77 """A comparison function."""
78 assert isinstance(other, Constant)
79 return self.name == other.name
80
82
84
86
88 """The abstract class of a lambda calculus expression."""
90 if self.__class__ is Expression:
91 raise NotImplementedError
92
95
97 return not self.equals(other)
98
100 """Are the two expressions equal, modulo alpha conversion?"""
101 return NotImplementedError
102
104 """Set of all variables."""
105 raise NotImplementedError
106
108 """Set of free variables."""
109 raise NotImplementedError
110
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
122 """Evaluate the form by repeatedly applying applications."""
123 raise NotImplementedError
124
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
134 raise NotImplementedError
135
137 raise NotImplementedError
138
140 raise NotImplementedError
141
143 raise NotImplementedError
144
146 """A variable expression which consists solely of a variable."""
151
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
164 return set([self.variable])
165
167 return set([self.variable])
168
171
172 - def replace(self, variable, expression):
173 if self.variable.equals(variable):
174 return expression
175 else:
176 return self
177
180
183
186
189
190 - def __str__(self): return '%s' % self.variable
191
192 - def __repr__(self): return "VariableExpression('%s')" % self.variable
193
195
196
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
214 """
215 An individual variable expression, as determined by C{is_indvar()}.
216 """
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
227 """A constant expression, consisting solely of a constant."""
232
234 if self.__class__ == other.__class__:
235 return self.constant.equals(other.constant)
236 else:
237 return False
238
241
244
247
248 - def replace(self, variable, expression):
250
253
256
259
262
263 - def __str__(self): return '%s' % self.constant
264
265 - def __repr__(self): return "ConstantExpression('%s')" % self.constant
266
268
269
271 """
272 A boolean operator, such as 'not' or 'and', or the equality
273 relation ('=').
274 """
280
282 if self.__class__ == other.__class__:
283 return self.constant == other.constant
284 else:
285 return False
286
289
290 - def __str__(self): return '%s' % self.operator
291
292 - def __repr__(self): return "Operator('%s')" % self.operator
293
294
295
297 """A variable binding expression: e.g. \\x.M."""
298
299
300 _counter = Counter()
301
311
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
324
325 relabeled = self._relabel(other)
326 return self.term == relabeled
327 else:
328 return False
329
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
339 return set([self.variable]).union(self.term.variables())
340
342 return self.term.free().difference(set([self.variable]))
343
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
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
365 return self.__class__(self.variable, self.term.simplify())
366
368 return self.__class__(self.variable, self.term.infixify())
369
370 - def __str__(self, continuation=0):
371
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
382 return hash(repr(self))
383
385 """A lambda expression: \\x.M."""
386 PREFIX = '\\'
387
389 bv = bound_vars.copy()
390 bv.add(self.variable)
391 return self.__class__(self.variable, self.term._skolemise(bv, counter))
392
394 return "LambdaExpression('%s', '%s')" % (self.variable, self.term)
395
397 """An existential quantification expression: some x.M."""
398 PREFIX = 'some '
399
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
411 return "SomeExpression('%s', '%s')" % (self.variable, self.term)
412
413
415 """A universal quantification expression: all x.M."""
416 PREFIX = 'all '
417
419 bv = bound_vars.copy()
420 bv.add(self.variable)
421 return self.__class__(self.variable, self.term._skolemise(bv, counter))
422
424 return "AllExpression('%s', '%s')" % (self.variable, self.term)
425
426
427
429 """An application expression: (M N)."""
436
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
446
448 return self.first.free().union(self.second.free())
449
455
456 fun = property(_functor,
457 doc="Every ApplicationExpression has a functor.")
458
459
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
476
481
482 args = property(_args,
483 doc="Every ApplicationExpression has args.")
484
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
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
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
514 first = self.first._skolemise(bound_vars, counter)
515 second = self.second._skolemise(bound_vars, counter)
516 return self.__class__(first, second)
517
519
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
529
531 """A lambda calculus expression parser."""
532
533
534
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
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
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
603 return None
604
612
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
619
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
632
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
646 first = self.next()
647 second = self.next()
648 exps = []
649 while self.token(0) != Parser.CLOSE:
650
651 exps.append(self.next())
652 tok = self.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
665 return ConstantExpression(Constant(tok))
666
667 elif tok in Parser.OPS:
668
669 return Operator(tok)
670
671 elif is_indvar(tok):
672
673 return IndVariableExpression(Variable(tok))
674
675 else:
676 if self.isVariable(tok):
677
678 return VariableExpression(Variable(tok))
679 else:
680 raise Error, "parse error, unexpected token: %s" % tok
681
682
683
684
685
688
689
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
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