Transcript PS12

Logic Programming: Introduction
o A procedure: a set of axioms (rules and facts) with identical signature (predicate symbol and arity).
o A logic program: a set of procedures (predicates), defining relations in the program domain.
procedure
program
predicate
Signature: parent (Parent, Child) /2
Purpose: Parent is a parent of Child
1. parent (erik, jonas).
2. parent (lena, jonas).
Signature: male(Person) /1
Purpose: Person is a male
1. male (erik).
arity
fact
rule
axioms
Signature: father (Dad, Child) /2
Purpose: Dad is father of Child
1. father (Dad, Child) :- parent(Dad, Child) , male (Dad).
The relation father holds between Dad and Child
1
if
parent holds
and
Dad is male
Logic Programming: Introduction
The prolog interpreter operates in a read-eval-print loop. Given a query, it attempts to prove it
based on the program:
o If it fails, it answers false.
o Else, if the query has no variables, it answers true.
o Else, it outputs all possible variables assignments found during proof process.
% Signature: parent (Parent, Child) /2
% Purpose: Parent is a parent of Child
parent (erik, jonas).
parent (lena, jonas).
% Signature: male(Person) /1
% Purpose: Person is a male
male (erik).
% Signature: father (Dad, Child) /2
% Purpose: Dad is father of Child
father (Dad, Child) :- parent(Dad, Child), male (Dad).
2
? - father (X,Y).
X=erik, Y=jonas
? - parent (X,jonas).
X=erik ;
X=lena
query
Next possible
assignment
Logic Programming: Example 1 – logic circuits
An electronic logic circuit combines:
o Logic gates: resistor, transistor. Implement simple logic functions.
o Connection points: connects one logic gate to another, or to power or ground.
A program that models electronic logic circuits:
o Connection points: are individual constants.
o Logic gates: are relations on the constants.
Power
Resistor
(symmetric)
Power
Connection
point
N1
Transistor
(asymmetric)
N2
Ground
N3
N4
Ground
3
N5
% Signature: transistor
resistor(End1,End2)/2
(Gate, Source, Drain)/3
% Purpose: A
… resistor component connects two ends
1
resistor(power, n1).
transistor(n2,ground,n1).
2
resistor(power, n2).
transistor(n3,n4,n2).
3
resistor(n1, power).
transistor(n5,ground,n4).
4
resistor(n2, power).
Note: In contrast resistor, the arguments order in
transistor is important. Each has a different role.
Logic Programming: Example 1 – logic circuits
% Signature: resistor(End1,End2)/2
End1,End2
% Purpose:
Purpose A resistor component connects two ends
1
resistor(power, n1).
2
resistor(power, n2).
3
resistor(n1, power).
4
resistor(n2, power).
Reminders…
o A procedure begins with a contract.
o Constants start with lowercase characters.
terms
o A predicate name is also a constant, which defines a relation between its arguments.
o variables start with uppercase characters (‘_’ for wildcard).
o Atomic formulas are either true, false or of the form predicate(t1 , ..., tn), ti is a term.
o A rule is a formula defining a relation that depends on certain conditions.
o A fact is an atomic formula which is unconditionally true.
4
Logic Programming: Example 1 – logic circuits
% Signature: resistor(End1,End2)/2
End1,End2
% Purpose:
Purpose A resistor component connects two ends
1
resistor(power, n1).
2
resistor(power, n2).
3
resistor(n1, power).
4
resistor(n2, power).
Reminders…
o A query is a sequence of atomic formulas that require a proof:
?- resistor(power, n1),resistor(n2, power).
true;
false
No more answers
“Does an X exists such that the resistor relation holds for (power, X)?”
?- resistor(power, X).
X = n1 ;
Is there another answer?
X = n2;
false
5
Logic Programming: Example 1 – logic circuits
Combining logic gates to create a “not” logic circuit:
o The resistor and transistor relations are based on facts.
o The relations can be combined by a rule to determine whether or not the not_circuit
relation stands for Input and Output.
power
resistor
Output
transistor
Input
ground
6
Logic Programming: Example 1 – logic circuits
Combining logic gates to create a NOT logic circuit:
% Signature: not_circuit(Input, Output)/2
% Purpose: not logic circuit.
1. not_circuit(Input, Output) :- transistor(Input, ground, Output) ,
2.
resistor(power, Output).
Rule head: an atomic formula with variables
“and”
Rule body
power
resistor
Output
transistor
Input
ground
“For all Input and Output:
(Input, Output) stands in the relation not_circuit if:
• (Input, ground, Output) stand in the relation transistor and
• (power, Output) stand in the relation resistor.”
7
?- not_circuit(X,Y).
X=n2,
Y=n1;
false
Logic Programming: Example 1 – logic circuits
Combining logic gates to create a NAND logic circuit:
% Signature: nand_circuit(Input1, Input2, Output)/3
% Purpose: nand logic circuit
nand_circuit(Input1, Input2, Output) :transistor(Input1, X, Output),
transistor(Input2, ground, X),
resistor(power, Output).
?- not_circuit(X, Y), nand_circuit(In1, In2, X).
X = n2,
Y = n1,
Power
In1 = n3,
In2 = n5;
N1
false
Power
Connection
point
N2
Ground
N3
N4
Ground
8
N5
Semantics: Unification algorithm
A program execution is triggered by a query in attempt to prove it goals:
o To find a possible proof, the answer-query algorithm is used.
o It makes multiple attempts to apply rules on a selected goal.
o This is done by applying a unification algorithm, Unify, to the rule head
and the goal.
9
Semantics: Unification algorithm
Definitions:
1. binding: a non-circular expression, X=t, where X is a variable and t is a term not including X.
2. Substitution: a function from a finite set of variables to a finite set of terms (or a finite set of
bindings).
3. Application (º) of a substitution S to an atomic formula A replaces variables in A with
corresponding terms in S (the result is an instance of A). For example:
S = {J=X}
A = not_circuit(J, J) , A º S = not_circuit(X, X)
B = not_circuit(X,Y) , B º S = not_circuit(X, Y)
4. Unifier: a substitution S is called a unifier of formulas A and B if A º S = B º S. For example:
S = {J=X} º {X=Y} = {J=Y, X=Y}
A º S = not_circuit(Y, Y)
B º S = not_circuit(Y, Y)
The algorithm Unify receives two atomic formulas and returns their most general unifier.
S = {J=5, X=5, Y=5} is a unifier for A and B, but not the most general one.
10
Semantics: Proof trees
Executing answer-query:
o The interpreter searches for a proof for a given query (a conjunction of goals).
o The search is done by building and traversing a proof tree where all possibilities are examined.
o The possible outcome is one of the following:
 The algorithm finishes, and possible values of the query variables are given.
 The algorithm finishes, but there is no proof for the query (false).
 The proof attempt loops and never ends.
