Logic Programming
Last updated
Last updated
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:
Why? Because then, calling goal_name(*args)(substitution) -> stream!
Writing eq_eq:
General algorithm: Pretty simple...
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:
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.
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:
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:
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.
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:
And here is conj_2:
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
Similarly, disjunction has the following strategy:
produce 2 streams using the 2 goals independently
append them
this is simple enough. Here is the code:
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
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!