I. Introduction to Logic Programming A. additional motivation for logic programming in particular B. logic programming idea ------------------------------------------ CREATING THE IDEA OF LOGIC PROGRAMMING Recall motivation for declarative prog: 1. write programs efficiently 2. execute specifications 3. separate directions about control and data structures How would you specify a sort routine? ------------------------------------------ How can we then use this to sort some particular list L? How could such a theorem be proved? ------------------------------------------ ABSTRACTING FROM THE EXAMPLE Model: programs are modeled as Specification of a problem: a problem to be solved is Answer to a problem: ------------------------------------------ C. History (omit) D. What to read in Dale Miller's notes II. Logical Computing A. What this is about ------------------------------------------ QUESTIONS FOR DESIGNING A LOGIC PROGRAMMING LANGUAGE 1. What should the language talk about? 2. What logical connectives work for describing things and relationships? 3. What logical connectives work for describing queries? ------------------------------------------ B. What should the language talk about? ------------------------------------------ WHAT TO DESCRIBE/SPECIFY? What? Syntax: ------------------------------------------ What should the language talk about? C. What logical connectives work for describing relationships? ------------------------------------------ CONNECTIVES FOR EFFECTIVE SPECIFICATION Effectively describe L2? - (ordered L2) and (permutation L1 L2) - (ordered L2) or (empty L2) Effectively describe a relationship? - (sorted L1 L2) if ((ordered L2) and (permutation L1 L2)) - (less X Y) if not (greater X Y) ------------------------------------------ What about universal quantification? Existential quantification? D. What logical connectives work for describing conjectures or queries? ------------------------------------------ CONNECTIVES FOR EFFECTIVE QUERYING Effectively ask for L2? - (ordered L2) and (permutation L1 L2) - (ordered L2) or (empty L2) ------------------------------------------ III. Pure Prolog A. Syntax reminders 1. Don't forget those periods! 2. comment convention is % to the end of the line 3. Case sensitive: variables begin with captial letter B. facts and rules ------------------------------------------ FACTS AND RULES % fact good prolog. % rule good X :- logical X. ------------------------------------------ 1. compound terms in LambdaProlog ------------------------------------------ COMPOUND TERMS (tree Subtree1 Root Subtree2) (((tree Subtree1) Root) Subtree2) %lists: a::b::nil (sentence (np (n ron)) (vp (v gave) (np (art a) (n paper)) (compls (prep to) (np (n sue))))) ------------------------------------------ 2. scope of variables ------------------------------------------ SCOPE OF VARIABLES (understand L X) :- (know terms L X), (know syntax L X), (know semantics L X). (grandparent K L) :- (parent K P), (parent P L). ------------------------------------------ Which L's should mean the same person? So what does that mean the scope of a variable is in Prolog? C. kinds and types ------------------------------------------ KINDS AND TYPES % declaration of a type kind event type. kind person type. % declaration of type of a name type actor event -> person -> o. ------------------------------------------ D. Examples 1. assertions ------------------------------------------ % A SEMANTIC NETWORK sig semantic_net. kind event type. kind person type. kind thing type. kind verb type. type event1 event. type paper thing. type sue person. type ron person. type gave verb. type event2 event. type football thing. type swen person. type object event -> thing -> o. type recipient event -> person -> o. type actor event -> person -> o. type action event -> verb -> o. ------------------------------------------ ------------------------------------------ module semantic_net. % a semantic network object event1 paper. recipient event1 sue. actor event1 ron. action event1 gave. ------------------------------------------ 2. queries what is the result of the query: recipient event1 Who. ? how would you add the fact that in event2, sue gave the football to swen? E. Lists ------------------------------------------ % LISTS sig list. % this is all built in to lambda Prolog % but this shows how it would be done. kind list type -> type. type nil (list T). type '::' T -> (list T) -> (list T). infixr '::' 5. ------------------------------------------ ------------------------------------------ LIST NOTATION ISN'T SPECIAL % signature file sig lisp_lists. kind lisp_list type -> type. type the_empty_list (lisp_list T). type cons T -> (lisp_list T) -> (lisp_list T). type to_list (lisp_list T) -> (list T) -> o. end % the module module lisp_lists. % an inductive definition to_list the_empty_list nil. to_list (cons Head Tail) (Head::PL) :- to_list Tail PL. end ------------------------------------------ what are these type decls like in Haskell? 1. example using lists ------------------------------------------ sig addtoend1. type addtoend (list T) -> T -> (list T) -> o. module addtoend1. addtoend ------------------------------------------ How would we write this? F. Interpretations of clauses ------------------------------------------ INTERPRETATIONS OF CLAUSES (h X) :- (b1 Y), (b2 Z), (b3 W). declarative interpretation: procedural interpretation: ------------------------------------------ 1. declarative 2. Procedural reading (programming language) G. tracing queries H. variation on addtoend ------------------------------------------ % VARIATION ON ADDTOEND sig addtoend2. type equals T -> T -> o. type addtoend (list T) -> T -> (list T). module addtoend2. equals (addtoend nil X) (X::nil). equals (addtoend (Y::L) X) (Y::M) :- equals (addtoend L X) M. ------------------------------------------ can you trace this? I. reverse can you write append of type (list T) -> (list T) -> (list T) -> o ? IV. Prolog Programming Techniques A. key ideas 1. Think of programs as *relations* 2. state what is true B. Recursion 1. Unary numbers ------------------------------------------ %%% The natural numbers in unary notation, %%% and some operations sig unary. kind nat type. type s nat -> nat. type z nat. type le nat -> nat -> o. type lt nat -> nat -> o. type ge nat -> nat -> o. type gt nat -> nat -> o. type plus nat -> nat -> nat -> o. type diff nat -> nat -> nat -> o. type times nat -> nat -> nat -> o. type to_int nat -> int -> o. type to_nat int -> nat -> o. ------------------------------------------ ------------------------------------------ %%% The natural numbers in unary notation, and some operations %%% These allow backtracking (except for to_int and to_nat). %%% AUTHOR: Gary T. Leavens module unary. %%% ``le N1 N2'' succeeds if N1 is less than or equal to N2. le z X. le (s X) (s Y) :- le X Y. %%% ``lt N1 N2'' succeeds if N1 is strictly less than N2. lt z (s X). lt (s X) (s Y) :- lt X Y. %%% ``ge N1 N2'' succeeds if N1 is greater than or equal to N2. ge X Y :- le Y X. %%% ``gt N1 N2'' succeeds if N1 is strictly greater than N2. gt X Y :- lt Y X. %%% ``plus X Y Z'' succeeds when Z is the sum of X and Y. plus z X X. plus(s X) Y (s Z) :- plus X Y Z. %%% ``diff X Y Z'' succeeds when Z is X - Y. diff X Y Z :- plus Z Y X. %%% ``times X Y Z'' succeeds when Z is the product of X and Y. times z X z. times (s X) Y Z :- (times X Y W), (plus W Y Z). %%% ``to_int N I'' succeeds if N represents the integer I. to_int z 0 :- !. to_int (s M) Np1 :- (to_int M N), (Np1 is N + 1). %%% ``to_nat I N'' succeeds if N represents the integer I. to_nat 0 z :- !. to_nat M (s N) :- (Mm1 is M - 1), (to_nat Mm1 N). ------------------------------------------ How would you do division? exponentiation? 2. More about lists ------------------------------------------ module list_examples. type member T -> (list T) -> o. % X is a member of a list of the form Y::Zs either if Y = X % or if X is a member of Zs. The cases are handled by unification. % The failure of (member X nil) is handled by the closed world assumption. member X (X::Xs). member X (Y::Ys) :- member X Ys. % an alternative translation would be... type member2 T -> (list T) -> o. member2 X (Y::Zs) :- X = Y. member2 X (Y::Zs) :- not (X = Y), (member2 X Zs). type append (list T) -> (list T) -> (list T) -> o. % The append of lists Xs and Ys is defined by induction % on the structure of Xs. % basis: if Xs is nil, the result is Ys append nil Ys Ys. % induction: if Xs has the form X::Xs', then the result is X::Zs, % where Zs is (append Xs' Ys Zs). append(X::Xs) Ys (X::Zs) :- append Xs Ys Zs. % Using append, we can do member solely using Prolog's backtracking. % The idea is that X is a member of a list L if L can be written as % L1 concatenated with X::nil concatenated with L2. This may seem tricky, % but it's just based on that definition. type member3 T -> (list T) -> o. member3 X L :- append L1 (X::L2) L. type reverse (list T) -> (list T) -> o. % The reverse of a list L is defined by induction on the structure of L: % basis: reverse of nil is nil reverse nil nil. % induction: if L has the form H::T, its reverse is the reverse of T % concatenated with H::nil. reverse (Head::Tail) L :- (reverse Tail M), (append M (Head::nil) L). ------------------------------------------ Can you write subst_first of type (list T) -> T -> T -> (list T)? 3. association lists ------------------------------------------ sig alists. kind alist type -> type -> type. type the_empty_alist (alist Key Val). type acons Key -> Val -> (alist Key Val) -> (alist Key Val). type lookup Key -> (alist Key Val) -> Val -> o. module alists. %%% lookup is like LISP assoc; it returns the value, if any, for a key in %%% an alist. There is a value if the key is a member of some Key-Value pair %%% in the alist. lookup Key (acons Key Value Alist) Value. lookup Key (acons K V Alist) Value :- lookup Key Alist Value. ------------------------------------------ ------------------------------------------ sig alists. kind alist type -> type -> type. type the_empty_alist (alist Key Val). type acons Key -> Val -> (alist Key Val) -> (alist Key Val). type lookup Key -> (alist Key Val) -> Val -> o. end module alists. %%% lookup is like LISP assoc; it returns the value, if any, for a key in %%% an alist. There is a value if the key is a member of some Key-Value pair %%% in the alist. lookup Key (acons Key Value Alist) Value. lookup Key (acons K V Alist) Value :- lookup Key Alist Value. end $ tjsim capitals. ... [capitals] ?- (capitals C), (lookup peru C Capital). The answer substitution: Capital = lima C = acons chile santiago (acons peru lima the_empty_alist) ------------------------------------------ 4. difference lists ------------------------------------------ sig diff_lists. kind diff_list type -> type. %%% difference list terms %%% A difference list is a term of the form (diff L Z), %%% where L is a list whose last element is the logical variable Z. type diff (list T) -> (list T) -> (diff_list T). %%% difference list observers. type dl_to_list (diff_list T) -> (list T) -> o. type list_to_dl (list T) -> (diff_list T) -> o. type simplify (diff_list T) -> (list T) -> o. type diffappend (diff_list T) -> (diff_list T) -> (diff_list T) -> o. end module diff_lists. %%% dl_to_list and list_to_dl work in one direction only, but don't rely %%% on the occurs check. %%% simplify works in both directions, but relies on the occurs check. %%% ``dl_to_list DL L'' succeeds if DL represents the list L. dl_to_list (diff nil X) nil :- !. dl_to_list (diff X X) nil :- !. dl_to_list (diff (X::Y) Z) (X::W) :- dl_to_list (diff Y Z) W. %%% ``list_to_dl L DL'' succeeds if L is represented by the diff list DL. list_to_dl nil (diff X X). list_to_dl (X::W) (diff (X::Y) Z) :- list_to_dl W (diff Y Z). %%% ``simplify DL L'' succeeds if DL represents the list L. simplify (diff X X) nil. simplify (diff (X::Y) Z) (X::W) :- simplify (diff Y Z) W. %%% ``diffappend DL1 DL2 DL3'' succeeds if DL3 is the concatenation %%% of DL1 and DL2. Appending difference lists works like the arithmetic: %%% (X-Y) + (Y-Z) = X-Z diffappend (diff X Y) (diff Y Z) (diff X Z). end ------------------------------------------ a. examples b. occurs check examples c. diffappend examples