Package jazzparser :: Package formalisms :: Package base :: Package semantics :: Module lambdacalc
[hide private]
[frames] | no frames]

Source Code for Module jazzparser.formalisms.base.semantics.lambdacalc

  1  """Lambda calculus semantic representations for the Jazz Parser. 
  2   
  3  Defines a set of base classes for use in defining and handling semantic  
  4  interpretations of jazz chord sequences. These take the form of  
  5  lambda-expressions containing predicates. 
  6   
  7  A semantic representation should be created as a Semantics object. 
  8  This should be initialised with a LogicalForm object defining 
  9  the logical form it represents. 
 10   
 11  LambdaAbstraction, FunctionApplication and Variable define the  
 12  basic lambda expressions. 
 13   
 14  """ 
 15  """ 
 16  ============================== License ======================================== 
 17   Copyright (C) 2008, 2010-12 University of Edinburgh, Mark Granroth-Wilding 
 18    
 19   This file is part of The Jazz Parser. 
 20    
 21   The Jazz Parser is free software: you can redistribute it and/or modify 
 22   it under the terms of the GNU General Public License as published by 
 23   the Free Software Foundation, either version 3 of the License, or 
 24   (at your option) any later version. 
 25    
 26   The Jazz Parser is distributed in the hope that it will be useful, 
 27   but WITHOUT ANY WARRANTY; without even the implied warranty of 
 28   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the 
 29   GNU General Public License for more details. 
 30    
 31   You should have received a copy of the GNU General Public License 
 32   along with The Jazz Parser.  If not, see <http://www.gnu.org/licenses/>. 
 33   
 34  ============================ End license ====================================== 
 35   
 36  """ 
 37  __author__ = "Mark Granroth-Wilding <mark.granroth-wilding@ed.ac.uk>"  
 38   
 39  import copy 
 40  import logging 
 41  from jazzparser import settings 
 42   
 43  # Get the logger from the logging system 
 44  logger = logging.getLogger("main_logger") 
 45   