12
Semantics: Proof trees
The tree structure depends on Prolog's goal selection and rule selection policies:
1. Query goals (Q1,…,Qn) are at the root of the proof tree.
Q = ?- Q1, ..., Qn
2. Choose current goal (atomic formula). Prolog's policy: the leftmost goal.
3. Choose current rule to prove current goal. (top to bottom program order).
4. Rename the variables in the rule and unify the rule head with the goal.
If unification succeeds:
1. A new child node is created.
2. The query for this node is the rule body.
5. A leaf may be created if the goal list is empty (success), or if the goal cannot be proven (failure).
6. Backtracking: When a leaf is reached, the search travels up to the first parent node where another
rule can be matched.
13
Semantics: Example 2 – A generated proof tree
?- nand_circuit(In1, In2, Out).
nand_circuit(Input1,Input2,Output) :transistor(Input1,X,Output),
transistor(Input2,ground,X),
resistor(power, Output).
nand_circuit(In1, In2, Out)
mgu
{ Input1_1 = In1, Input2_1 = In2,
Output_1 = Out }
Rule 1
transistor(In1, X_1, Out),
transistor(In2, ground, X_1),
resistor(power, Out)
{ In1=n2, X_1=ground, Out=n1}
{ In1=n3, X_1=n4, Out=n2}
Fact 1 – transistor
Fact 2 – transistor
transistor(In2,ground,ground),
resistor(power, n1)
{In2=n2}
Fact 1 –
transistor
fail
transistor(In2,ground,n4),
resistor(power, n2)
{ In2=n5}
{ In2=n3} Fact 3 –
Fact 2 –
transistor
transistor
fail
fail
transistor (Gate, Source, Drain) :transistor(n2,ground,n1).
transistor(n3,n4,n2).
transistor(n5,ground,n4).
{ In1=n5, X_1=ground,
Out=n4}
Fact 2 – transistor
transistor(In2,ground,ground),
resistor(power, n2)
{ In2=n2}
{ In2=n5}
{ In2=n3}
Fact 1 –
Fact 3 –
Fact 2 –
transistor
transistor
transistor
fail
fail
a finite success tree
resistor(power, n2)
true
14
resistor(End1,End2) :resistor(power, n1).
resistor(power, n2).
resistor(n1, power).
resistor(n2, power).
with one success path.
Semantics: proof trees
Possible types of proof trees:
o A success tree has at least one success path in it.
o A failure tree is one in which every path is a failure path.
o A proof tree is an infinite tree if it contains an infinite path.
o Otherwise, it is a finite tree.
Example:
An infinite is generated by repeatedly applying the rule p(X):-p(Y),q(X,Y) (left recursion).
To avoid the infinite path, we could rewrite the rule: p(X):- q(X,Y),p(Y) (tail recursion).
15
Semantics:
Example
3 – SQLlogic
in Relational
Logic Programming
An
example:
Relational
programming
& SQL operations.
o
Relations may be regarded as tables in a database of facts.
o
Recall the resistor and transistor relations presented earlier:
Table name: resistor
Schema: End1,
End2
Data:
(power, n1),
(power, n2),
(n1,
power),
(n2,
power).
Table name: transistor
Schema: Gate, Source, Drain
Data: (n2, ground,
n1)
(n3, n4,
n2),
(n5, ground,
n4).
SQL Operation: Natural join
% Signature: res_join_trans(End1, X, Gate, Source)/4
% Purpose: Join between resistor and transistor
%
according to End2 of resistor and Gate of transistor.
res_join_trans(End1, X, Source, Drain):resistor(End1,X),
transistor(X, Source, Drain).
16
?-res_join_trans(End1,X,Source,Drain).
End1
X
Source
Drain
false.
= power,
= n2,
= ground,
= n1 ;
Semantics:
Example
3 – SQLlogic
in Relational
Logic Programming
An
example:
Relational
programming
& SQL operations.
o
Relations may be regarded as tables in a database of facts.
o
Recall the resistor and transistor relations presented earlier:
Table name: resistor
Schema: End1,
End2
Data:
(power, n1),
(power, n2),
(n1,
power),
(n2,
power).
Table name: transistor
Schema: Gate, Source, Drain
Data: (n2, ground,
n1)
(n3, n4,
n2),
(n5, ground,
n4).
Transitive closure for the resistor relation
%Signature: res_closure(X, Y)/2
res_closure(X, Y) :- resistor(X, Y).
res_closure(X, Y) :- resistor(X, Z), res_closure(Z, Y).
The resistor relation is symmetric. Therefore, we get a finite
series of answers repeated an infinite number of times.
17
?- res_closure(X, Y).
X = power,
Y = n1 ;
X = power,
Y = n2 ;
X = n1,
Y = power ;
X = n2,
Y = power ;
X = power ,
Y = power ;
X = power,
Y = n1 ;
X = power,
Y = n2 ;
X = power,
Y = power ;
X = power,
Y = n1;
...
Fullexample:
Logic Programming
An
Relational logic programming & SQL operations.
o
Relational logic programming has no ability to describe composite data, only atoms.
o
Full logic programming is equipped with functors to describe composite data.
Q: In the following procedure, which symbols are predicates? Which are functors?
% Signature: tree_member(Element,Tree)/ 2
% Purpose: Testing tree membership, checks if Element is an element of the binary tree Tree.
tree_member (X,tree(X,Left,Right)).
tree_member (X,tree(Y,Left,Right)):- tree_member(X,Left).
tree_member (X,tree(Y,Left,Right)):- tree_member(X,Right).
Predicate
A Functor applied to three data items.
Q: how can you tell? by their relative location in the program:
• A predicate appears as an identifier of an atomic formula.
• A functor is way to construct a term. A term is a part of a formula.
• A functor can be nested – a predicate cannot.
NOTE: The same name may be used for both a predicate and a functor!
18
Fullexample:
Logic Programming:
with functors& SQL operations.
An
RelationalUnification
logic programming
Unification is more complex with functors. Here is an execution of the Unify algorithm, step by step:
Unify(A,B) where A = tree_member (tree (X, 10, f(X)), W) ; B = tree_member (tree (Y, Y, Z), f(Z)).
Initially, s={}
As= tree_member (tree (X, 10, f(Y)), W )
Bs= tree_member (tree (Y, Y , Z ), f(Z))
As ≠ Bs
 Disagreement-set = {X=Y}
 X does not occur in Y
 s=s  {X=Y} = {X=Y}
