Logic Programming Logic is the study of correct arguments. For instance, for some predicate P; for instance:
we can “prove” this by doing the thing we can also do that by contradiction (but that won’t create a witness y of the statement) PROLOG PROgramming LOgic - PROLOG; not general, but good in specific cases (databases, scheduling outputs, etc.) pros and cons pros very declarative easy to write some backtracking search approaches worst “algorithm” / “complexity” obscured because you only have one algorithm because you get performance only by wrangling goal ordering PROLOG time So, every predicate returns true/false. rev([1,2,3], [3,2,1]) => true However, you could give the “witness” as a variable, and PROLOG will fill in the witness rev([1,2,3], y) => true y := [3,2,1] you can actually put random places, and PROLOG will try to fill it out rev([1,2,a], [3,2,b]) => true a := 3 b := 1 phraseology a constant: 1, nil a variable a constructor: c(x,y,z) an atom: apply a predicate to terms lists have special sugar [x,y, ...] program A PROLOG program has facts and rules. rule/clause P1(t11, ...) := P2(t21, ...), ... (“if all the things on the right hand side is true, then the left hand side is true”) (if you want to write the disjunction “OR” of the predicates, write ; instead of ,) fact a rule without a RHS, so automatically true P1(t11, ...). PROLOG semantics Let \sigma range over all “ground substitutions” (substitution that maps variables to terms without variables—“grounding” the variables). Given:
the semantics is the smallest set of atoms placed in F which would be satisfying
all facts are in F any implications proven by atoms in F is in F PROLOG execution Given a goal a, find a rule whose LHS matches a, add the RHS atoms as subgols until you get to facts. example imokay :- youreokay, hesokay youreokay :- theyreokay hesokay. theyreokay. Let’s say we want to prove imokay imokay > =youreokay, hesokay; two more subgoals now yourokay > =theyreokay; still two more subgoals theyreokay => fact hesokay => fact Ok, now let’s add an new constraint: imokay :- youreokay, hesokay youreokay :- theyreokay hesokay. theyreokay. hesnotokay := imnotok shesokay := hesnotokay shesokay := theyreokay refine rule: we will select the first textually matching rule if a subgoal failso select the next matching rule if no matching rule is found, fail this is standard recursive backtracing. depth-first instead of breadth-first PROLOG semantics implies breadth-first search, but that’s pretty bad (i.e. we have to keep adding our subgoals in a breadth-first way). variable substitution To satisfy a goal g, we want to find the first untried rule G :- H_1, …, H_{n}, such hat s_1 = unify(g,G) such that the function computes a substitution s1 s uch that after substitution the syntax are equivalent s_1(g) = s_1(G) backtracking Consider a rule G :- H_1, H_2, …, H_{n} If there are substitutions that fail on H_1, we will have to backtrack on the right on different inputs as well, and not just backtrack on different G. As you match and unify statements, cache your substitutions around and keep applying them. occurs check Most implementations for substitution on a=T doesn’t ever check that a doesn’t occur in T. But that’s deviating from the semantics. cut Backtracking can be super expensive, so PROLOG includes backtracking boundaries: A :- B,C,!,D meaning if D fails, we don’t try to resatisfy B,C with different variables and instead fail the entire rule. examples reverse a list % first we define a predicate for (a,b,_), if b is stuck to the right of a addright(nil, X, [X]). addright(cons(A,B), X, cons(A,Z)) = addright(B,X,Z) % now, reverse is just done simply rev(nil, nil). rev(cons(X<y), Z) := rev(Y,W), addright(W,Y,Z)