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,
deftake_inf(n,subst_stream,res): # res must be emptyif n ==0:# unchangedreturn reseliflen(subst_stream)==0:# unchangedreturn reselifcallable(subst_stream[0]):# checks if the currrent element is a generatorprint(f"when called, the generator gives {subst_stream[0]()}")returntake_inf(n, subst_stream[0](), res)# change the list being looked atelifisinstance(subst_stream[0],dict):# unchanged res.append(subst_stream[0])returntake_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:
defappend_map_inf(goal,subst_stream,res): # why did using the empty argument not work?#print(subst_stream)iflen(subst_stream)==0:return res#print(f"the appended subst is: {goal(subst_stream.pop())}")#assert(False)ifisinstance(subst_stream[0],dict): res.extend(goal(subst_stream[0]))elifcallable(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
returnappend_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...
defrun_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 argsreturn 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_wrapif num_goals >1: l =perform_split(fin)# produces some independent goals listfor _ inrange(len(l)): l[_]=run_expn(n, q, l[_])for _ inrange(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 ansdefis_np(ind,strng): after, before =0,0for j inrange(ind +1, len(strng)):if strng[j]==')': after +=1elif strng[j]=="(": after -=1for j inrange(ind):if strng[j]=='(': before +=1elif strng[j]==')': before -=1return (after ==0and before ==0)returnTruedefperform_split(i_str): res =list() loc_str ="" i_str +=","for _ inrange(len(i_str)):# if _ == (len(i_str) - 1):# res.append(loc_str)ifnot (i_str[_]==','andis_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 """defconstruct_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 =0while (count < bef_count): start -=1if args[start]==")": count +=1 res = args[start]+ res # fin = args[ind:start] res = before + resreturn res, findefadd_unknowns(fin_wrap,num_goals): ind = fin_wrap.find("()")+1 temp =list(fin_wrap) added =""for _ inrange(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.
defnot_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 elemifvar_huh(t1)orvar_huh(t2):ifvar_huh(t1): t1 = random.randint(-1* max_size, max_size)ifvar_huh(t2): t2 = random.randint(-1* max_size, max_size)if (t1 == t2):not_equaliser(t1, t2)# do again if still equalelse:return t1, t2
Feel free to run the tool on reasonable examples of your choice!