As= tree_member (tree (Y, 10, f(Y)), W )
Bs= tree_member (tree (Y, Y ,Z ), f(Z))
As ≠ Bs
 Disagreement-set = {Y=10}
 s=s  {Y=10} = {X=10, Y=10}
As= tree_member (tree (10, 10, f(10)), W )
Bs= tree_member (tree (10, 10, Z ), f(Z))
As ≠ Bs
 Disagreement-set = {Z=f(10)}
 s=s  {Z=f(10)} = {X=10, Y=10, Z=f(10)}
As= tree_member (tree (10, 10, f(10)), W )
As ≠ Bs
Bs= tree_member (tree (10, 10, f(10)), f(f(10)))
 Disagreement-set = {W=f(f(10))}
 s={X=10, Y=10, Z=f(10), W=f(f(10))}
As= tree_member (tree (10, 10, f(10)), f(f(10)) )
Bs= tree_member (tree (10, 10, f(10)), f(f(10)))
Q: Why do we check for occurence?
19
Fullexample:
Logic Programming:
with functors& SQL operations.
An
RelationalUnification
logic programming
A: Consider the following two atomic formulas:
A = tree_member (tree (X, Y, f(X)), X )
B = tree_member (tree (Y, Y, Z ), f(Z))
Applying Unify(A,B) will result in a loop: X=Y, Z=f(Y), Y=f(Z)=f(f(Y))…
the substitution cannot be successfully solved.
20
Full Logic Programming:
Example queries
% Signature: tree_member(Element,Tree)/ 2
% Purpose: Testing tree membership, checks if Element is
%
an element of the binary tree Tree.
tree_member (X,tree(X,Left,Right)).
tree_member (X,tree(Y,Left,Right)):- tree_member(X,Left).
tree_member (X,tree(Y,Left,Right)):- tree_member(X,Right).
?- tree_member(1, tree(1,nil, nil)).
true
?- tree_member(2,tree(1,tree(2,nil,nil), tree(3,nil, nil))).
true.
?- tree_member(1, tree(3,1, 3)).
false.
?- tree_member(X,tree(1,tree(2,nil,nil), tree(3,nil, nil))).
X=1;
X=2;
X=3;
false.
21
Full Logic Programming:
An example proof tree
?- tree_member(X, tree(1, tree(2, nil, nil), tree(3, nil, nil))).
tree_member(X, tree(1, tree(2, nil, nil), tree(3, nil, nil)))
{X_1 = 1, X = 1
Left_1 = tree(2,nil,nil,
Right_1 = tree(3, nil, nil)}
{X_1 = X, Y_1 = 1,
Left_1 = tree(2,nil,nil),
Right_1 = tree(3, nil, nil)}
{X_1 = X, Y_1 = 1,
Left_1 = tree(2,nil,nil),
Right_1 = tree(3, nil, nil)}
tree_member (X, tree(3,nil,nil))
tree_member (X, tree(2,nil,nil))
{X_2 = 2, X = 2
{X_2 = X, Y_2 = 2,
{X_2 = X, Y_2 = 2,
Left_2 = nil,
Left_2 = nil, Right_2 = nil} Left_2 = nil, Right_2 = nil}
Right_2 = nil}
tree_member (X, nil)
tree_member (X, nil)
true
{X=1}
true
{X=2}
fail
% Signature: tree_member(Element,Tree)/ 2
%…
tree_member (X,tree(X,Left,Right)).
tree_member (X,tree(Y,Left,Right)):tree_member(X,Left).
tree_member (X,tree(Y,Left,Right)):tree_member(X,Right).
22
fail
{X_2 = 3, X = 3
Left_2 = nil,
Right_2 = nil}
true
{X_2 = X, Y_2 = 3,
Left_2 = nil,
Right_2 = nil}
tree_member (X, nil)
{X_2 = X, Y_2 = 3,
Left_2 = nil,
Right_2 = nil}
tree_member (X, nil)
{X=3}
fail
fail
Full Logic Programming:
An example proof tree
% Signature: tree_member(Element,Tree)/ 2
% Purpose: Testing tree membership, checks if Element is
%
an element of the binary tree Tree.
tree_member (X,tree(X,Left,Right)).
tree_member (X,tree(Y,Left,Right)):- tree_member(X,Left).
tree_member (X,tree(Y,Left,Right)):- tree_member(X,Right).
?- tree_member(1, T).
T = tree(1, _G445, _G446) ;
T = tree(_G444, tree(1, _G449, _G450), _G446) ;
T = tree(_G444, tree(_G448, tree(1, _G453, _G454), _G450), _G446) ;
...
o Looking for all trees in which 1 is a member, we get an infinite success tree
with partially instantiated answers (containing variables).
o We use a rule that requires a defined input, but our input is a variable.
Possible answers are generated by the proof algorithm.
o In this case we call the rule a generator rule.
23