I. Logical Basis of Logic Programming A. answering queries from ground facts 1. terms ------------------------------------------ TERMS AND GROUND TERMS def: a term is a in the grammar. Simple cases: either a constant (1, "a string", sue) variable (X, Xs) application ((f 3) Y), (f 3 Y) lambda abstraction (X : int \ X) def: a ground term has no free variables. examples: (foo a b) (X : int \ X) counterexamples: (foo X Y) (X : int \ Y) ------------------------------------------ what is (X : int \ X) like in Haskell? can a variable be both free and bound in a term? 2. without logical variables ------------------------------------------ ANSWERING QUERIES WITHOUT VARIABLES (WITH FACTS WITHOUT VARIABLES) in module semantic_net: object event1 paper. $ tjsim semantic_net [semantic_net] ?- object event1 paper. yes logical rule: identity G ____ G ------------------------------------------ ------------------------------------------ CLOSED WORLD ASSUMPTION module semantic_net. object event1 paper. recipeint event1 sue. actor event1 ron. action event1 gave. [semantic_net] ?- object event1 football. no (more) solutions [semantic_net] ?- not(object event1 football). yes logical rule: closed world assumption G is not provable ______________________ not G ------------------------------------------ 3. with logical variables, ------------------------------------------ ANSWERING QUERIES WITH LOGICAL VARIABLES [semantic_net] ?- object event1 What. The answer substitution: What = paper logical meaning of query: logical rule: generalization ___________________________ exists X1...Xn . P(X1...Xn) def: a logical variable has a name that starts with an upper case letter and stands for an ------------------------------------------ a. substitution ------------------------------------------ SUBSTITUTIONS def: a substitution is example: s: {X, Y} -> {(X \ X), (father me dad)} where s[[X]] = (X \ X) s[[Y]] = (father me dad). empty: {} -> {} counterexample: bad: {X} -> {X} application of a substitution to a term: s[[(t X Y)]] = ------------------------------------------ b. instances ------------------------------------------ INSTANCES def: A is an instance of B iff Examples: FOR YOU TO DO Give 3 instances of the term: (tree Left Right (f Node)) Can (tree Right Left (f 2)) be an instance? ------------------------------------------ can an instance have variables in it? c. recap of existential queries d. conjunctive queries ------------------------------------------ CONJUNCTIVE QUERIES [semantic_net] ?- (actor Event Who), (action Event gave). The answer substitution: Who = ron Event = event1 logical meaning: exists Event, Who . (actor Event Who) and (action Event gave) logical rule: conjunction ______________________________ exists X1...Xn . P1(X1...Xn) and P2(X1...Xn) ------------------------------------------ B. answering queries using rules ------------------------------------------ LOGICAL MEANING OF RULES sig patriarchical_family. kind person type. kind person type. type son person -> person -> o. type dad person -> person -> o. type male person -> o. type daughter person -> person -> o. type female person -> o. module patriarchical_family. son X Y :- (dad Y X), (male X). daughter X Y :- (dad Y X), (female X). logical meaning: ------------------------------------------ ------------------------------------------ VARIABLES NOT IN HEAD ACT AS IF EXISTENTIALLLY QUANTIFIED (granddad X Z) :- (dad X Y), (dad Y Z). means: all X,Y,Z . (granddad X Z) <== (dad X Y) and (dad Y Z). = all X,Z . all Y. (granddad X Z) <== (dad X Y) and (dad Y Z). = all X,Z . all Y. (granddad X Z) or not((dad X Y) and (dad Y Z)). = all X,Z . (granddad X Z) or (all Y. not((dad X Y) and (dad Y Z))). = all X,Z . (granddad X Z) or not(exists Y. ((dad X Y) and (dad Y Z))). = all X,Z . (granddad X Z) <== (exists Y. ((dad X Y) and (dad Y Z))). ------------------------------------------ 1. logical basis for queries using rules ------------------------------------------ ANSWERING QUERIES USING RULES module my_family. accumulate patriarchical_family. dad pop gayle. dad pop me. dad pop glen. dad pop gina. female gayle. female gina. male me. male glen. $ tjsim my_family [my_family] ?- son me pop. yes logical rule: universal modus ponens: where s is a ________________________ A' = s[[A]] A' ------------------------------------------ Why does that make sense? What does it mean computationally? C. answering queries using universal facts 1. universal facts ------------------------------------------ ANSWERING QUERIES USING UNIVERSAL FACTS module universal_truths. plus 0 X X. likes X vanilla. $tjsim universal_truths [universal_truths] ?- likes arch vanilla. yes [universal_truths] ?- plus 0 3 3. yes logical rule: instantiation all X . A _____________ where s is a substitution A' and A' = s[[A]] ------------------------------------------ 2. universal facts and existential queries ------------------------------------------ ANSWERING EXISTENTIAL QUERIES WITH UNIVERSAL FACTS [universal_truths] ?- plus 0 Z 2. The answer substitution: Z = 2 logical proof: all X . (plus 0 X X) [axiom] _____________________ [instantiation] (plus 0 2 2) _____________________ [generalization] exists Z . (plus 0 Z 2) by subst. s = {X |-> 2, Z |-> 2} (note only print the user's part) ------------------------------------------ ------------------------------------------ COMMON INSTANCES def: C is a common instance of A and B e.g. (plus 0 2 2) is common instance of (plus 0 Z 2) and (plus 0 X X) ------------------------------------------ D. meaning of a logic program what does a logic program mean? what could it mean for a logic program to be correct? ------------------------------------------ SEMANTICS AND CORRECTNESS def: meaning of a logic program P, M[[P]], ------------------------------------------ is the meaning of the son relation sound? complete? Is (son X Y) by itself complete? Sound? II. Unification A. the problem ------------------------------------------ THE PROBLEM How to make "guess" when matching existential queries vs. universally quantified rules? What are we guessing? What determines that? ------------------------------------------ 1. two further problems a. the variable convention ------------------------------------------ TWO FURTHER PROBLEMS Problem 1: good (tree Left Right). % fact ?- good (tree Right Left). % query Is there a common instance? Solution: ------------------------------------------ b. generality and most general unifiers ------------------------------------------ FURTHER PROBLEM 2 Example (member Y (Y::nil)). % fact ?- (member Z (X::nil)). % query What substitution to use? s1 = {Y |-> 1, Z |-> 1, X |-> 1} s2 = {Y |-> 2, Z |-> 2, X |-> 2} s3 = {Y |-> 3, Z |-> 3, X |-> 3} ... ------------------------------------------ ------------------------------------------ GENERALITY def: a term T is more general than V iff example: (foo X X X) vs. (foo 3 3 3) def: T is an alphabetic variant of V iff ------------------------------------------ which is more general? is (member Y (Y::nil)) an alphabetic variant of (member Z (X::nil))? 2. unifier ------------------------------------------ UNIFIER def: a unifier for terms T and V is a def: T and V unify iff there is a unifier for T and V. def: most general unifier (mgu) of T and V is unifier for T and V that generates the most general common instance. ------------------------------------------ ------------------------------------------ UNIFIER EXAMPLES sig unifier-examples. kind thing type. type algol thing. type star thing -> o. type g A -> int -> o. type eq A -> A -> o. module unifier-examples. star algol. g X 3. eq X X. $ tjsim unifier-examples [unifier-examples] ?- star X. ?- g 4 Y. ?- eq Y Z. ------------------------------------------ a. exercises ------------------------------------------ FOR YOU TO DO Compute the mgu, if any, of each pair: (member 3 3::nil) (member X (X::nil)) (member Y (3::nil)) (member X (X::nil)) (member 3 (4::nil)) (member X (X::L)) (length (3::nil) N) (member X (X::L)) (member X (X::L)) (member (3::nil) N) (member X (X::L)) (member Y ((tree (Y::nil) (Q::nil))::M)) (diff X X) (diff (1::2::Y) Y) ------------------------------------------ b. occurs check From the examples, why would we want the occurs check? III. Resolution (logical basis for Prolog) A. putting universality together with rules How can we answer existential queries with universally quantified rules? B. An abstract interpreter ------------------------------------------ ABSTRACT INTERPRETER (may not terminate) input: a logic program P, and a goal G output: a substitution s or failure resolvent <- G. s <- { }. while the resolvent is not empty do choose from the resolvent a goal A and from P a (renamed) clause A' :- B1,...,Bn such that A and A' unify with mgu s'. (fail if no such goal and clause exist) remove A from the resolvent and add B1,...,Bn to the resolvent. resolvent <- s'[[resolvent]] s <- s' o s % compose s' with s done. output s % success ------------------------------------------ ------------------------------------------ COMPOSITION OF SUBSTITUTIONS def: s' o s = {a |-> b | s'[[s[[a]]]] = b} Examples: {Q |-> Z, X |-> sue} o {Y |-> (foo X), R |-> bob} = {Y |-> (foo sue), R |-> bob} ------------------------------------------ C. tracing the abstract interpreter 1. Example (for use below) ------------------------------------------ sig some-facts. kind person type. type sue person. type ron person. type scientist person -> o. type spanish person -> o. type american person -> o. type logician person -> o. module some-facts. % facts scientist sue. %1 scientist ron. %2 spanish sue. %3 american ron. %4 % rule logician X :- scientist X. %5 ------------------------------------------ 2. tracing a goal ------------------------------------------ A FAILURE TRACE [some-facts] ?- (logician Y), (american Y). resolvent = (logician Y), (american Y) s = { } resolves with %5, s' = { Y |-> X' } resolvent = (scientist X'), (american X') s = { Y |-> X' } resolves with %1, s'' = { X' |-> sue } resolvent = (american sue) s = s'' o s' = { Y |-> sue } failure ------------------------------------------ ------------------------------------------ A SUCCESSFUL TRACE ?- (logician Y), (american Y). resolvent = (logician Y), (american Y) s = { } resolves with %5, s' = { Y |-> X' } resolvent = (scientist X'), (american X') s = { Y |-> X' } resolves with %2, s'' = { X' |-> ron } resolvent = (american ron) s = s'' o s' = { Y |-> ron } resolves with %4, s''' = { } resolvent = s = s''' o s'' o s' = { Y |-> ron } output s = { Y |-> ron } ------------------------------------------ D. correctness of the abstract interpreter (skip!) 1. to ask a query Q, see if not(Q) produces a contradiction ------------------------------------------ TO ASK QUERY Q Idea: see if (not Q) is a contradiction ?- (logician Y), (american Y). ------------------------------------------ ------------------------------------------ meaning: exists Y . (logician Y) and (american Y) negation is: not (exists Y . (logician Y) and (american Y)) = forall Y . not ((logician Y) and (american Y)) = forall Y . (not (logician Y)) or (not (american Y)) ------------------------------------------ 2. to eliminate quantifiers, use fresh variables (skolemize) ------------------------------------------ ELIMINATE QUANTIFIERS BY SKOLEMIZING forall Y . (not (logician Y)) or (not (american Y)) = (not (logician Y)) or (not (american Y)) forall X . (logician X) <== (scientist X) = (logician X) or not(scientist X) universal modus ponens becomes: for s a substitution (A or not(B1) or ... or not(Bn)), s[[B1]], ..., s[[Bn]] __________________________________ s[[A]] ------------------------------------------ a. to remove implications, use formula: (A <== B) = (A or not B) b. resolution rule for doing refutations ------------------------------------------ REFUTATION AND RESOLUTION Form of refutations: (not R), R _________________ *contradiction* Conjunctive query in this form: (not R) or (not P), P ___________________ (not R) ------------------------------------------ ------------------------------------------ REFUTATION OF A NEGATED QUERY (not (logician Y)) or (not (american Y)), (logician X) or not(scientist X) __________________________________________ not(scientist U) or (not (american U)), (scientist ron) _______________________ (not (american ron)), (american ron) _______________________ *contradiction* ------------------------------------------ What substitutions were used in the refutation? ------------------------------------------ RESOLUTION simple version of resolution: (not R) or (not P), (P or (not Q)) _______________________________ (not R) or (not Q) for s a substitution: (not A1) or ... or (not Ai) or ... or (not Am), (Ai or (not B1) or ... or (not Bn)) ________________________________________ (not s[[A1]]) or ... or (not s[[B1]]) or ... or (not s[[Bn]]) or ... or (not s[[Am]]) ------------------------------------------ E. Why Horn clauses? IV. Procedural model of Prolog A. practical questions in using resolution (and Prolog's answers) ------------------------------------------ CHOICES IN THE ABSTRACT INTERPRETER what substitution to use? what to resolve? what disjunct in goal to resolve? what clause to resolve against? ------------------------------------------ 1. Top-down vs. bottom up control a. top-down control (backward chaining) as in Prolog b. bottom up control (forward chaining) as in OPS5 2. Depth-first search vs breadth-first search. ------------------------------------------ sig needs_breadth_first. type p o. type q o. module needs_breadth_first. p :- p, q. p. q. ------------------------------------------ B. search trees that show backtracking C. Another way to see examples, time vs. goals stack graphs ------------------------------------------ sig pop_psych1. type imokay o. type youreokay o. type hesokay o. type theyreokay o. module pop_psych1. imokay :- youreokay, hesokay. % C1 youreokay :- theyreokay. % C2 hesokay. % C3 theyreokay. % C4 [pop_psych1] ?- imokay. yes ------------------------------------------ ------------------------------------------ sig pop_psych2. accum_sig pop_psych1. type shesokay o. type imnotokay o. type hesnotokay o. module pop_psych2. accumulate pop_psych1. hesnotokay :- imnotokay. % C5 shesokay :- hesnotokay. % C6 shesokay :- theyreokay. % C7 [pop_psych2] ?- shesokay. yes ------------------------------------------ ------------------------------------------ sig pop_psych3. accum_sig pop_psych2. module pop_psych3. accumulate pop_psych2. hesnotokay :- shesokay. % C8 hesnotokay :- imokay. % C9 [pop_psych3] ?- shesokay. Simulator: Stack overflow. ------------------------------------------ can you trace this? D. practical implications 1. order of rules matters 2. order of clauses in body matters 3. termination domain (skip) how would you define the termination domain of a program? V. non-logical features of logic programming languages A. Cut (!) ------------------------------------------ sig cut_examples. type mbr T -> (list T) -> o. type mbr1 T -> (list T) -> o. type mbr2 T -> (list T) -> o. module cut_examples. mbr Head (Head::Tail). mbr Element (Head::Tail) :- mbr Element Tail. % membership test only mbr1 Head (Head::Tail) :- !. mbr1 Element (Head::Tail) :- mbr Element Tail. % discussed in class... mbr2 Head (Head::Tail). mbr2 Element (Head::Tail) :- !, mbr Element Tail. ------------------------------------------ 1. What does cut do? a. cut prunes all clauses below it ------------------------------------------ CUT PRUNES ALL CLAUSES BELOW IT sig cut_examples2. type p o. type b o. type a o. type c o. type d o. type e o. type f o. type g o. type h o. module cut_examples2. p :- a, b, c. b :- d, e, !, f. b :- g, h. a. d. e. c. g. h. ------------------------------------------ does the query b. succeed? How about p.? b. Backtracking across cut causes whole clause to fail ------------------------------------------ USING CUT TO DO IF THEN ELSE sig if. type if o -> o -> o -> o. module if. %%% ``if Test E1 E2'' does E1 when Test %%% succeeds, and otherwise does E2. %%% This uses cut! if Test E1 E2 :- Test, !, E1. if Test E1 E2 :- E2. ------------------------------------------ B. Negation as failure 1. negation treated as unprovability (closed world assumption) ------------------------------------------ NEGATION IN (\)PROLOG not G :- G, !, fail. not G . ------------------------------------------ 2. good programming style avoids cut-fail, since logic disappears. 3. "not" doesn't work correctly for non-ground goals ------------------------------------------ NOT DOESN'T WORK CORRECTLY ON NON-GROUND GOALS sig negation_problem. kind person type. kind person type. type unmarried_student person -> o. type married person -> o. type student person -> o. type bill person. type joe person. module negation_problem. unmarried_student X :- (not (married X)), (student X). student bill. married joe. [negation_problem] ?- unmarried_student X. no (more) solutions [negation_problem] ?- unmarried_student bill. yes ------------------------------------------ C. Other non-logical stuff in Prolog 1. is: allows one to use computer's arithmetic ------------------------------------------ ACCESS TO MACHINE ARITHMETIC sig inc. type inc int -> int -> o. module inc. inc N M :- M is N + 1. [inc] ?- inc 2 M. The answer substitution: M = 3 More solutions (y/n)? y no (more) solutions [inc] ?- inc 2 3. yes [inc] ?- inc N 3. Error: is: Flexible term head in evaluation: _194 no (more) solutions ------------------------------------------ 2. asserta, assertz: put rules in database 3. retract: takes rule out of database VI. higher order features of lambda prolog A. lambda terms 1. syntax ------------------------------------------ LAMBDA TERMS in \Prolog syntax: (var \ body) (var : type \ body) examples: (x \ x) (i \ (s (s i))) (x \ (T \ type_of H x T)) ------------------------------------------ what's this like in SML or Haskell? 2. type rules ------------------------------------------ SOME TYPE RULES FOR \PROLOG |- M : [query] -------------- ?- M. checks |- M: [-> E] -------------------------- |- (M N): T [-> I] ---------------------- |- (x \ M): ------------------------------------------ 3. mapping so what would the type be in \Prolog? what's the type of reduce? can you write reduce of type (A -> B -> B) -> (list A) -> B -> B -> o ? What's this like in Haskell? ------------------------------------------ sig inc. type inc int -> int -> o. module inc. inc N M :- M is N + 1. Using inc, how would you increment each element in a list of ints? I.e, what are M and I such that: ?- M I (5::8::2::nil) L. L = 6 :: 9 :: 3 :: nil. ------------------------------------------ what goes wrong with mapfun and inc? can you write for_each of type for_each (A -> o) -> (list A) -> o. such that for_each P L succeeds if P is true for each element of list L? B. semantics of lambda abstractions (skip or go quickly if done already) what 2 rules can you derive from these examples? how can these be used lambda-prolog or SML? ------------------------------------------ SUMMARY OF EQUATIONAL RULES FOR THE LAMBDA CALCULUS [alpha] (x \ M) = (y \ [y/x]M) if y is not free in M and y is not bound in M [beta] (x \ M) N = [N/x]M [eta] (x \ M x) = M if x is not free in M ------------------------------------------ ------------------------------------------ SUBSTITUTION [N/x]x = N [N/x]y = y, if y is not x [N/x](M M') = ([N/x]M [N/x]M') [N/x](x \ M) = (x \ M) [N/x](y \ M) = ((z \ [N/x]([z/y]M))), if y is not x and if x is not free in M or y is not free in N, then z is y, else z is not in M or N ------------------------------------------ ------------------------------------------ FREE VARIABLES FV(x) = {x} FV(M M') = FV(M) union FV(M') FV(y \ M) = FV(M) - {y} ------------------------------------------ C. implication (=>) 1. examples of using => in queries ("what if" querries) 2. intuionistic examples ------------------------------------------ module intuitionistic. type false o. type p o. type q o. type r o. ------------------------------------------ 3. semantics D. universal quantifier (pi) ------------------------------------------ sig qualifier_db. kind student type. kind class type. type john student. type mary student. type cs541 class. type cs542 class. type cs641 class. type passed student -> class -> o. type qualify student -> o. module qualifier_db. passed john cs541. passed mary cs541. passed mary cs542. passed mary cs641. % the following doesn't do what you think. qualify X :- (pi c \ (passed X c)). ------------------------------------------ ------------------------------------------ sig qualifier_db_fixed. kind student type. kind class type. type john student. type mary student. type cs541 class. type cs542 class. type cs641 class. type passed student -> class -> o. type classes list class -> o. type qualify student -> o. module qualifier_db_fixed. import maps. passed john cs541. passed mary cs541. passed mary cs542. passed mary cs641. classes (cs541::cs542::cs641::nil). qualify X :- classes CL, for_each (passed X) CL. ------------------------------------------ E. existential quantifier (sigma) So what's the difference between these queries? VII. higher-order abstract syntax VIII. Research Directions in declarative langauges A. Software Engineering 1. Specification and Verification 2. Programming in the Large B. New Logics and models of computation C. Compilation and Efficiency