1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
from lambda_calculus import Variable, Abstraction, Application
from lambda_calculus.visitors.normalisation import BetaNormalisingVisitor
import networkx as nx
import sys
import itertools
S = Abstraction('x',
Abstraction('y',
Abstraction('z',
Application(Application(Variable('x'), Variable('z')),
Application(Variable('y'), Variable('z'))))))
K = Abstraction('x',
Abstraction('y',
Variable('x')))
class Node(object):
def __init__(self, left, right):
self.left = left
self.right = right
def __repr__(self):
return '(%s %s)' % (self.left if isinstance(self.left, Node) else self.left[1], self.right if isinstance(self.right, Node) else self.right[1])
def app(self):
return Application(
self.left.app() if isinstance(self.left, Node) else self.left[0],
self.right.app() if isinstance(self.right, Node) else self.right[0])
# Given a tree and a label, yields every possible augmentation of the tree by
# adding a new node with the label as a child "above" some existing Node or Leaf.
def add_leaf(tree, label):
yield Node(label, tree)
if isinstance(tree, Node):
for left in add_leaf(tree.left, label):
yield Node(left, tree.right)
for right in add_leaf(tree.right, label):
yield Node(tree.left, right)
# Given a list of labels, yield each rooted, unordered full binary tree with
# the specified labels.
def enum_unordered(labels):
if len(labels) == 1:
yield labels[0]
else:
for tree in enum_unordered(labels[1:]):
for new_tree in add_leaf(tree, labels[0]):
yield new_tree
def enum_ordered(labels):
if len(labels) == 1:
yield labels[0]
else:
for i in range(1, len(labels)):
for left in enum_ordered(labels[:i]):
for right in enum_ordered(labels[i:]):
yield Node(left, right)
# def count(n,elements):
# l = len(elements)
# def Convert(n,base):
# string = elements
# if n < base:
# return [string[n]]
# else:
# return Convert(n//base,base) + [string[n%base]]
# return (Convert(i,l) for i in range(0,l**n+1))
sys.setrecursionlimit(1000)
all_products = lambda *args, repeat:itertools.chain(*(itertools.product(*args, repeat=n) for n in range(1,repeat+1)))
g = nx.Graph()
for term in all_products([(S,'S'), (K,'K')], repeat=5):
for parensed in enum_ordered(term):
try:
beta = BetaNormalisingVisitor().skip_intermediate(
parensed.app() if isinstance(parensed, Node) else parensed[0]
)
g.add_edge(repr(parensed) if isinstance(parensed, Node) else parensed[1], str(beta))
except:
print(str(beta), "cant be reduced")
pass
import matplotlib.pyplot as plt
# # nx.nx_pydot.write_dot(g, 'out.dot')
nx.draw(g, with_labels=True)
plt.show()
# for n1 in [S,K]:
# for n2 in [S,K]:
# for n3 in [S,K]:
# # for n4 in [S,K]:
# for term in enum_ordered([n1,n2,n3]):
# beta = BetaNormalisingVisitor().skip_intermediate(term)
# if beta.body == Variable(beta.bound):
# print(str(term), 'reduces to identity')
|
