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

99 - def get_ancestor_bound_variables(self):

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

214 - def get_ancestor_bound_variables(self):

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

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