Logic Programming

Initial example, something to solve:

$$((x == 3) \wedge (y == x) \wedge \neg (z == y)) \vee ((v == z)\wedge(z == x)\wedge(y==4))$$

We can patiently assign values and create solutions, or come up with a way to represent the problem's constraints and get the solutions automatically.

In fact, all we need to do is "somehow" translate the example above to this:

the high level idea: the repeated application of goals to substitutions produces the final model(s): for each constraint, extend the substitution until all constraints are satisfied (or fails if no extensions possible in way to satisfying thre goal, considering no change as an "empty extension")

The eq_eq() goal:

Eg: x is a var; eq_eq(x, 3)? default input: the empty substitution (dict()). Use What does it produce? [{x: 3}].

Non-empty substitution? Let it be {x:4}. In this case, a contradiction. Result is [] (our definition of "fail"). This is called (fail). Tautological substitution? Let it be {x:3}. Then, we return success, [substitution] [{x : 3}].

If the goal does not mention variables, it is either contradiction (fail) or a (success). eg: eq_eq(3,3) (success).

The general structure our goals will have is:

def goal_name(*args): # goals can involve multiple args
    def anon(substitution):
        # change substitution based on goal rules to form stream
        return stream
    return anon
    

Why? Because then, calling goal_name(*args)(substitution) -> stream!

Writing eq_eq:

General algorithm: Pretty simple...

def eq_eq(u, v): # only 2 things are possibly equal, a binary relation 
    def anon(s):
        s = unify(u, v, s) # try to produce a new substitution that "equalizes"
                            # u and v given the current substitution
        if s:
            return succeed(s)
        else:
            return fail()
    return anon

Explain post line 3:

What are u and v? They are "terms", which are either constants, or variables (a constant, a variable or a tuple of 2 terms: definition of 2 terms). Here is how we define variables:

class Var:
    def __init__(self):
        self.id = ""

    def __repr__(self):
        return 'var ' + str(self.id)

    def __eq__(self, other):
        return (type(self) == type(other)) and (self.id == other.id)

    def __hash__(self): # we can now use these as dict keys
        return ord(self.id)

def var(name):
    res = Var()
    res.id = name
    return res

Unification:

Naive: Take the goal eq_eq(x, 3). Based on examples we've seen, all I need to do is check if x is mapped to 3 right? WRONG! Substitutions can be more complicated. For example:

Let there be eq_eq(x, 3)({x: w, w: 3}). We need to walk down the substitution and check each key to reach the "root value" of x. That would be 3, and our unification is successful.

def unify(u, v, s):
    u = walk(u, s) # give me the root value of u
    v = walk(v, s) # give me the root value of v
    if equals(u, v): # we are done, 
        return s
    elif isinstance(u, Var) and not occurs(u, v, s): # rem: u is fresh wrt the substitution
        s[u] = v # efectively altering the substitution
        return s
    elif isinstance(v, Var) and not occurs(v, u, s): # rem: v is fresh wrt the substitution
        s[v] = u
        return s
    elif isinstance(u, tuple) and isinstance(v, tuple):
        s = unify(u[0], v[0], s) # perform unification on every element of the tuple
        if (s == False):
            return False
        else:
            return unify(u[1:], v[1:], s)
    else:
        return False

Line 4: Tautology, do nothing to the substitution

Lines 6 and 9: a fresh variable can be assigned to anything (it is thereafter forever mapped within that substitution)

Here is walk:

def walk(v, s):
    if isinstance(v, Var) and (v in s):
        return walk(s[v], s)
    else:
        return v

Line 12 addresses another problem: a "deeper walk". Consider the example:

eq_eq(z, y)({u: 3, v: 4, z: (u, v), y: (3, 4)}). This SHOULD be successfully unified: How?

(Trace through lines 12 through 19 to answer how?)

Line 17: given the substitution for the first value of the tuple, extend the substitution recursively for the remaining values of the tuple

Also draw attention to occurs checks. Why do we do it? To prevent cycles.

(The motivation behind the occurs check is to ensure that given a variable x, to which we are about to assign y, we need to ensure that x is not in y; so if y reduced to a variable in the substitution, all we need to do is ensure that x is not an element of or equal to y).

