# 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,

```python
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&#x20;

order of values in streams doesn't matter, we may end up in:

<img src="https://4206299962-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2Fxq51GRrexLVjjzJzwwLp%2Fuploads%2Fg9XLJI37bB55sbjQfCrQ%2Ffile.excalidraw.svg?alt=media&#x26;token=83cfffe3-be72-4eb3-aa1e-241cb5a8889b" alt="" class="gitbook-drawing">

Other, more nuanced implementations perform interleaving...

other changes:

```python
        
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:&#x20;

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:&#x20;

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

```python
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.

```python
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!


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://arnav-1.gitbook.io/15-113-lecture-notes/infinite-streams-and-negations.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.