Consider we have the goal (we will write it later) not_eq...
Then: not_eq(x, 3){dict()}: x can be EVERYTHING except any object that reduces to 3
This is an example of a goal that produces an infinite stream. We therefore we have revise our definition of a stream:
A stream:
is the empty list
a pair whose last element is a stream
a suspension: an anonymous function that returns a stream
So, the stream representation of not_eq(x, 3)(dict()) is:
[{x:4},<stream−generator−fn>]
Given this new definition of streams, we need to modify some functions. Specifically,
def take_inf(n, subst_stream, res): # res must be empty
if n == 0: # unchanged
return res
elif len(subst_stream) == 0: # unchanged
return res
elif callable(subst_stream[0]): # checks if the currrent element is a generator
print(f"when called, the generator gives {subst_stream[0]()}")
return take_inf(n, subst_stream[0](), res) # change the list being looked at
elif isinstance(subst_stream[0],dict): # unchanged
res.append(subst_stream[0])
return take_inf(n-1, subst_stream[1:], res)
OK, admittedly, this causes certain hard-to-avoid problems:
Let's say I want to specifically extract substitution for u from a random stream. Since
order of values in streams doesn't matter, we may end up in:
Other, more nuanced implementations perform interleaving...
other changes:
def append_map_inf(goal, subst_stream, res): # why did using the empty argument not work?
#print(subst_stream)
if len(subst_stream) == 0:
return res
#print(f"the appended subst is: {goal(subst_stream.pop())}")
#assert(False)
if isinstance(subst_stream[0],dict):
res.extend(goal(subst_stream[0]))
elif callable(subst_stream[0]):
stream = subst_stream[0]() # call the suspension to yield stream
res.append(lambda: append_map_inf(goal, stream, list())) # creating a new suspension from the original suspension
return append_map_inf(goal, subst_stream[1:], res)
append_inf sees no changes
Interestingly, we do not change eq_eq and unify. Why?
TO DEAL WITH ANOTHER LIMITATION:
So, it is not possible to prove logical equivalence with basic tools like these.
So, we don't need to change eq_eq and unify.
ONTO NEGATION:
This too is very difficult to implement purely, because of the problems posed by infinite streams. We have a very crude, hacky, unintellectual implementation.
We will not explain this, it is dumb and stupid code...
def run_expn(n, q, args):
mask = f"run({str(n)}, {q.id}, " # evaluation mask
# print(f"expn is now {args}")
neg_count = args.count("negate")
if neg_count == 0: # nothing to negate, return args
return args
ind = args.find("negate") # ew
before = args[0:ind] # everything before the first negate is unchanged
bef_count = before.count("(") # stores number of "(" occuring before first negate discovered
fin_wrap, fin = construct_wrap(before, bef_count, args, ind)
num_goals = len(perform_split(fin))
fin_wrap = add_unknowns(fin_wrap, num_goals)
# print(after)
ans = fin_wrap
if num_goals > 1:
l = perform_split(fin) # produces some independent goals list
for _ in range(len(l)):
l[_] = run_expn(n, q, l[_])
for _ in range(len(l)):
ans = ans.replace("*",l[_],1)
else:
l = list()
#l.append(fin[0:fin.index("(")])
the_arg = fin[fin.index("(")+1:-1]
l.append(the_arg[0:the_arg.index("(")])
l.extend(perform_split(the_arg[the_arg.index("(")+1:-1]))
match l:
case["conj",*args]:
after = "disj("
for arg in args:
after += f"negate({arg}),"
after = after[0:-1]
rep = run_expn(n, q, after + ")")
ans = ans.replace("*",rep)
case["disj",*args]:
after = "conj("
for arg in args:
after += f"negate({arg}),"
after = after[0:-1]
rep = run_expn(n, q, after + ")")
ans = ans.replace("*",rep)
case["negate",arg]:
rep = run_expn(n, q, arg)
ans = ans.replace("*",rep)
case["eq_eq",arg1,arg2]:
rep = run_expn(n, q, f"not_eq({arg1},{arg2})")
ans = ans.replace("*",rep)
case["not_eq",arg1,arg2]:
rep = run_expn(n, q, f"eq_eq({arg1},{arg2})")
ans = ans.replace("*",rep)
case _:
print("oops!")
return ans
def is_np(ind, strng):
after, before = 0, 0
for j in range(ind + 1, len(strng)):
if strng[j] == ')':
after += 1
elif strng[j] == "(":
after -= 1
for j in range(ind):
if strng[j] == '(':
before += 1
elif strng[j] == ')':
before -= 1
return (after == 0 and before == 0)
return True
def perform_split(i_str):
res = list()
loc_str = ""
i_str += ","
for _ in range(len(i_str)):
# if _ == (len(i_str) - 1):
# res.append(loc_str)
if not (i_str[_] == ',' and is_np(_, i_str)):
loc_str += i_str[_]
else:
res.append(loc_str)
loc_str = ""
return res
""" def get_bef_count(ind, args):
res = 0
for _ in range(ind):
if args[_] == "(":
res += 1
return res """
def construct_wrap(before, bef_count, args, ind): # before is the stuff before the negate
# bef_count: no. of open parens before the first "negate"
# args: the whole string to be evaluated
# index: the first index of negate
res = ""
start = len(args)
count = 0
while (count < bef_count):
start -= 1
if args[start] == ")":
count += 1
res = args[start] + res #
fin = args[ind:start]
res = before + res
return res, fin
def add_unknowns(fin_wrap, num_goals):
ind = fin_wrap.find("()") + 1
temp = list(fin_wrap)
added = ""
for _ in range(num_goals):
added += "*,"
temp.insert(ind, added[:-1])
return "".join(temp)
When we meet the base case of not_eq(u, 3)({}), we essentially try to "disunify" u with respect to 3. u can "technically" be mapped to any value, but we will stick to ints through the following not-equaliser.
def not_equaliser(t1,t2):
# 0 pairs
# one is var
# set var to random till not equal to constant
# both are var
# set both to random till unequal
# 1 pair
# we will decide to return unequal values of the same type
# use 0 pair base case for each elem
# 2 pairs
# use 0 pair base case for each elem
if var_huh(t1) or var_huh(t2):
if var_huh(t1):
t1 = random.randint(-1 * max_size, max_size)
if var_huh(t2):
t2 = random.randint(-1 * max_size, max_size)
if (t1 == t2):
not_equaliser(t1, t2) # do again if still equal
else:
return t1, t2
Feel free to run the tool on reasonable examples of your choice!