For perusal of reader:

def occurs(x, y, s):
    y = walk(y, s)
    if var_huh(y):
        if (y == x):
            return True
    elif is_pair(y):
        return (occurs(x, y[0], s) or (occurs(x, y[1:], s)))
    return False

That's all there is to unification (walk is trivial).

The code below is optional functionality, and is for the purpose of reification of solutions.

def run(n, q, goal):
    res = list()
    res_copy = run_goal(n, goal)
    return list(map(reify(q), res_copy)) # reify the values of a particular
                                        # variable of interest using map
    # for _ in range(len(res_copy)):
        # res.append(reify(q)(res_copy[_]))
    # return res
    
def run_goal(n, goal): # simple enough, takes substitutions from goal
    print(goal(empty_s())) 
    # apply goal to default (empty substituion to begin)
    return take_inf(n, goal(empty_s()), list())
    
def take_inf(n, subst_stream, res):
    if n == 0: # n is 0, take nothing from the stream
        return res
    elif len(subst_stream) == 0: # cannot take anything more from stream
        return res
    elif isinstance(subst_stream[0],dict):
        res.append(subst_stream[0])
        return take_inf(n-1, subst_stream[1:], res)

Conjunctions and Disjunctions:

Conjunctions act on goals; (connectives for goals).

Individual extensions on substitutions created by goals are accumulated through conjunction.

A simple strategy for conjunction:

1. 0 arguments? vacuous success

2. 1 argument? the goal : conj(goal) is same as goal

3. 2 arguments? call helper on first goal and conjunction of rest of goals, in the context of the initial stream produced by the first goal

Implementation:

def conj(*args): #transcription of the given strategy
    if len(args) == 0:
        return succeed
    elif len(args) == 1:
        return args[0]
    else:
        return conj_2(args[0], conj(*args[1:]))

And here is conj_2:

def conj_2(goal_1, goal_2):
    return lambda subst: append_map_inf(goal_2, goal_1(subst), list())

Hmmm what is this mystery append map-inf?

mental map for working of conjunction

Here is append_map_inf: (This is again simplistic and will be later modified)

The code for append_map_inf is just a transcription of the diagram above

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]))
    return append_map_inf(goal, subst_stream[1:], res)

Similarly, disjunction has the following strategy:

1. produce 2 streams using the 2 goals independently

2. append them

this is simple enough. Here is the code:

def disj(*args):
    if len(args) == 0:
        return fail
    elif len(args) == 1:
        return args[0]
    else:
        return disj_2(args[0], disj(*args[1:]))

def disj_2(goal_1, goal_2):
    def anon(subst):
        subst1, subst2 = dict(subst), subst
        return append_inf(goal_2(subst1), goal_1(subst2))
    return anon

def append_inf(subst_stream1, subst_stream2):
    # print(subst_stream1)
    # print(subst_stream2)
    res = copy.deepcopy(subst_stream1)
    res.extend(subst_stream2)
    return res

You may think we end up with repeats in the event of passing the same goal, we could control this...have omitted

Also, initially one may think we also end up with repeats when 2 logically equivalent formulae are passed. However, we have no guarantee of order of solutions, nor do we have a guarantee

that the stream is finite...

We can still achieve a lot with simple AND, ORS and our basic goal eq_eq.

In fact, we can define more goals through compositions of these basic goals.

CLASS ACTIVITY: LET'S WRITE something to get the even members of a list

def evmembero(mem, l):
    def anon(subst):
        if len(l) == 0:
            return fail(subst)
        return conj(disj(eq_eq(mem, l[0]), evmembero(mem, l[1:])), eveno(mem))(subst)
    return anon

def eveno(x):
    def anon(subst):
        if (walk(x,subst) % 2 == 0):
            return succeed(subst)
        else:
            return fail(subst)
    return anon

Through this example, we explore the power of logic programming. The crux of logic programming is to represent the output as a solution to a logical expression (this differs from the more familiar imperative approach of telling the program exactly what to do).

Advantage: Our programs are more "mathematical", and thus more verifiable!