SHARE
TWEET

Untitled

a guest Jun 26th, 2019 63 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. import itertools
  2.  
  3.  
  4. class LambdaTerm:
  5.     """Abstract base class for lambda terms."""
  6.  
  7.     def __eq__(self, other): #tests if given lambda Terms are alpha-equivalent after beta-reduction
  8.         def full_sub(sub, substr, perm): #sub denotes list of symbols in str to be subsituted, substr denotes said string, perm denotes what the symbols are to be substituted with
  9.             mal = [0]*(len(substr))
  10.             newstr = ''
  11.             for i in range(0, len(substr)):
  12.                 if substr[i] in ['(', ')', '@', 'λ', '\\', '.', ' ']:
  13.                     mal[i]=substr[i]
  14.             for i in range(0, len(perm)):
  15.                 for k in range(0, len(substr)):
  16.                     if substr[k] == sub[i]:
  17.                         mal[k] = perm[i]
  18.             for i in range(0, len(mal)):
  19.                 newstr += str(mal[i])
  20.             return newstr
  21.         alpha_eq=False
  22.         self=self.reduce()
  23.         other=other.reduce()
  24.         if type(self) == type(other):
  25.             #try permutations
  26.             selfstr=str(self)
  27.             otherstr=str(other)
  28.             selfsyms = []
  29.             othersyms = []
  30.             for i in range(0, len(selfstr)):
  31.                 if selfstr[i] not in selfsyms and selfstr[i] not in ['(', ')', '@', 'λ', '\\', '.', ' ']:
  32.                     selfsyms.append(selfstr[i])
  33.             for i in range(0, len(otherstr)):
  34.                 if otherstr[i] not in othersyms and otherstr[i] not in ['(', ')', '@', 'λ', '\\', '.', ' ']:
  35.                     othersyms.append(otherstr[i])
  36.             if len(selfsyms) == len(othersyms):
  37.                 permstocheck = list(itertools.permutations(selfsyms))
  38.                 for i in range(0, len(permstocheck)):
  39.                     if selfstr == full_sub(othersyms, otherstr, permstocheck[i]):
  40.                         alpha_eq = True
  41.                         break
  42.         return alpha_eq
  43.  
  44.     def fromstring(self):
  45.         """Construct a lambda term from a string."""
  46.         self=self.strip()
  47.        
  48.         def dict_parentheses(string): #makes a dictionary that matches indices of opening parentheses to indices of corresponging closing parentheses.
  49.             istart = []
  50.             parentheses_dict = {}
  51.             for i, c in enumerate(string):
  52.                 if c == '(':
  53.                      istart.append(i)
  54.                 if c == ')':
  55.                     try:
  56.                         parentheses_dict[istart.pop()] = i
  57.                     except IndexError:
  58.                         return 'Error: invalid string, too many closing parentheses'
  59.             if istart:  # check if stack is empty afterwards
  60.                 return 'Error: invalid string, too many opening parentheses'
  61.             return parentheses_dict
  62.        
  63.         haakjes = dict_parentheses(self)
  64.         traverser = 0
  65.         #start Term.
  66.         if self[0] not in ['(', '@', 'λ', ')', '\\']: #found a variable.
  67.             Term = Variable(self[0])
  68.             traverser += 1
  69.         elif self[0] == '(': #evaluate Term within parentheses.
  70.             Term = LambdaTerm.fromstring(self[1:haakjes[0]])
  71.             traverser = haakjes[0]+1
  72.         else: #@ or λ can only be encountered at start of string, thus
  73.             Term = Abstraction(Variable(self[1]), LambdaTerm.fromstring(self[3:]))
  74.             traverser = len(self)
  75.         while traverser < len(self):
  76.             if self[traverser] not in ['(', '@', 'λ', ')', ' ', '\\']: #found a variable.
  77.                 Term = Application(Term, Variable(self[traverser]))
  78.                 traverser+=1
  79.             elif self[traverser] == '(': #evaluate term in parentheses
  80.                 Term = Application(Term, LambdaTerm.fromstring(self[traverser+1:haakjes[traverser]]))
  81.                 traverser=haakjes[traverser]+1
  82.             elif self[traverser] == ' ':
  83.                 traverser += 1
  84.             else: return "illegal string"  #@ or λ can only be encountered at start of string.
  85.         return Term
  86.  
  87.  
  88.     def reduce(self):
  89.         """Automatically runs the correct reduction function when reduce() is called from LambdaTerm"""
  90.         if isinstance (self, Variable):
  91.             return Variable.reduce(self)
  92.         elif isinstance (self, Abstraction):
  93.             return Abstraction.reduce(self)
  94.         else:
  95.             return Application.reduce(self)
  96.  
  97.  
  98.  
  99. class Variable(LambdaTerm):
  100.     """Represents a variable."""
  101.     def __init__(self, symbol):
  102.         self.symbol = symbol
  103.     def __repr__(self):
  104.         return 'Variable('+repr(self.symbol)+')'
  105.     def __str__(self):
  106.         return str(self.symbol)
  107.     def substitute(self, rules):
  108.         #let rules always be given in format [a, b] where a is the variable that should be replaced by lambdaterm b.
  109.         if self.symbol == rules[0].symbol:
  110.             return rules[1]
  111.         return self
  112.     def reduce(self):   #extra function to stop recursive reduction when recurson of Application reaches this class
  113.         return self
  114.  
  115. class Abstraction(LambdaTerm):
  116.     """Represents a lambda term of the form (λx.M)."""
  117.  
  118.     def __init__(self, variable, body):
  119.         self.variable = variable
  120.         self.body = body
  121.     def __repr__(self):
  122.         return "Abstraction("+repr(self.variable)+', '+repr(self.body)+')'
  123.     def __str__(self):
  124.         return 'λ'+str(self.variable)+'.'+str(self.body)
  125.     def __call__(self, argument):
  126.         copy = self
  127.         return Application(copy, argument).reduce()
  128.     def substitute(self, rules): #given new variable should never collide with bound variable! also, we assume that variable in self.variable is immutable
  129.         z = self.body.substitute(rules)
  130.         return Abstraction(self.variable, z)
  131.     def reduce(self):   #extra function to facilitate recursive reduction when recurson of Application encounters this class
  132.         self.body=self.body.reduce()
  133.         return self
  134.  
  135. class Application(LambdaTerm):
  136.     """Represents a lambda term of the form (M N)."""
  137.  
  138.     def __init__(self, function, argument): #Implementeer Alfa-conversie om name collisions te voorkomen
  139.         self.function = function
  140.         self.argument = argument
  141.     def __repr__(self):
  142.         return 'Application('+repr(self.function)+', '+repr(self.argument)+')'
  143.     def __str__(self):
  144.         if type(self.function) == Abstraction: a = '('+str(self.function)+')'
  145.         if type(self.function) == Application: a = str(self.function)
  146.         if type(self.function) == Variable: a = str(self.function)
  147.         if type(self.argument) == Abstraction: b = '('+str(self.argument)+')'
  148.         if type(self.argument) == Application: b = str(self.argument)
  149.         if type(self.argument) == Variable: b = str(self.argument)
  150.         return a+b
  151.     def substitute(self, rules):
  152.         a = self.function.substitute(rules)
  153.         b = self.argument.substitute(rules)
  154.         return Application(a, b)
  155.     def reduce(self):
  156.         if type(self.function) == Abstraction and type(self.argument) == Variable:
  157.             return self.function.body.substitute([self.function.variable, self.argument])
  158.         elif type(self.function) == Abstraction and type(self.argument) == Application:
  159.             self.argument = self.argument.reduce()
  160.             return self.function.body.substitute([self.function.variable, self.argument])
  161.         elif type(self.function) == Variable:
  162.             self.argument = self.argument.reduce()
  163.             return self
  164.         elif type(self.function) == Abstraction and type(self.argument) == Abstraction:
  165.             z = self.function.body.substitute([self.function.variable, self.argument])
  166.             return z.reduce()
  167.         elif type(self.function) == Application and type(self.argument) != Application:
  168.             self.function=self.function.reduce()
  169.             return self.reduce()
  170.         elif type(self.function) != Application and type(self.argument) == Application:
  171.             self.argument = self.argument.reduce()
  172.         elif type(self.function) == Application and type(self.argument) == Application:
  173.             self.function = self.function.reduce()
  174.             self.argument = self.argument.reduce()
  175.             return self.reduce()
  176.         else:
  177.             return (type(self.function), type(self.argument))
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top