Transcript Full Logic Programming

Full Logic Programming
Data structures
• Pure LP allows only to represent relations
(=predicates)
• To obtain full LP we will add functors
(=function symbols)
• This will allow us to represent data structures
Data structures
• Pure LP allows only to represent relations
(=predicates)
• To obtain full LP we will add functors (=function
symbols)
• This will allow us to represent data structures
• In particular, functors can be nested
Data structures
• Pure LP allows only to represent relations
(=predicates)
• To obtain full LP we will add functors (=function
symbols)
• This will allow us to represent data structures
• In particular, functors can be nested
Functor examples
cons(a,[ ]) describes the list [a].
[ ] is an individual constant, standing for the empty list .
The cons functor has a syntactic sugar notation as an inx
operator |:
• cons(a,[ ]) is written: [a|[ ]].
• cons(b,cons(a,[ ])) the list [b,a], or [b|[a|[ ]]]. The
syntax [b,a] uses the
• printed form of lists in Prolog.
• tree(Element,Left,Right) a binary tree, with Element as
the root, and Left and Right as its sub-trees.
• tree(5,tree(8,void,void),tree(9,void,tree(3,void,void)))
Capturing natural number
arithmetics
•
•
•
•
•
1. Definition of natural numbers:
% Signature: natural_number(N)/1
% Purpose: N is a natural number.
natural_number(0).
natural_number(s(X)) :- natural_number(X).
Addition and substraction
•
•
•
•
•
•
•
•
•
•
•
•
•
% Signature: Plus(X,Y,Z)/3
% Purpose: Z is the sum of X and Y.
plus(X, 0, X) :- natural_number(X).
plus(X, s(Y), s(Z)) :- plus(X, Y, Z).
?- plus(s(0), 0, s(0)). /* checks 1+0=1
Yes.
?- plus(X, s(0), s(s(0)). /* checks X+1=2, e.g., minus
X=s(0).
?- plus(X, Y, s(s(0))). /* checks X+Y=2, e.g., all pairs of natural
numbers, whose sum equals 2
X=0, Y=s(s(0));
X=s(0), Y=s(0);
X=s(s(0)), Y=0.
Less or Equal
•
•
•
•
% Signature: le(X,Y)/2
% Purpose: X is less or equal Y.
le(0, X) :- natural_number(X).
le(s(X), s(Z)) :- le(X, Z).
Multiplication
•
•
•
•
% Signature: Times(X,Y,Z)/2
% Purpose: Z = X*Y
times(0, X, 0) :- natural_number(X).
times(s(X), Y, Z) :- times(X, Y, XY), plus(XY, Y, Z).
Implications
• Pure LP can’t capture unbounded arithmetics.
• It follows that full LP is strictly more expressible than pure LP
– In facts full LP is as expressible as Turing Machines
• Full LP is undecidable
– In RE: if there is a proof we will find it, but if not we may fail to
terminate
• Proofs may be of unbounded size since unification may generate
new symbols through repeated substitutions of variables x with f(y).
Data Structures
% Signature: binary_tree(T)/1
% Purpose: T is a binary tree.
binary_tree(void).
binary_tree(tree(Element,Left,Right)) :binary_tree(Left),binary_tree(Right).
% Signature: tree_member(X, T)/2
% Purpose: X is a member of T.
tree_member(X, tree(X, _, _)).
tree_member(X, tree(Y,Left, _)):- tree_member(X,Left).
tree_member(X, tree(Y, _, Right)):- tree_member(X,Right).
Lists
• Syntax:
• [ ] is the empty list .
• [Head|Tail] is a syntactic sugar for cons(Head, Tail), where Tail is a
list term.
• Simple syntax for bounded length lists:
• [a|[ ]] = [a]
• [a|[ b|[ ]]] = [a,b]
• [rina]
• [sister_of(rina),moshe|[yossi,reuven]] =
[sister_of(rina),moshe,yossi,reuven]
• Defining a list:
• list([]). /* defines the basis
• list([X|Xs]) :- list(Xs). /* defines the recursion
Lists
• Syntax:
• [ ] is the empty list .
• [Head|Tail] is a syntactic sugar for cons(Head, Tail), where Tail is a
list term.
• Simple syntax for bounded length lists:
• [a|[ ]] = [a]
• [a|[ b|[ ]]] = [a,b]
• [rina]
• [sister_of(rina),moshe|[yossi,reuven]] =
[sister_of(rina),moshe,yossi,reuven]
• Defining a list:
• list([]). /* defines the basis
• list([X|Xs]) :- list(Xs). /* defines the recursion
List membership:
•
•
•
•
% Signature: member(X, List)/2
% Purpose: X is a member of List.
member(X, [X|Xs]).
member(X, [Y|Ys]) :- member(X, Ys)
List membership:
•
•
•
•
% Signature: member(X, List)/2
% Purpose: X is a member of List.
member(X, [X|Xs]).
member(X, [Y|Ys]) :- member(X, Ys)
Append
• append([], Xs, Xs).
• append([X|Xs], Ys, [X|Zs] ) :• append(Xs, Ys, Zs).
• ?- append([a,b], [c], X).
• ?- append(Xs, [a,d], [b,c,a,d]).
• ?- append(Xs, Ys, [a,b,c,d]).
Append
• append([], Xs, Xs).
• append([X|Xs], Y, [X|Zs] ) :- append(Xs, Y, Zs).
• ?- append([a,b], [c], X).
• ?- append(Xs, [a,d], [b,c,a,d]).
• ?- append(Xs, Ys, [a,b,c,d]).
Reverse
reverse([], []).
reverse([H|T], R) :reverse(T, S), append(S, [H], R).
OR
reverse(Xs, Ys):- reverse_help(Xs,[],Ys).
reverse_help([X|Xs], Acc, Ys ) :reverse_help(Xs,[X|Acc],Ys).
reverse_help([ ],Ys,Ys ).