Logic Programming
Initial example, something to solve:
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 anonExplain 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 resUnification:
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 FalseThat'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:
0 arguments? vacuous success
1 argument? the goal : conj(goal) is same as goal
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?
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:
produce 2 streams using the 2 goals independently
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 resYou 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!
Last updated