Transcript Logic Programming in 50 Minutes - School of Informatics

Logic Programming in 50 Minutes
The purpose of this lecture is to explain why
logic programming was invented; how it might
be useful to you; and what you need to do to
start programming.
Logic Programming
School of Informatics, University of Edinburgh
1
The Ideal
Every program specification can be written in logic.
Specifications are independent of computers.
Rules of logic can prove the correctness of a
specification even if computers didn’t exist.
But proof can also be done by a computer
smart enough to find the right proof.
nearly
So specifications and programs arethe same.
Logic Programming
School of Informatics, University of Edinburgh
2
Where Has This Worked?
• Symbolic reasoning systems (machine
learning, planning, constraint solving, etc)
• Language systems (parsers, generators, etc)
• Verification systems (theorem provers,
model checkers, etc).
• Multi-agent systems (reactive systems,
performative handling, brokering, etc)
• Web systems (page parsing/generation,
semantic webs)
Logic Programming
School of Informatics, University of Edinburgh
3
Axioms, Assumptions, Goals
ancestor(X, Y)  parent(X, Y).
Your parent is your ancestor.
ancestor(X, Y)  parent(X, Z) &
Your parent’s ancestors are your ancestors.
ancestor(Z, Y).
Given: parent(dave, thomas). parent(dave,helen).
parent(helen, margaret), etc.
We can prove:
 A. ancestor(dave, A)
 B. ancestor(B, margaret)
 A,B. ancestor(B, A)
Logic Programming
School of Informatics, University of Edinburgh
4
Proof Involves Search
 A. ancestor(dave, A)
A=Y
1
3
A=Y
parent(dave, Y)
Y = thomas 2
parent(dave, Z) & ancestor(Z, Y)
5
parent(dave, thomas)
4 Z = helen
parent(helen, Y)
parent(dave, helen)
6
Y = margaret
parent(helen, margaret)
2
4
6
parent(dave, thomas).
parent(dave,helen).
parent(helen, margaret).
1
3
ancestor(X, Y)  parent(X, Y). 5
ancestor(X, Y)  parent(X, Z) &
ancestor(Z, Y).
Logic Programming
School of Informatics, University of Edinburgh
5
Practical Problem 1
Not all specifications are executable.
X = X2 is a specification of square root
but doesn’t compute square roots.
We need to write specifications with an
understanding of their future use.
Logic Programming
School of Informatics, University of Edinburgh
6
Practical Problem 2
Proof mechanisms that are unsophisticated
can easily be fooled.
e.g. Prolog has trouble with this:
Given: p(X)  p(Y) & q(Y,X).
p(1).
q(1,2).
Prove: p(1).
Proof mechanisms that are sophisticated are
difficult to operate as programming systems.
Logic Programming
School of Informatics, University of Edinburgh
7
Practical Problem 3
Some computable specifications consume a lot
of resource before giving an answer.
e.g. Prolog has trouble with this:
Given: p  is_integer(X) & X > 100000.
is_integer(1).
is_integer(N)  is_integer(N1) &
N is N + 1.
Logic programming system designers worry
about efficiency. So must programmers.
Logic Programming
School of Informatics, University of Edinburgh
8
Practical Problem 4
Programmers like to think about closed worlds
so negation often is simplified to “I can’t prove
it true in my current circumstances”.
e.g. Prolog has trouble with this:
Given: p(X) not(q(X)) & r(X).
q(2).
r(1).
Prove: p(X)
Logic Programming
School of Informatics, University of Edinburgh
9
A Logic Program’s Interpretation
ancestor(X, Y)  parent(X, Y).
ancestor(X, Y)  parent(X, Z) &
ancestor(Z, Y).
parent(dave, thomas).
parent(dave,helen).
parent(helen, margaret).
ancestor(dave, thomas).
ancestor(dave,helen).
ancestor(helen, margaret).
ancestor(dave,margaret)
parent(dave, thomas).
parent(dave,helen).
parent(helen, margaret).
Interpretation contains all ground conclusions:
 A1,B1. ancestor(A1, B1)
 A2,B2. parent(A2, B2)
Logic Programming
School of Informatics, University of Edinburgh
10
Everything is a Structured Term
ancestor(X, Y)  parent(X, Y).
ancestor(X, Y)  parent(X, Z) &
ancestor(Z, Y).
parent(dave, thomas).

parent(dave,helen).
parent(helen, margaret). ancestor
parent
dave
thomas
Z
&
Y parent
X
Z
ancestor
Z
Y
Logic Programming
School of Informatics, University of Edinburgh
11
Logic Programs Manipulate Terms
sum(null, 0).
sum(seq(First,Rest), N)  sum(Rest, N1) &
N is N1 + 1.
We can prove:
 N. sum(null, N)
 N. sum(seq(5,null), N)
 N. sum(seq(5,seq(2,null)), N)
and so on….
N=0
N=5
N=9
Logic Programming
School of Informatics, University of Edinburgh
12
Logic Programming Learning Curve
Learning effort
Imperative programming
Logic programming
Time
A crude caricature:
Imperative programmers learn lots of little things
Logic programmers learn one big thing
Logic Programming
School of Informatics, University of Edinburgh
13
Starting to Program in Prolog
sicstus
Unix command to start SICStus Prolog
Goal, using a built-in predicate
| ?- 1 < 2.
which succeeds
yes
Goal, using a built-in logical operator
| ?- not(1 < 2).
which fails
no
| ?- [library(lists)]. Loading definitions from a (library) file
| ?- append([a,b], [c], X). Goal, using a loaded predicate.
X = [a,b,c]
Result of variable binding
Logic Programming
School of Informatics, University of Edinburgh
14
Sources
Books:



Sterling & Shapiro “The Art of Prolog”
Clocksin & Mellish “Prolog Programming”
John Lloyd “Foundations of Logic Programming”
Organisation: Association for Logic Programming
Main conference: International Conference on
Logic Programming
Main journal: Theory and Practice of LP
(pre-2001 main journal was Journal of LP)
Logic Programming
School of Informatics, University of Edinburgh
15