:- module(_,_,[sr/bfall]).
% :- module(_,_,[sr/afall]).
% :- module(_,_,[sr/idall]).

% A real logic program!

% In pure LP, define the naturals, arithmetic 
% operations on them, and the squares of the 
% naturals that are smaller than five.

nat(0).
nat(s(X)) :- nat(X).

le(0,X) :- nat(X).
le(s(X),s(Y)) :- le(X,Y).

add(0,Y,Y) :- nat(Y).
add(s(X),Y,s(Z)) :- add(X,Y,Z).

mult(0,Y,0) :- nat(Y).
mult(s(X),Y,Z) :- mult(X,Y,W), add(W,Y,Z).

nat_square(X,Y) :- nat(X), nat(Y), mult(X,X,Y).

output(X) :- le(Y,s(s(s(s(s(0)))))), nat(Y), nat_square(Y,X).

%  Some examples of queries. Copy on the right, hit 
%  ENTER to execute, and then ; for other solutions.
%  Some may not terminate (this is OK). 
%
%  ?- nat(s(0)).
%  ?- nat(X).
%  ?- add(s(0),s(s(0)),X).
%  ?- add(s(0),X,s(s(s(0)))).
%  ?- add(X,Y,s(0)).
%  ?- nat_square(s(s(0)), X).
%  ?- nat_square(X,s(s(s(s(0))))).
%  ?- nat_square(X,Y).
%  ?- output(X).

%% :- op(100,fy,s).

% Important observation: note that we always get all the correct
% answers. However, after the last answer, we may terminate (answer
% no) or not terminate. See the rest of the slides and examples to
% understand the formal basis for this!