1
2 from nltk_lite.utilities import Counter
3 from featurelite import SubstituteBindingsMixin, FeatureI
4 from featurelite import Variable as FeatureVariable
5 _counter = Counter()
6
11
12 -class Error(Exception): pass
13
15 """A variable, either free or bound."""
16
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
28
30 return not self.equals(other)
31
33 """A comparison function."""
34 if not isinstance(other, Variable): return False
35 return self.name == other.name
36
38
40
42
44 """A nonlogical constant."""
45
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
57
59 return not self.equals(other)
60
62 """A comparison function."""
63 assert isinstance(other, Constant)
64 return self.name == other.name
65
67
69
71
73 """The abstract class of a lambda calculus expression."""
75 if self.__class__ is Expression:
76 raise NotImplementedError
77
80
82 return not self.equals(other)
83
85 """Are the two expressions equal, modulo alpha conversion?"""
86 return NotImplementedError
87
89 """Set of all variables."""
90 raise NotImplementedError
91
93 """Set of free variables."""
94 raise NotImplementedError
95
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
114 """Evaluate the form by repeatedly applying applications."""
115 raise NotImplementedError
116
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
128 raise NotImplementedError
129
132
134 raise NotImplementedError
135
137 raise NotImplementedError
138
140 raise NotImplementedError, self.__class__
141
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
154 """A variable expression which consists solely of a variable."""
159
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
172 return [self.variable]
173
175 return set([self.variable])
176
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
191
194
197
200
201 - def __str__(self): return '%s' % self.variable
202
203 - def __repr__(self): return "VariableExpression('%s')" % self.variable
204
206
207
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
225 """
226 An individual variable expression, as determined by C{is_indvar()}.
227 """
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
238 """A constant expression, consisting solely of a constant."""
243
245 if self.__class__ == other.__class__:
246 return self.constant.equals(other.constant)
247 else:
248 return False
249
252
255
258
259 - def replace(self, variable, expression, replace_bound=False):
261
264
267
270
273
274 - def __str__(self): return '%s' % self.constant
275
276 - def __repr__(self): return "ConstantExpression('%s')" % self.constant
277
279
280
282 """
283 A boolean operator, such as 'not' or 'and', or the equality
284 relation ('=').
285 """
291
293 if self.__class__ == other.__class__:
294 return self.constant == other.constant
295 else:
296 return False
297
300
301 - def __str__(self): return '%s' % self.operator
302
303 - def __repr__(self): return "Operator('%s')" % self.operator
304
305
306
308 """A variable binding expression: e.g. \\x.M."""
309
310
311 _counter = Counter()
312
322
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
335
336 relabeled = self._relabel(other)
337 return self.term == relabeled
338 else:
339 return False
340
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
354
356 return self.term.free().difference(set([self.variable]))
357
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
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
381 return self.__class__(self.variable, self.term.simplify())
382
384 return self.__class__(self.variable, self.term.infixify())
385
386 - def __str__(self, continuation=0):
387
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
399
401 """A lambda expression: \\x.M."""
402 PREFIX = '\\'
403
405 bv = bound_vars.copy()
406 bv.add(self.variable)
407 return self.__class__(self.variable, self.term._skolemise(bv, counter))
408
411
412
414 """An existential quantification expression: some x.M."""
415 PREFIX = 'some '
416
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
429
430
431
433 """A universal quantification expression: all x.M."""
434 PREFIX = 'all '
435
437 bv = bound_vars.copy()
438 bv.add(self.variable)
439 return self.__class__(self.variable, self.term._skolemise(bv, counter))
440
443
444
445
446
448 """An application expression: (M N)."""
455
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
468
470 return self.first.free().union(self.second.free())
471
477
478 fun = property(_functor,
479 doc="Every ApplicationExpression has a functor.")
480
481
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
498
503
504 args = property(_args,
505 doc="Every ApplicationExpression has args.")
506
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
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
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
537 first = self.first._skolemise(bound_vars, counter)
538 second = self.second._skolemise(bound_vars, counter)
539 return self.__class__(first, second)
540
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]
548
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
557
558
561
564
567
570
573
575 """A lambda calculus expression parser."""
576
577
578
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
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
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
647 return None
648
656
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
663
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
676
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
690 first = self.next()
691 second = self.next()
692 exps = []
693 while self.token(0) != Parser.CLOSE:
694
695 exps.append(self.next())
696 tok = self.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
709 return ConstantExpression(Constant(tok))
710
711 elif tok in Parser.OPS:
712
713 return Operator(tok)
714
715 elif is_indvar(tok):
716
717 return IndVariableExpression(Variable(tok))
718
719 else:
720 if self.isVariable(tok):
721
722 return VariableExpression(Variable(tok))
723 else:
724 raise Error, "parse error, unexpected token: %s" % tok
725
726
727
728
729
738
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
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