Infinite Streams and Negations

Finite streams are rare. Here is an example:

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:

1. is the empty list

2. a pair whose last element is a stream

3. 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!