Into to Prolog

Download Report

Transcript Into to Prolog

Introduction to Prolog
What if all we could do was to make assertions
(statements) about the world?


Example: family tree
parent(linda, simon).
male(simon).
parent(linda, sharon).
female(sharon).
parent(sam, simon).
male(sam).
parent(sam, sharon).
female(linda).
parent(bertha, sam).
female(bertha).
parent(alfred, linda).
male(alfred).
We also want to ask questions about facts:
-bash-3.00$ gprolog
| ?- consult(levytree).
% open levytree.pl
| ?- female(sharon).
% Is Sharon female?
yes
| ?- parent(Who, simon).
% variables in upper-case!
Who = linda;
% Anyone else?
Who = sam;
% Anyone else?
no
| ?- halt.
-bash-3.00$
Finally, we need rules to relate facts:
mother(M,C) :- parent(M,C), female(M).
sister(S,X) :- parent(P,S), parent(P,X),
female(S).
| ?- sister(Who, simon).
Who = sharon;
Who = sharon;
no
| ?-
% Why twice?

This paradigm (approach) is called logic programming or
logic-oriented programming.

Obviously useful for databases!

But also Turing-equivalent; e.g.:
fac(0, 1).
fac(N, F) :N > 0,
N1 is N-1,
% like “let N1 = N-1”
fac(N1, F1),
F is N * F1.
Prolog: Under the Hood

Prolog: non-determinism (guessing) with backtracking
(back up to where you made the wrong guess)

Recall family-tree example:
parent(linda, simon).
parent(sam, simon).
male(sam).
father(F, C) :- parent(F, C), male(F).

Consider the query
| ?- father(Who, simon).
1) father(Who, simon) expands to the goals
parent(Who, simon) and male(Who).
2) parent(Who, simon) is satisfied by
parent(linda, simon), with Who bound to linda.
3) So male(Who) becomes male(linda), the next goal.
4) But the database doesn't contain this fact, so we assume
it's false: negation by failure (closed-world hypothesis).
5) So we unbind Who from linda, and back-track to the
rule immediately after parent(linda,simon).
6) This rule is parent(sam, simon), so we continue with
Who bound to sam.
7) So male(Who) becomes male(sam), the next goal.
8) This goal is eventually satisfied, completing the “proof”
of father(Who, simon), with Who bound to sam.
Recall unification algorithm for type inference (Chapter 4):
Unification: check-equal-type!(t1,t2)
• If t1 and t2 are same Scheme value (e.g., 7), succeed
with unspecified return value.
• If t1 (t2) is a type var, check that it is the same variable
type as t2 (t1) (and bind to constant if possible)
• If t1 and t2 are atomic types (bool, int), suceed if they
have the same name; else fail.
• If t1 and t2 are procedure types, check # of args equal
and recur on args.
• Otherwise, fail.
Unification : Prolog
• If t1 and t2 are same value (e.g., linda ), succeed.
• If t1 (t2) is a variable, bind it to the value of t2 (t1) .
• If t1 and t2 are predicates , check # of args equal and
recur on predicates and args.
• Otherwise, fail.
?- f(A,B) = f(3,4).
A = 3
B = 4
yes