View file src/slc/pl.py - Download
# Proof Logic
# Proof =
# - ('SMB', s)
# - ('ANY')
# - ('VAR')
# - ('NXV', x)
# - ('FNC', x)
# - ('APL', x, y)
# - ('GTR', x, y)
# - ('EQU', x, y)
# - ('RLR', x, y)
# - ('RED', x, y)
# (...)
full_red = False
orig_reduce1 = False
def equal(x, y):
if x == y: return True
if not x: return False
if not y: return False
if len(x) != len(y): return False
for i in range(len(x)):
if x[i] != y[i]: return False
return True
def shift(u, x):
if equal(x, u):
return ('NXV', x)
if (not x):
return x
if x[0] == 'SMB': return x
if x[0] == 'ANY': return x
if x[0] == 'VAR': return x
if x[0] == 'FNC': return ('FNC', shift(('NXV', u), x[1]))
if (len(x) < 3): return (x[0], shift(u, x[1]))
return (x[0], shift(u, x[1]), shift(u, x[2]))
def subst(u, a, b):
if equal(u, a): return b
if (not a): return a
if a[0] == 'NXV' and equal(a[1], u): return u
if a[0] == 'SMB' or a[0] == 'VAR' or a[0] == 'ANY': return a
if a[0] == 'FNC': return ('FNC', subst(('NXV', u), a[1], shift(('VAR',), b)))
if len(a) < 3: return (a[0], subst(u, a[1], b))
return (a[0], subst(u, a[1], b), subst(u, a[2], b))
# x contains y ?
def cont(x, y):
if equal(x, y): return True
if not x: return False
if x[0] == 'SMB' or x[0] == 'VAR' or x[0] == 'ANY': return False
if len(x) < 3: return cont(x[1], y)
return cont(x[1], y) or cont(x[2], y)
def contsp(x, y):
if cont(x, y): return True
if full_red: return False
if not x: return False
if not y: return False
if x[0] != y[0]: return False
if len(x) < 2:
x1 = None
x2 = None
elif len(x) == 2:
x1 = x[1]
x2 = None
else:
x1 = x[1]
x2 = x[2]
if len(y) < 2:
y1 = None
y2 = None
elif len(y) == 2:
y1 = y[1]
y2 = None
else:
y1 = y[1]
y2 = y[2]
return contsp(x1, y1) and contsp(x2, y2)
def reduce1(x):
if not x: return x
if x[0] == 'SMB': return x
if x[0] == 'ANY': return x
if x[0] == 'VAR': return x
if x[0] == 'APL' and x[1][0] == 'FNC': return subst(('VAR',), x[1][1], x[2])
if x[0] == 'FNC' and x[1][0] == 'APL' and x[1][2][0] == 'VAR': return x[1][1]
if len(x) < 3: return (x[0], reduce1(x[1]))
return (x[0], reduce1(x[1]), reduce1(x[2]))
MAX = 10000
def reduce2(x):
if not x: return x
a = []
n = 0
y = x
while True:
n += 1
a.append(y)
z = reduce1(y)
if n >= MAX: break
found = False
for a1 in a:
if contsp(z, a1):
found = True
break
if found: return y
y = z
return z
def reduce(x):
return reduce2(x)
def eq(x, y):
return equal(x, y)
def eqr(x, y):
return eq(x, y) or eq(x, reduce(y)) or eq(reduce(x), y) or eq(reduce(x), reduce(y))
def sides(x):
if not x: return (None, None)
if x[0] == 'SMB' or x[0] == 'ANY' or x[0] == 'VAR': return (x, x)
if x[0] == 'EQU': return (x[1], x[2])
if x[0] == 'RED': return sides(reduce(x[1]))
if x[0] == 'RLR':
lr = sides(x[1])
return (reduce(lr[0]), reduce(lr[1]))
if x[0] == 'GTR':
lr1 = sides(x[1])
l1 = lr1[0]
r1 = lr1[1]
lr2 = sides(x[2])
l2 = lr2[0]
r2 = lr2[1]
if eqr(l1, l2): return (r1, r2)
if eqr(r1, l2): return (l1, r2)
if eqr(l1, r2): return (r1, l2)
if eqr(r1, r2): return (l1, l2)
return (x, x)
lr1 = sides(x[1])
if len(x) < 3:
return ((x[0], lr1[0]), (x[0], lr1[1]))
lr2 = sides(x[2])
return ((x[0], lr1[0], lr2[0]), (x[0], lr1[1], lr2[1]))
def left(x):
return sides(x)[0]
def right(x):
return sides(x)[1]
def abstr(u, v, x):
if equal(v, x): return u
if not cont(x, v): return x
if not x: return x
if x[0] == 'FNC': return ('FNC', abstr(('NXV', u), v, x[1]))
if len(x) < 2:
return (x[0],)
if len(x) == 2:
return (x[0], abstr(u, v, x[1]))
return (x[0], abstr(u, v, x[1]), abstr(u, v, x[2]))
def pllambda(v, x):
if x[0] == 'APL' and equal(x[2], v) and not cont(x[1], v): return x[1]
return ('FNC', abstr(('VAR',), v, x))
def string_of_proof(x):
if x[0] == 'SMB': return x[1]
if x[0] == 'ANY': return '_'
if x[0] == 'VAR': return '*'
if x[0] == 'NXV': return "'" + string_of_proof(x[1])
if x[0] == 'FNC': return '[' + string_of_proof(x[1]) + ']'
if x[0] == 'APL': return '(' + string_of_proof(x[1]) + ' ' + string_of_proof(x[2]) + ')'
if x[0] == 'GTR': return '(' + string_of_proof(x[1]) + ' ; ' + string_of_proof(x[2]) + ')'
if x[0] == 'EQU': return '(' + string_of_proof(x[1]) + ' = ' + string_of_proof(x[2]) + ')'
if x[0] == 'RED': return '@' + string_of_proof(x[1])
if x[0] == 'RLR': return '$' + string_of_proof(x[1])
if x[0] == 'AXM': return f"AXM{x[1]}"
return '?'
def deduce(x):
concl = sides(x)
print('The proof')
print(' ' + string_of_proof(x))
print('proves')
print(' ' + string_of_proof(concl[0]))
print('equals')
print(' ' + string_of_proof(concl[1]))
return concl
DI = ('EQU', ('SMB', 'I'), pllambda(('SMB', 'a'), ('SMB', 'a')))
DK = ('EQU', ('SMB', 'K'), pllambda(('SMB', 'a'), pllambda(('SMB', 'b'), ('SMB', 'a'))))
DS = ('EQU', ('SMB', 'S'), pllambda(('SMB', 'a'), pllambda(('SMB', 'b'), pllambda(('SMB', 'c'), ('APL', ('APL', ('SMB', 'a'), ('SMB', 'c')), ('APL', ('SMB', 'b'), ('SMB', 'c')))))))
SKKI = ('GTR', ('APL', ('APL', DS, DK), DK), DI)
sides(SKKI)
deduce(SKKI)
ext = ('GTR', ('APL', ('APL', DS, ('APL', DK, ('SMB', 'x'))), ('APL', DK, ('SMB', 'y'))), ('APL', DK, ('APL', ('SMB', 'x'), ('SMB', 'y'))))
print(sides(ext))
deduce(ext)
def ap(f, x):
return ('APL', f, x)
def ap2(f, x, y):
return ap(ap(f, x), y)
def ap3(f, x, y, z):
return ap(ap(ap(f, x), y), z)
def gtr(x, y):
return ('GTR', x, y)
def equ(x, y):
return ('EQU', x, y)
def rlr(x):
return ('RLR', x)
I = ('FNC', ('VAR',))
x = ('SMB', 'x')
y = ('SMB', 'y')
z = ('SMB', 'z')
parent = ('SMB', 'parent')
grandparent = ('SMB', 'grandparent')
allan = ('SMB', 'allan')
brenda = ('SMB', 'brenda')
charles = ('SMB', 'charles')
gpRule1 = pllambda(x, pllambda(y, pllambda(z, equ(ap(ap2(parent, x, y), ap(ap2(parent, y, z), ap2(grandparent, x, z))), I))))
gpAxiom1 = equ(ap2(parent, allan, brenda), I)
gpAxiom2 = equ(ap2(parent, brenda, charles), I)
gpTheorem1 = rlr(gtr (ap2(grandparent,allan,charles),
gtr (ap(gpAxiom2,ap2(grandparent,allan,charles)),
gtr (ap(gpAxiom1,ap(ap2(parent,brenda,charles),ap2(grandparent,allan,charles))),
ap3(gpRule1,allan,brenda,charles)))))
print(sides(gpTheorem1))
deduce(gpTheorem1)
axm1 = ('EQU', ('SMB', 'a'), ('SMB', 'b'))
axm2 = ('EQU', ('SMB', 'b'), ('SMB', 'c'))
ops = ['ANY', 'VAR', 'NXV', 'FNC', 'APL', 'GTR', 'RLR', 'RED']
#smbs = ['a', 'b', 'c']
#axms = [DI, DK, DS]
smbs = ['a', 'b', 'c']
axms = [axm1, axm2]
# def num_op(op):
# if op in ops: return ops.index(op) + 1
# return 0
arities = {
'SMB': 0,
'ANY': 0,
'VAR': 0,
'NXV': 1,
'FNC': 1,
'APL': 2,
'GTR': 2,
'EQU': 2,
'RLR': 1,
'RED': 1,
'AXM': 0,
}
def dict_of_proof_1(x, dict, start, step):
if x[0] == 'SMB':
if x[1] in smbs:
dict[start] = 1 + len(ops) + smbs.index(x[1])
else:
dict[start] = 0
elif x[0] == 'AXM':
dict[start] = 1 + len(ops) + len(smbs) + x[1]
elif x[0] in ops:
dict[start] = 1 + ops.index(x[0])
else:
dict[start] = 0
if arities[x[0]] > 0:
dict_of_proof_1(x[1], dict, start+step, step*2)
if arities[x[0]] > 1:
dict_of_proof_1(x[2], dict, start+2*step, step*2)
def dict_of_proof(x):
dict = {}
dict_of_proof_1(x, dict, 0, 1)
return dict
def proof_of_dict_1(dict, start, step):
numop = dict[start]
if numop == 0 or numop >= 1+len(ops)+len(smbs)+len(axms):
return None
if numop >= 1+len(ops)+len(smbs):
# return ('AXM', numop-1-len(ops)-len(smbs)
return axms[numop-1-len(ops)-len(smbs)]
if numop >= 1+len(ops):
return ('SMB', smbs[numop-1-len(ops)])
op = ops[numop-1]
if arities[op] < 1:
return (op,)
y = proof_of_dict_1(dict, start+step, step*2)
if arities[op] < 2:
return (op, y)
z = proof_of_dict_1(dict, start+2*step, step*2)
return (op, y, z)
def proof_of_dict(dict):
return proof_of_dict_1(dict, 0, 1)
print(proof_of_dict(dict_of_proof(('APL',('APL',('VAR',),('VAR',)),('VAR',)))))
print(proof_of_dict(dict_of_proof(('AXM',1))))
import random
random.seed(32)
def random_proof():
opnum = random.randrange(len(ops)+len(smbs)+len(axms))
if opnum >= len(ops)+len(smbs):
return ('AXM', opnum-len(ops)-len(smbs))
if opnum >= len(ops):
return ('SMB', smbs[opnum-len(ops)])
op = ops[opnum]
if arities[op] < 1:
return (op,)
y = random_proof()
if arities[op] < 2:
return (op, y)
z = random_proof()
return (op, y, z)
def subst_axm(x):
op = x[0]
if op == 'AXM':
return axms[x[1]]
if op == 'SMB':
return x
if arities[op] < 1:
return (op,)
y = subst_axm(x[1])
if arities[op] < 2:
return (op, y)
z = subst_axm(x[2])
return (op, y, z)
def prove(a, b):
#print("Random proofs:")
random.seed(32)
for i in range(100000):
x = random_proof()
y = subst_axm(x)
concl = sides(y)
if equal(concl[0], a) and equal(concl[1], b):
print("---------------------------------------------------------------------")
print(i)
print(x)
print(y)
deduce(y)
break
a = ('SMB', 'a')
b = ('SMB', 'b')
c = ('SMB', 'c')
prove(('SMB', 'a'), ('SMB', 'a'))
prove(('SMB', 'b'), ('SMB', 'b'))
prove(('SMB', 'c'), ('SMB', 'c'))
prove(('SMB', 'a'), ('SMB', 'b'))
prove(('SMB', 'b'), ('SMB', 'a'))
prove(('SMB', 'b'), ('SMB', 'c'))
prove(('SMB', 'c'), ('SMB', 'b'))
prove(('SMB', 'a'), ('SMB', 'c'))
prove(('SMB', 'c'), ('SMB', 'a'))
#prove(('APL', ('SMB', 'a'), ('SMB', 'b')), ('APL', ('SMB', 'a'), ('SMB', 'c')))
prove(ap(a, b), ap(a, c))
prove(ap(a, c), ap(c, a))
prove(ap(b, a), ap(b, c))
prove(ap(b, c), ap(b, a))
def dict_of_list(l):
dict = {}
for i in range(len(l)):
dict[i] = l[i]
return dict
def list_of_dict(dict):
m = max(dict.keys())
l = [0 for i in range(m+1)]
for i, x in dict.items():
l[i] = x
return l
def proofs_of_size(n):
proofs = []
for op in ops:
if arities[op] == 0:
proofs.append((op,))
for s in smbs:
proofs.append(('SMB', s))
for i in range(len(axms)):
proofs.append(('AXM', i))
if n > 0:
proofs1 = proofs_of_size(n-1)
for x in proofs1:
for op in ops:
if arities[op] == 1:
proofs.append((op, x))
for y in proofs1:
for op in ops:
if arities[op] == 2:
proofs.append((op, x, y))
return proofs
for x in proofs_of_size(1):
print(string_of_proof(x))
def f2(p2, y):
f = p2[0]
p = p2[1]
x = p2[2]
for op in ops:
if arities[op] == 2:
f(p, (op, x, y))
def f1(p1, x):
f = p1[0]
p = p1[1]
n = p1[2]
for op in ops:
if arities[op] == 1:
f(p, (op, x))
treat_proofs_of_size(n, f2, (f, p, x))
def treat_proofs_of_size(n, f, p):
for op in ops:
if arities[op] == 0:
f(p, (op,))
for s in smbs:
f(p, ('SMB', s))
for i in range(len(axms)):
f(p, ('AXM', i))
if n > 0:
treat_proofs_of_size(n-1, f1, (f, p, n-1))
def f(p, x):
print(string_of_proof(x))
print("")
treat_proofs_of_size(0, f, 0)
l = []
def fa(p, x):
l.append(x)
treat_proofs_of_size(1, fa, 0)
print("")
for x in l:
print(string_of_proof(x))