Summary

This document appears to be related to Prolog programming, a logic programming language.

Full Transcript

CSCC24 – Principles of Programming Languages Anya Tafliovich1 1 with thanks to S.McIlraigh, G.Penn, P.Ragde 1 Logic Programming and Prolog Logic programming languages are neither procedural nor functiona...

CSCC24 – Principles of Programming Languages Anya Tafliovich1 1 with thanks to S.McIlraigh, G.Penn, P.Ragde 1 Logic Programming and Prolog Logic programming languages are neither procedural nor functional. Specify relations between objects larger(3,2) father(tom,jane) Separate logic from control: Programmer declares what facts and relations are true. System determines how to use facts to solve problems. System instantiates variables in order to make relations true. Prolog Suppose we state these facts: male(charlie). parent(charlie,bob). female(alice). parent(eve,bob). male(bob). parent(charlie,alice). female(eve). parent(eve,alice). We can then make queries: ?- male(charlie). ?- parent(Person, bob). true Person = charlie; Person = eve; ?- male(eve). false false ?- parent(Person, bob), ?- female(Person). female(Person). Person = alice; Person = eve; Person = eve; false false Prolog We can also state rules, such as this one: sibling(X, Y) :- parent(P, X), parent(P, Y). Then the queries become more interesting: ?- sibling(charlie, eve). false ?- sibling(bob, Sib). Sib = bob; Sib = alice; Sib = bob; Sib = alice; false 4 Logic vs Functional Programming In FP, we program with functions. f (x, y , z) = x ∗ y + z − 2 Given a function, we can only ask one kind of question: Here are the argument values; tell me what the function’s value is. In LP, we program with relations. r (x, y , z) = {(1, 2, 3), (9, 5, 13), (0, 0, 4)} Given a predicate, we can ask many kinds of question: Here are some of the argument values; tell me what the others have to be in order to make a true statement. Logic Programming A program consists of facts and rules. Running a program means asking queries. The language tries to find one or more ways to prove that the query is true. This may have the side effect of freezing variable values. The language determines how to do all of this, not the program. How does the language do it? Using unification, resolution, and backtracking. Some Prolog Syntax Layer 0: constants and variables: Constants are: Atoms: any string consisting of alphanumeric characters and underscore ( ) that begins with a lowercase letter. Numbers. Variables are strings that begin with ’ ’ or an uppercase letter. 7 Some Prolog Syntax ::= | ::= | _ ::= ::= | ::= epsilon | | | _ ::= A |... | Z ::= a |... | z ::=... Some Prolog Syntax Layer 1: terms. These are inductively defined: Constants and variables are terms. Compound terms – applications of any n-ary functor to any n terms – are terms. Nothing else is a term. Note: Prolog distinguishes numbers and variables from other terms in certain contexts, but is otherwise untyped/monotyped. 9 Some Prolog Syntax Layer 2: atomic formulae. These consist of an n-ary relation (also called predicate) applied to n terms Note: formulae look a lot like terms because of Prolog’s weak typing. But formulae are either true or false; terms denote entities in the world. In Prolog, atomic formulae can be used in three ways: As facts: in which they assert truth, As queries: in which they enquire about truth, As components of more complicated statements (see below). 10 Some Prolog Syntax ::= | | '(' { , } ')' ::= '(' { , } ')' 11 Prolog Queries A query is a proposed fact that is to be proven. If the query has no variables, returns true/false. If the query has variables, returns appropriate values of variables (called a substitution). ?- male(charlie). true ?- male(eve). false ?- female(Person). Person = alice; Person = eve; false Some Prolog Syntax Layer 3: complex formulae. These are formed by combining simpler formulae. We only discuss a couple: conjunction: in Prolog, and looks like ’,’ Can be used as queries, but not as facts. Using multiple facts is an implicit conjunction. ?- parent(Person, bob), female(Person). Person = eve; false Some Prolog Syntax implication: in Prolog, these are very special. They are written backwards (conclusion first), and the conclusion must be an atomic formula. This backwards implication is written as ’:-’, and is called a rule. Rules can be used in programs to assert implications, but not in queries. sibling(X, Y) :- parent(P, X), parent(P, Y). Horn Clauses (Rules) A Horn Clause is: c ← h1 ∧ h2 ∧ h3 ∧... ∧ hn Antecedents: conjunction of zero or more atomic formulae. Consequent: an atomic formula. Meaning of a Horn clause: “The consequent is true if the antecedents are all true” c is true if h1 , h2 , h3 ,... , and hn are all true 15 Horn Clause Horn Clause = Clause Consequent = Goal = Head Antecedents = Subgoals = Tail Horn Clause with No Tail = Fact Horn Clause with Tail = Rule In Prolog, a Horn clause c ← h1 ∧... ∧ hn is written c :- h1 ,... , hn. Syntax elements: ’:-’ ’,’ ’.’ Prolog Horn Clause A Horn clause with no tail: male(charlie). I.e., a fact: charlie is a male dependent on no other conditions. A Horn clause with a tail: father(charlie,bob):- male(charlie), parent(charlie,bob). I.e., a rule: charlie is the father of bob if charlie is male and charlie is a parent of bob’s. 17 Some Prolog Syntax A logic program is a collection of Horn clauses. Finally, a simplified Prolog grammar: ::=. | :- { , }. ::= '(' { , } ')' ::= '(' { , } ')' | | ::=... ::=... Meaning of Prolog Rules A prolog rule must have the form: c :- a1, a2, a3,..., an. which means in logic: a1 ∧ a2 ∧ a3 ∧ · · · ∧ an → c Restrictions There can be zero or more antecedents, and they are conjoined. There cannot be more than one consequent. 19 non-Horn clauses Many non-Horn formulae can be converted into logically equivalent Horn-formulae, using propositional tautologies, e.g.: ¬¬a ⇔ a double negation ¬(a ∨ b) ⇔ ¬a ∧ ¬b DeMorgan a ∨ (b ∧ c) ⇔ (a ∨ b) ∧ (a ∨ c) distributivity a → b ⇔ ¬a ∨ b implication Bending the Restrictions? Getting disjoined antecedents Example: a1 ∨ a2 ∨ a3 → c. Solution? Syntactic sugar: ; Getting more than 1 consequent, conjoined Example: a1 ∧ a2 ∧ a3 → c1 ∧ c2. Solution? Getting more than 1 consequent, disjoined Example: a1 ∧ a2 ∧ a3 → c1 ∨ c2. Solution? 21 We cannot disjoin consequents Inference with non-Horn formulae is much more difficult, e.g.: a :- b. a :- c. b ; c. ?- a. 22 Variables Variables may appear in the antecedents and consequent of a Horn clause. Prolog interprets free variables of a rule universally. c(X1 ,...,Xn ) :- f(X1 ,...,Xn ,Y1 ,...,Yk ) is, in first-order logic: ∀X1 ,... , Xn , Y1 ,... , Ym · c(X1 ,... , Xn ) ← f (X1 ,... , Xn , Y1 ,... , Ym ) or, equivalently ∀X1 ,... , Xn · c(X1 ,... , Xn ) ← ∃Y1 ,... , Ym · f (X1 ,... , Xn , Y1 ,... , Ym ) Because of this equivalence, we sometimes say that free variables that do not appear in the head are quantified existentially. Note that the Prolog query ?-q(X1 ,..., Xn ) means ∃X1 ,... , Xn · q(X1 ,... , Xn ) 23 Horn Clauses with Variables isaMother(X) :- female(X), parent(X, Y). In first-order logic: ∀X · isaMother (X ) ← ∃Y · parent(X , Y ) ∧ female(X ). 24 Execution of Prolog Programs Unification: variable bindings. Backward Chaining/ Top-Down Reasoning/ Goal-Directed Reasoning: Reduces a goal to one or more subgoals. Backtracking: Systematically searches for all possible solutions that can be obtained via unification and backchaining. Unification Two atomic formulae unify if and only if they can be made syntactically identical by replacing their variables by other terms. For example, parent(bob,Y) unifies with parent(bob,sue) by replacing Y by sue. ?- parent(bob,Y)=parent(bob,sue). Y = sue ; false parent(bob,Y) unifies with parent(X,sue) by replacing Y by sue and X by bob. ?- parent(bob,Y)=parent(X,sue). Y = sue X = bob ; false Unification A substitution is a function that maps variables to Prolog terms. e.g., { X/sue, Y/bob } An instantiation is an application of a substitution to all of the free variables in a formula or term. If S is a substitution and T is a formula or term, then ST denotes the instantiation of T by S. T = parent(X,Y) S = { X/sue, Y/bob } ST = parent(sue,bob) T = likes(X,X) S = { X/bob } ST = likes(bob,bob) Unification C is a common instance of formulae/terms A and B, if there exist substitutions S1 and S2 such that C = S1(A) = S2(B). A = parent(bob,X), B = parent(Y,sue)} S1 = { X/sue }, S2 = { Y/bob } S1(A) = S2(B) = parent(bob,sue) = C A and B are unifiable if they have a common instance C. A substitution that produces a common instance is called a unifier of A and B. parent(bob,X) and parent(Y,sue) are unifiable: { X/sue, Y/bob } is the unifier Unification Examples: p(a,a) unifies with p(a,a). p(a,b) does not unify with p(a,a). p(X,X) unifies with p(b,b) and with p(c,c), but not with p(b,c). p(X,b) unifies with p(Y,Y) with unifier X/b, Y/b to become p(b,b). p(X,Z,Z) unifies with p(Y,Y,b) with unifier X/b, Y/b, Z/b to become p(b,b,b). p(X,b,X) does not unify with p(Y,Y,c). 29 Unification Examples: p(f(X),X) unifies with p(Y,b) with unifier {X\b, Y\f(b)} to become p(f(b),b). p(b,f(X,Y),c) unifies with p(U,f(U,V),V) with unifier {X\b, Y\c, U\b, V\c} to become p(b,f(b,c),c). 30 Unification p(b,f(X,X),c) does not unify with p(U,f(U,V),V). Reason: To make the first arguments equal, we must replace U by b. To make the third arguments equal, we must replace V by c. These substitutions convert p(U,f(U,V),V) into p(b,f(b,c),c). However, no substitution for X will convert p(b,f(X,X),c) into p(b,f(b,c),c). Unification p(f(X),X) should not unify with p(Y,Y). Reason: Any unification would require that f(X) = Y and Y = X But no substitution can make f(X) = X However, Prolog claims they unify: ?- p(f(X),X)=p(Y,Y). X = f(**) Y = f(**) ; false Unification If a rule has a variable that appears only once, that variable is called a “singleton variable”. Its value doesn’t matter — it doesn’t have to match anything elsewhere in the rule. isaMother(X) :- female(X), parent(X, Y). Such a variable consumes resources at run time. We can replace it with , the anonymous variable. It matches anything. If we don’t, Prolog will warn us. Note that p( , ) unifies with p(b,c). Every instance of the anonymous variable refers to a different, unique variable. 33 Most General Unifier (MGU) The atomic formulas p(X,f(Y)) and p(g(U),V) have infinitely many unifiers. {X\g(a), Y\b, U\a, V\f(b)} unifies them to give p(g(a),f(b)). {X\g(c), Y\d, U\c, V\f(d)} unifies them to give p(g(c),f(d)). However, these unifiers are more specific than necessary. The most general unifier (mgu) is {X\g(U), V\f(Y)} It unifies the two atomic formulas to give p(g(U),f(Y)). Every other unifier results in an atomic formula of this form. The mgu uses variables to fill in as few details as possible. Most General Unifier Example: f (W , g (Z ), Z ) f (X , Y , h(X )) To unify these two formulae, we need Y = g (Z ) Z = h(X ) X = W Working backwards from W , we get Y = g (Z ) = g (h(W ) Z = h(X ) = h(W ) X = W So, the mgu is {X \W , Y \g (h(W )), Z \h(W )} 35 Most General Unifier The substitution that results in the most general instance is called the most general unifier (mgu). It is unique, up to consistent renaming of variables. This is the one that Prolog computes. A substitution, σ, is a most general unifier of a set of expressions E if it unifies E , and for any unifier, ω, of E , there is a unifier, λ, such that ω = σ ◦ λ. 36 Most General Unifier A substitution, σ, is a most general unifier of a set of expressions E if it unifies E , and for any unifier, ω, of E , there is a unifier, λ, such that ω = σ ◦ λ. e.g., given p(X,f(Y)) and p(g(U),V), an MGU σ = { X/g(U), V/f(Y) }, and a unifier ω={X/g(a), Y/b, U/a, V/f(b)}, we have ω(p(X,f(Y))) = p(g(a),f(b)), σ(p(X,f(Y))) = p(g(U),f(Y)), so exists λ= { U/a, Y/b } , so that ω(p(X,f(Y))) = λ(σ(p(X,f(Y)))) also ω(p(g(U),V)) = p(g(a),f(b)), σ(p(g(U),V)) = p(g(U),f(Y)), so for λ= { U/a, Y/b } , we have ω(p(g(U),V)) = λ(σ(p(g(U),V))) 37 Most General Unifier Examples: t1 t2 MGU f(X,a) f(a,Y) f(h(X,a),b) f(h(g(a,b),Y),b) g(a,W,h(X)) g(Y,f(Y,Z),Z) f(X,g(X),Z) f(Z,Y,h(Y)) f(X,h(b,X)) f(g(P,a),h(b,g(Q,Q))) 38 Execution of Prolog Programs Unification: variable bindings. Backward Chaining/ Top-Down Reasoning/ Goal-Directed Reasoning: Reduces a goal to one or more subgoals. Backtracking: Systematically searches for all possible solutions that can be obtained via unification and backchaining. Prolog Search Trees Encapsulate unification, backward chaining, and backtracking. Internal nodes are ordered list of subgoals. Leaves are success nodes or failures, where computation can proceed no further. Edges are labeled with variable bindings that occur by unification. Describe all possible computation paths. There can be many success nodes. There can be infinite branches. 40 Prolog Search Trees 1) male(charlie). 5) parent(charlie,bob). 2) male(bob). 6) parent(eve,bob). 3) female(alice). 7) parent(charlie,alice). 4) female(eve). 8) parent(eve,alice). 9) sibling(X, Y) :- parent(P, X), parent(P, Y). ?- sibling(alice, Who). Who = bob ; Who = alice ; Who = bob ; Who = alice. Prolog Search Trees Trace it by hand Trace it with gtrace (or trace). sib(al,W) 9/X=al,Y=W p(P,al),p(P,W) fail 7/P=ch 8/P=eve p(ch,W) p(eve,W) fail 5/W=bob 6/W=bob 7/W=al 8/W=al success success fail success success fail 42 Logic Programming vs. Prolog Logic Programming: nondeterministic: Arbitrarily choose rule to expand first. Arbitrarily choose subgoal to to explore first. Results don’t depend on rule and subgoal ordering. Prolog: deterministic: Expand first rule first. Explore first subgoal first. Results may depend on rule and subgoal ordering. 43 Syntax of Lists in Prolog A Prolog list is: [] the empty list, or [Head|Tail] a list with first element Head and rest of the elements list Tail Luckily, we abbreviate [ e1 | [ e2 | [... en ]]] as [e1 , e2 ,... en ] Lists in Prolog List Unification: two lists unify iff they have the same structure and the corresponding elements unify. ?- [X, Y, Z] = [john, likes, fish]. ?- [cat] = [X|Y]. ?- [1,2] = [X|Y]. 45 Lists in Prolog ?- [a,b,c] = [X|Y]. ?- [a,b|Z]=[X|Y]. ?- [X,abc,Y]=[X,abc|Y]. ?- [[the|Y]|Z] = [[X,hare] | [is,here]]. 46 Lists in Prolog % member(?X,?List) iff X is an element of List member(X,[X|_]). member(X,[_|Rest]):-member(X,Rest). ?- member(a, [a,b,c]). true ?- member(b, [a,c]). false. ?- member(X, [a,b,c]). X = a ; X = b ; X = c ; false. ?- member(a, X). X = [a|_] ; X = [_, a|_] ; X = [_, _, a|_] Lists in Prolog [trace] ?- member(c,[a,b,c,d]). Call: (7) member(c, [a, b, c, d]) ? Call: (8) member(c, [b, c, d]) ? Call: (9) member(c, [c, d]) ? Exit: (9) member(c, [c, d]) ? Exit: (8) member(c, [b, c, d]) ? Exit: (7) member(c, [a, b, c, d]) ? true Lists in Prolog [trace] ?- member(X,[a,b,c,d]). Call: (7) member(_G314, [a, b, c, d]) ? Exit: (7) member(a, [a, b, c, d]) ? X = a ; Redo: (7) member(_G314, [a, b, c, d]) ? Call: (8) member(_G314, [b, c, d]) ? Exit: (8) member(b, [b, c, d]) ? Exit: (7) member(b, [a, b, c, d]) ? X = b ; Redo: (8) member(_G314, [b, c, d]) ? Call: (9) member(_G314, [c, d]) ? Exit: (9) member(c, [c, d]) ? Exit: (8) member(c, [b, c, d]) ? Exit: (7) member(c, [a, b, c, d]) ? Lists in Prolog X = c ; Redo: (9) member(_G314, [c, d]) ? Call: (10) member(_G314, [d]) ? Exit: (10) member(d, [d]) ? Exit: (9) member(d, [c, d]) ? Exit: (8) member(d, [b, c, d]) ? Exit: (7) member(d, [a, b, c, d]) ? X = d ; Redo: (10) member(_G314, [d]) ? Call: (11) member(_G314, []) ? Fail: (11) member(_G314, []) ? false Lists in Prolog % append(?X,?Y,?Z) iff Z is the result of % appending list Y to list X append([],Y,Y). append([H|T],Y,[H|Z]):-append(T,Y,Z). ?- append([a],[b,c],Y). Y = [a, b, c]. ?- append(X,[b,c],[a,b,c]). X = [a] ; false ?- append(X,Y,[a,b,c]). X = [], Y = [a, b, c] ; X = [a], Y = [b, c] ; X = [a, b], Y = [c] ; X = [a, b, c], Y = [] ; false Lists in Prolog [trace] ?- append([a,b,c],[d,e],Z). Call: (7) append([a, b, c], [d, e], _G319) ? Call: (8) append([b, c], [d, e], _G385) ? Call: (9) append([c], [d, e], _G388) ? Call: (10) append([], [d, e], _G391) ? Exit: (10) append([], [d, e], [d, e]) ? Exit: (9) append([c], [d, e], [c, d, e]) ? Exit: (8) append([b, c], [d, e], [b, c, d, e]) ? Exit: (7) append([a, b, c], [d, e], [a, b, c, d, e]) ? Z = [a, b, c, d, e]. Lists in Prolog % mylength(?L,?N) iff N is the length of list L mylength([],0). mylength([_|T],N):-mylength(T,N-1). ?- mylength([a,b,c],3). false. Huh? [trace] ?- mylength([a,b,c],3). Call: (7) mylength([a, b, c], 3) ? Call: (8) mylength([b, c], 3-1) ? Call: (9) mylength([c], 3-1-1) ? Call: (10) mylength([], 3-1-1-1) ? Fail: (10) mylength([], 3-1-1-1) ? Fail: (9) mylength([c], 3-1-1) ? Fail: (8) mylength([b, c], 3-1) ? Fail: (7) mylength([a, b, c], 3) ? false. 53 Arithmetic in Prolog What is the result of these queries: ?- X = 97-65, Y = 32-0, X = Y. ?- X = 97-65, Y = 67, Z = 95-Y, X = Z. To evaluate arithmetic expressions is Prolog, use: expr 1 is expr 2, where expr 2 is fully instantiated; if expr 1 is a variable, it is bound to the result of evaluating expr 2 expr 1 < expr 2 or expr 1 > expr 2, where both expr 1 and expr 2 are instantiated 54 Arithmetic in Prolog ?- 5 is 2+3. true. ?- X is 2+3. X = 5. ?- 5 < 6. true. ?- 2+3 < 3+3. true. 55 Arithmetic in Prolog % mylength(?L,?N) iff N is the length of list L mylength([],0). mylength([_|T],N):-N is NT+1, mylength(T,NT). ?- mylength([a,b,c],3). ERROR: is/2: Arguments are not sufficiently instantiated ^ Exception: (8) 3 is _G226+1 ? Why? [trace] ?- mylength([a,b,c],3). Call: (7) mylength([a, b, c], 3) ? ^ Call: (8) 3 is _G358+1 ? ERROR: is/2: Arguments are not sufficiently instantiated ^ Exception: (8) 3 is _G358+1 ? Exception: (7) mylength([a, b, c], 3) ? 56 Arithmetic in Prolog % mylength(?L,?N) iff N is the length of list L mylength([],0). mylength([_|T],N):-mylength(T,NT), N is NT+1. ?- mylength([a,b,c],3). true 57 Lists in Prolog How? [trace] ?- mylength([a,b,c],3). Call: (8) mylength([a, b, c], 3) ? Call: (9) mylength([b, c], _L193) ? Call: (10) mylength([c], _L212) ? Call: (11) mylength([], _L231) ? Exit: (11) mylength([], 0) ? ^ Call: (11) _L212 is 0+1 ? ^ Exit: (11) 1 is 0+1 ? Exit: (10) mylength([c], 1) ? ^ Call: (10) _L193 is 1+1 ? ^ Exit: (10) 2 is 1+1 ? Exit: (9) mylength([b, c], 2) ? ^ Call: (9) 3 is 2+1 ? ^ Exit: (9) 3 is 2+1 ? Exit: (8) mylength([a, b, c], 3) ? true 58 Lists in Prolog % mylength(?L,?N) iff N is the length of list L mylength([],0). mylength([_|T],N):-mylength(T,NT), N is NT+1. ?- mylength([a,b,c], L). L = 3. ?- mylength([X,Y], L). L = 2. ?- mylength(X, 3). X = [_G226, _G229, _G232] ;