46 -class Semantics(object):
47 """This acts as the root node in the LF's tree structure. Any 48 LF that is built as a semantic representation should 49 be contained in an instance of Semantics. 50 51 """
52 - def __init__(self, lf):
53 """ 54 Creates a new container for a logical form. The 55 logical form itself should be given as lf (an instance 56 of a subclass of LogicalForm) 57 58 """ 59 self.lf = lf 60 lf.parent = self
61
62 - def beta_reduce(self, *args, **kwargs):
63 """ 64 Beta-reduction. Takes place in place 65 (i.e. the result will be substituted into the parent), but the 66 final result is returning, for convenience. 67 68 """ 69 return self.lf.beta_reduce(*args, **kwargs)
70
71 - def replace_immediate_constituent(self, old_lf, new_lf):
72 if self.lf is old_lf: 73 self.lf = new_lf 74 new_lf.parent = self
75
76 - def __eq__(self, expr):
77 return (type(self) == type(expr)) and \ 78 (self.lf == expr.lf)
79
80 - def __ne__(self, other):
81 return not (self == other)
82
83 - def alpha_equivalent(self, other):
84 # Start with an empty substitution 85 return self.lf.alpha_equivalent(other.lf, {})
86
87 - def __str__(self):
88 return "%s" % (self.lf)
89
90 - def to_latex(self):
91 return self.lf.to_latex()
92
93 - def get_children(self):
94 return [self.lf]
95
96 - def copy(self):
97 return type(self)(self.lf.copy())
98
100 return set()
101
102 - def __repr__(self):
103 return str(self)
104 105
106 -class LogicalForm(object):
107 """ 108 A semantic element, used to build the semantic 109 interpretations returned by the parser. 110 This class is effectively abstract. Most of its methods 111 should be overridden. 112 113 """
114 - def __init__(self):
115 """ Builds a basic logical form object. """ 116 self.parent = None
117
118 - def alpha_convert(self, source_var, target_var):
119 """This should be overridden by subclasses.""" 120 raise NotImplementedError, "Called abstract "\ 121 "LogicalForm.alpha_convert() on %s" % type(self).__name__
122
123 - def beta_reduce(self, *args, **kwargs):
124 """This should be overridden by subclasses.""" 125 raise NotImplementedError, "Called abstract "\ 126 "LogicalForm.beta_reduce() on %s" % type(self).__name__
127
128 - def substitute(self, source_variable, target_expression):
129 """This should be overridden by subclasses.""" 130 raise NotImplementedError, "Called abstract "\ 131 "LogicalForm.substitute() on %s" % type(self).__name__
132
133 - def replace_immediate_constituent(self, old_lf, new_lf):
134 """ 135 This should be overridden by subclasses. 136 It should replace the LogicalForm old_lf with new_lf if it 137 appears as an immediate constituent of this LogicalForm. 138 139 """ 140 raise NotImplementedError, "Called abstract "\ 141 "LogicalForm.replace_immediate_constituent() on %s" % \ 142 type(self).__name__
143
144 - def get_variables(self):
145 """ 146 This should be overridden by subclasses. 147 148 This method returns a list of all the variables 149 used in this LF. This includes bound and unbound variables. 150 (Only unbound variables need to be alpha-converted to 151 avoid accidental binding, but we will convert bound variables 152 too for readability.) 153 154 Note that this only contains one instance of each variable, 155 not every occurrence. 156 157 """ 158 raise NotImplementedError, "Called abstract "\ 159 "LogicalForm.get_variables() on %s" % type(self).__name__
160
161 - def get_bound_variables(self):
162 """This should be overridden by subclasses.""" 163 raise NotImplementedError, "Called abstract "\ 164 "LogicalForm.get_variables() on %s" % type(self).__name__
165
166 - def get_unbound_variables(self):
167 return set(self.get_variables()) - set(self.get_bound_variables())
168
169 - def get_children(self):
170 """This should be overridden by subclasses.""" 171 raise NotImplementedError, "Called abstract "\ 172 "LogicalForm.get_children() on %s" % type(self).__name__
173
174 - def get_instances(self, lf):
175 """ 176 Returns all instances of logical forms equal to L{lf} among this 177 logical form and its descendents. 178 This is particularly useful for getting all instances of a 179 variable. 180 181 """ 182 insts = [] 183 if self == lf: 184 insts.append(self) 185 for child in self.get_children(): 186 insts.extend(child.get_instances(lf)) 187 return insts
188
189 - def alpha_equivalent(self, other, substitution):
190 """This should be overridden by subclasses.""" 191 raise NotImplementedError, "Called abstract "\ 192 "LogicalForm.alpha_equivalent() on %s" % type(self).__name__
193
194 - def __eq__(self, other):
195 """This should be overridden by subclasses.""" 196 raise NotImplementedError, "Called abstract "\ 197 "LogicalForm.__eq__() on %s" % type(self).__name__
198
199 - def __ne__(self, lf):
200 return not (self == lf)
201
202 - def copy(self):
203 """This should be overridden by subclasses.""" 204 raise NotImplementedError, "Called abstract "\ 205 "LogicalForm.copy() on %s" % type(self).__name__
206
207 - def replace_in_parent(self, other):
208 """ 209 Replaces references in this LF's parent to this LF with references 210 to the LF other. 211 """ 212 self.parent.replace_immediate_constituent(self, other)
213
215 """ 216 Returns all the variables that are bound at some point 217 higher up the structure and can therefore be used unbound within 218 this element. 219 """ 220 if self.parent is not None: 221 vars = self.parent.get_ancestor_bound_variables() 222 if isinstance(self.parent, LambdaAbstraction): 223 vars.add(self.parent.variable) 224 return vars 225 else: 226 return set()
227
228 - def __repr__(self):
229 return str(self)
230 231
232 -class LambdaAbstraction(LogicalForm):
233 """ 234 A type of complex logical form element corresponding 235 to a lambda abstraction. 236 237 """ 238
239 - def __init__(self, variable, expression):
240 """ 241 Builds a lambda abstraction. variable should be a 242 Variable object and expression should be another 243 LogicalForm, potentially containing the variable, 244 bound by this abstraction. 245 246 """ 247 super(LambdaAbstraction, self).__init__() 248 self.variable = variable.copy() 249 self.variable.parent = self 250 self.expression = expression.copy() 251 self.expression.parent = self
252
253 - def copy(self):
254 # Copying of these args is already done in the constructor 255 return type(self)(self.variable, self.expression)
256
257 - def alpha_convert(self, source_var, target_var):
258 self.variable.alpha_convert(source_var, target_var) 259 self.expression.alpha_convert(source_var, target_var)
260
261 - def beta_reduce(self, *args, **kwargs):
262 self.expression.beta_reduce(*args, **kwargs) 263 return self
264
265 - def substitute(self, source_variable, target_expression):
266 # Note: should never end up having to substitute the abstracted variable 267 if source_variable == self.variable: 268 logger.warning("Trying to substitute a bound variable: %s for %s in abstraction %s" % (target_expression, source_variable, self)) 269 raise ValueError, "Trying to substitute a bound variable: %s for %s in abstraction %s" % (target_expression, source_variable, self) 270 self.expression.substitute(source_variable, target_expression)
271
272 - def replace_immediate_constituent(self, old_lf, new_lf):
273 if self.variable is old_lf: 274 self.variable.parent = None 275 self.variable = new_lf 276 new_lf.parent = self 277 if self.expression is old_lf: 278 self.expression.parent = None 279 self.expression = new_lf 280 new_lf.parent = self
281
282 - def get_variables(self):
283 # Add the abstracted variable to the list 284 our_var = [self.variable] 285 # Recursively add all variables in sub-expressions 286 return list(set(self.expression.get_variables() + our_var))
287
288 - def get_bound_variables(self):
289 # Start with the abstracted variable 290 vars = [self.variable] 291 # Add any bound vars in the subexpression 292 vars.extend(self.expression.get_bound_variables()) 293 return vars
294
295 - def __eq__(self, lf):
296 return (type(lf) == type(self)) and \ 297 (self.variable == lf.variable) and \ 298 (self.expression == lf.expression)
299
300 - def alpha_equivalent(self, other, substitution):
301 """ 302 Checks whether self is equal to a LF that can be derived by 303 some variable substitution S into other, where S contains the 304 substitution T given by "substitution". 305 """ 306 # Must both be lambda abstractions 307 if type(self) != type(other): 308 return False 309 # If the abstracted variable is in T, something's gone horribly wrong: 310 # it shouldn't yet be bound, so can't be in the current substitution. 311 if other.variable in substitution: 312 return False 313 314 # Check self isn't already the target of a substitution 315 if self in substitution.values(): 316 return False 317 318 # We're allowed now to add a substitution to make the abstracted 319 # variables equal 320 # We might need to use a Variable class specific to the formalism 321 if hasattr(type(self), 'VARIABLE_CLASS'): 322 var_cls = type(self).VARIABLE_CLASS 323 else: 324 var_cls = Variable 325 # This new substitution should only be used within this scope 326 new_subst = copy.copy(substitution) 327 new_subst[other.variable] = var_cls(self.variable.name, \ 328 self.variable.index) 329 330 # Check that the subexpressions are alpha-equivalent, using this subst 331 return self.expression.alpha_equivalent(other.expression, new_subst)
332
333 - def comma_string(self):
334 """Returns the string that is to be used if this expression 335 follows another lambda abstraction. 336 337 """ 338 output = self.variable.__str__() 339 ## If the sub-expression is another abstraction, use comma notation for that 340 if self.expression.__class__ == self.__class__: 341 output += "," 342 output += self.expression.comma_string() 343 else: 344 output += "." 345 output += self.expression.__str__() 346 return output
347
348 - def comma_latex(self):
349 """Returns the Latex representation that is to be used if this expression 350 follows another lambda abstraction. 351 352 """ 353 output = self.variable.to_latex() 354 ## If the sub-expression is another abstraction, use comma notation for that 355 if self.expression.__class__ == self.__class__: 356 output += "," 357 output += self.expression.comma_latex() 358 else: 359 output += "." 360 output += self.expression.to_latex() 361 return output
362
363 - def __str__(self):
364 output = "" 365 output += "\\" 366 ## From here on, same as the comma string 367 output += self.comma_string() 368 return output
369
370 - def to_latex(self):
371 output = "\\lambda " 372 ## From here on, same as the comma string 373 output += self.comma_latex() 374 return output
375
376 - def get_children(self):
377 return [self.variable, self.expression]
378
379 -class Variable(LogicalForm):
380 """A variable in a semantic expression.""" 381
382 - def __init__(self, name, index=0):
383 """Creates a new variable object, representing the 384 variable given by name. 385 386 """ 387 super(Variable, self).__init__() 388 self.name = name 389 self.index = index
390
391 - def copy(self):
392 return type(self)(copy.copy(self.name),copy.copy(self.index))
393
394 - def get_variable_name(self):
395 return "%s%d" % (self.name, self.index)
396
397 - def alpha_convert(self, source_var, target_var):
398 if (self.name == source_var.name) and (self.index == source_var.index): 399 self.name = target_var.name 400 self.index = target_var.index
401
402 - def beta_reduce(self, *args, **kwargs):
403 # Doesn't do anything 404 return self
405
406 - def substitute(self, source_variable, target_expression):
407 if source_variable==self: 408 new_expression = target_expression.copy() 409 ## We've been asked to substitute self with another expression 410 self.parent.replace_immediate_constituent(self, \ 411 new_expression)
412
413 - def replace_immediate_constituent(self, old_lf, new_lf):
414 # Variable has no constituents 415 pass
416
417 - def get_variables(self):
418 # This is a variable: base case 419 return [self]
420
421 - def get_bound_variables(self):
422 # This is an unbound variable. Return nothing. 423 return []
424
425 - def __eq__(self, lf):
426 """For the time being, two variables are considered equal 427 if they have the same name. We could use some more elaborate 428 internal representation if this turns out to be a problem, 429 but if alpha conversion is carried out when it should be this 430 method ought to be ok. 431 432 """ 433 return (type(lf) == type(self)) and \ 434 (lf.name == self.name) and \ 435 (lf.index == self.index)
436
437 - def alpha_equivalent(self, other, substitution):
438 """ 439 Checks whether self is equal to a LF that can be derived by 440 some variable substitution S into other, where S contains the 441 substitution T given by "substitution". 442 """ 443 # Must both be variables 444 if type(self) != type(other): 445 return False 446 447 # If there's a substitution for other, we use it. Otherwise, 448 # it must have been a free variable, so we add it to the substitution 449 # to make sure it's substituted in the same way everywhere 450 if other in substitution: 451 return self == substitution[other] 452 else: 453 # Check self isn't already the target of a substitution 454 if self in substitution.values(): 455 return False 456 substitution[other] = self.copy() 457 return True
458
459 - def __str__(self):
460 output = self.get_variable_name() 461 return output
462
463 - def to_latex(self):
464 # Put the index as a subscript 465 from jazzparser.utils.latex import filter_latex 466 return "%s_{%d}" % (filter_latex(self.name), self.index)
467
468 - def get_children(self):
469 return []
470
471 - def get_sibling_variables(self):
472 """ 473 Returns a list of all the instances of Variable within 474 the logical form that represent the same variable. 475 476 If it's a free variable, returns all other occurrences 477 within the logical form. If it's bound, returns all 478 other variables bound by the same abstraction. 479 480 """ 481 parent = self 482 while not (isinstance(parent, LambdaAbstraction) and \ 483 parent.variable == self) and \ 484 not isinstance(parent, Semantics) and \ 485 parent.parent is not None: 486 parent = parent.parent 487 return parent.get_instances(self)
488
489 - def __hash__(self):
490 return self.index
491 492
493 -class FunctionApplication(LogicalForm):
494 """ 495 A function application in a semantic expression. 496 This is where all the real work goes on. Beta-reduction of function 497 applications is the only bit that really does anything interesting. 498 499 """ 500 INFIX_OPERATORS = [] 501
502 - def __init__(self, functor, argument):
503 """ 504 functor must be a lambda abstraction. 505 argument can be any LogicalForm. 506 507 """ 508 super(FunctionApplication, self).__init__() 509 self.functor = functor.copy() 510 self.functor.parent = self 511 self.argument = argument.copy() 512 self.argument.parent = self
513
514 - def copy(self):
515 # Copying of args is done in the constructor anyway 516 return type(self)(self.functor, self.argument)
517
518 - def alpha_convert(self, source_var, target_var):
519 self.functor.alpha_convert(source_var, target_var) 520 self.argument.alpha_convert(source_var, target_var)
521
522 - def beta_reduce(self, *args, **kwargs):
523 ## Before doing anything else, the functor must be beta-converted 524 self.functor.beta_reduce(*args, **kwargs) 525 ## Now if the functor is a lambda expression, we must apply it to the arg 526 if isinstance(self.functor, LambdaAbstraction): 527 ## First make sure no variable in the functor occurs in the arg. 528 # Free variables are fine to overlap - they might be bound higher up. 529 arg_vars = set(self.argument.get_bound_variables()) 530 fun_vars = set(self.functor.get_bound_variables()) 531 # Also avoid using any variables bound higher up 532 used_vars = set([ 533 var.copy() for var in \ 534 (arg_vars | 535 fun_vars | 536 self.get_ancestor_bound_variables())]) 537 # Alpha-convert each of the intersection's variables 538 # in one of the expressions 539 overlap = [var.copy() for var in (arg_vars & fun_vars)] 540 for var in overlap: 541 # Alpha-convert the argument to remove the potential accidental binding 542 # Get a variable that's not been used yet in either expression 543 new_var = next_unused_variable(var, used_vars) 544 self.argument.alpha_convert(var, new_var) 545 # Don't use the variable again 546 used_vars.add(new_var) 547 548 self.functor.expression.substitute(self.functor.variable, self.argument) 549 550 ## self should now be replaced by this converted argument 551 expr = self.functor.expression 552 self.replace_in_parent(expr) 553 554 ## Continue beta-conversion on the resulting expression 555 return expr.beta_reduce(*args, **kwargs) 556 elif hasattr(self.functor,'_function_apply'): 557 # The functor defines its own function application behaviour 558 self.argument.beta_reduce(*args, **kwargs) 559 result = self.functor._function_apply(self.argument) 560 if result is None: 561 # Function application gave up: this means we're 562 # in beta normal form already 563 return self 564 parent = self.parent 565 self.replace_in_parent(result) 566 567 # The new thing we've just put into our parent might not 568 # yet be in BNF 569 return result.beta_reduce(*args, **kwargs) 570 else: 571 ## Otherwise, just beta-convert the constituents 572 # Functor already done 573 self.argument.beta_reduce(*args, **kwargs) 574 return self
575
576 - def substitute(self, source_variable, target_expression):
577 try: 578 self.functor.substitute(source_variable,target_expression) 579 self.argument.substitute(source_variable,target_expression) 580 except ValueError, err: 581 raise ValueError, "%s. Within: %s" % (err, self)
582
583 - def replace_immediate_constituent(self, old_lf, new_lf):
584 if self.functor is old_lf: 585 old_functor = self.functor 586 self.functor = new_lf 587 new_lf.parent = self 588 # Make sure the old functor is now orphaned 589 old_functor.parent = None 590 if self.argument is old_lf: 591 old_argument = self.argument 592 self.argument = new_lf 593 new_lf.parent = self 594 # Make sure the old argument is now orphaned 595 old_argument.parent = None
596
597 - def get_variables(self):
598 return list(set(self.functor.get_variables() + self.argument.get_variables()))
599
600 - def get_bound_variables(self):
601 vars = [] 602 vars.extend(self.functor.get_bound_variables()) 603 vars.extend(self.argument.get_bound_variables()) 604 return vars
605
606 - def __eq__(self, lf):
607 return (type(lf) == type(self)) and \ 608 (self.functor == lf.functor) and \ 609 (self.argument == lf.argument)
610
611 - def alpha_equivalent(self, other, substitution):
612 """ 613 Checks whether self is equal to a LF that can be derived by 614 some variable substitution S into other, where S contains the 615 substitution T given by "substitution". 616 """ 617 # Must both be applications 618 if type(self) != type(other): 619 return False 620 621 # Recursively check equivalence of functor and arg using same substitution 622 return self.functor.alpha_equivalent(other.functor, substitution) \ 623 and self.argument.alpha_equivalent(other.argument, substitution)
624
625 - def _format(self, formatter):
626 """Put together the arguments in a suitable format, using formatter to produce the arguments' output.""" 627 # Special notation for infix operators 628 if isinstance(self.functor, FunctionApplication): 629 # Check whether this is one of the special infix operators 630 operator = self.functor.functor 631 if isinstance(operator, Literal) and operator.name in self.INFIX_OPERATORS: 632 # Output the whole thing as a single binary infix operation 633 arg1 = self.functor.argument 634 arg2 = self.argument 635 operator_name,brackets = self.INFIX_OPERATORS[operator.name] 636 if brackets: 637 return "(%s%s%s)" % (formatter(arg1), operator_name, formatter(arg2)) 638 else: 639 return "%s%s%s" % (formatter(arg1), operator_name, formatter(arg2)) 640 # Not infix: just a normal function app 641 return "(%s %s)" % (formatter(self.functor), formatter(self.argument))
642
643 - def __str__(self):
644 output = self._format(str) 645 return output
646
647 - def to_latex(self):
648 return self._format(lambda x: x.to_latex())
649
650 - def get_children(self):
651 return [self.functor, self.argument]
652
653 -class Terminal(LogicalForm):
654 """ 655 Base class for any logical forms that are atomic: have no children. 656 This overrides abstract classes that will always have the same 657 behaviour for terminals. 658 659 """
660 - def alpha_convert(self, source_var, target_var):
661 """Alpha-converting a terminal does nothing.""" 662 return
663
664 - def beta_reduce(self, *args, **kwargs):
665 """Beta-converting a terminal does nothing.""" 666 return self
667
668 - def substitute(self, source_variable, target_expression):
669 """There are no variables in a terminal, so this does nothing.""" 670 return
671
672 - def replace_immediate_constituent(self, old_lf, new_lf):
673 """A terminal has no constituents, so this does nothing.""" 674 return
675
676 - def get_variables(self):
677 """No variables in a terminal.""" 678 return []
679
680 - def get_bound_variables(self):
681 """No variables in a terminal.""" 682 return []
683
684 - def get_children(self):
685 """No children of a terminal.""" 686 return []
687
688 - def alpha_equivalent(self, other, substitution):
689 """ 690 Checks whether self is equal to a LF that can be derived by 691 some variable substitution S into other, where S contains the 692 substitution T given by "substitution". 693 694 Substitution has no effect on a terminal, so they're only 695 alpha-equivalent if they're equal. 696 697 """ 698 return self == other
699
700 -class Literal(Terminal):
701 """ 702 Represents any literal that is used in a semantic 703 expression. These are the predicates that are glued 704 together using lambda expressions. 705 706 """ 707
708 - def __init__(self, name):
709 """Builds a basic logical form object for a literal. 710 711 """ 712 super(Literal, self).__init__() 713 self.name = name
714
715 - def copy(self):
716 return type(self)(copy.copy(self.name))
717
718 - def __eq__(self, lf):
719 ## Check this is the same literal 720 return type(lf) == type(self) and lf.name == self.name
721
722 - def __str__(self):
723 output = self.name 724 return output
725
726 - def to_latex(self):
727 output = self.name 728 return output
729
730 -class DummyLogicalForm(LogicalForm):
731 """ 732 A logical form that doesn't really represent anything, but 733 implements the full interface of LogicalForm. You shouldn't 734 use this class or even subclass it, as it essentially just bypasses 735 the interface's requirements on subclasses. 736 737 It's useful for getting a formalism off the ground before you've 738 got as far as implementing the semantics. 739 740 """
741 - def alpha_convert(self, *args):
742 pass
743
744 - def beta_reduce(self, *args, **kwargs):
745 return self
746
747 - def substitute(self, *args):
748 pass
749
750 - def replace_immediate_constituent(self, old, new):
751 pass
752
753 - def get_variables(self):
754 return []
755
756 - def get_bound_variables(self):
757 return []
758
759 - def get_children(self):
760 return []
761
762 - def alpha_equivalent(self, other, substitution):
763 return self == other
764
765 - def __eq__(self, other):
766 return type(self) == type(other)
767
768 - def copy(self):
769 return type(self)()
770
771 - def __str__(self):
772 return "<Dummy>"
773
774 -def multi_apply(application, fun, arg, *args):
775 """ 776 Given a function application class, uses it to produce the curried 777 application of multiple arguments. 778 """ 779 leftapp = application(fun, arg) 780 for next_arg in args: 781 leftapp = application(leftapp, next_arg) 782 return leftapp
783
784 -def multi_abstract(abstraction, arg0, arg1, *args):
785 """ 786 Given a lambda abstraction class, uses it to produce the nested 787 abstraction over any number of variables. 788 """ 789 # Work backwards through the arguments, using the last one as the 790 # expression and all others as abstracted variables 791 all_args = list(reversed([arg0, arg1]+list(args))) 792 expr = all_args[0] 793 vars = all_args[1:] 794 # Abstract over each variable in turn, backwards 795 for var in vars: 796 expr = abstraction(var, expr) 797 return expr
798 799 ########################################## 800 ### Utility functions ### 801 ########################################## 802
803 -def distinguish_variables(sem1, sem2, semantics=True):
804 """ 805 Utility method. Given two instances of Semantics, check to 806 make sure they have no common variable names and renames them 807 if there are any. 808 Modifies the object in situ. 809 The semantics flag indicates that the arguments are within 810 a Semantics object. 811 812 """ 813 if semantics: 814 sem1 = sem1.lf 815 sem2 = sem2.lf 816 vars1 = set(sem1.get_variables()) 817 vars2 = set(sem2.get_variables()) 818 all_vars = vars1 | vars2 819 intersection = vars1 & vars2 820 # Replace each variable that appears in both 821 for var in intersection: 822 # Find a variable name not used in the second lf or the first 823 new_var = next_unused_variable(var, list(all_vars)) 824 # Use alpha-conversion to rename the variable 825 sem1.alpha_convert(var.copy(),new_var) 826 all_vars.add(new_var)
827
828 -def next_unused_variable(start_var, var_list):
829 """ 830 Returns an altered version of the start_var to represent 831 a new variable such that it is not equal to the original 832 value and is not in the var_list 833 834 """ 835 new_var = start_var.copy() 836 new_var.index = 0 837 # Check whether this variable name is used already 838 while new_var in var_list: 839 # Try incrementing the index if it is 840 new_var.index += 1 841 return new_var
842