• API
• FAQ
• Tools
• Archive
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.

Top