/*
NOTE: integer arithmetic resources
- natural numbers: https://en.wikipedia.org/wiki/Peano_axioms
- successor notation: https://en.wikipedia.org/wiki/Successor_function
*/
% natural_numbers/1
natural_numbers(0).
natural_numbers(s(N)) :-
natural_numbers(N).
% s(0) = 1
% s(s(0)) = 2
% ...
?- natural_numbers(s(0)). % true.
?- natural_numbers(s(s(0))). % true.
% natural_numbers_sum/3
natural_numbers_sum(0, M, M).
natural_numbers_sum(s(N), M, s(Sum)) :-
natural_numbers_sum(M, N, Sum).
% 1 + 1 = 2 -> s(0) + s(0) = s(s(0))
?- natural_numbers_sum(s(0), s(0), s(s(0))).
% true.
% built-in predicates
:- use_module(library(clpfd)).
% equality: (#=)/2
?- 1 #= 1. % true.
% disequality: (#\=)/2
?- 1 #\= 2. % true.
% less than: (#<)/2
?- 1 #< 2. % true.
% greater than: (#>)/2
?- 1 #> 2. % false.
% integer expressions
?- 1 + 2 #= 7 - 4. % true.
?- 1 + 2 #= X - 4. % X = 7.
?- 2 * X #= 5. % false.
?- 2 * X #= 4. % X = 2.
% note: (#=)/2 is not same as (=)/2
?- 1 + 2 = 3. % false.
% domain of variable
?- X #\= 1.
% X in inf..0\/2..sup.
% constrain variable to domain
?- X #= 4, X in 1..2. % false.
?- X #= 2, X in 1..2. % X = 2.
% constrain multiple variables
?- [X, Y] ins 1..2.
% X in 1..2, Y in 1..2.
% labeling: bind a variable to integer in domain
?- X in 0..2, indomain(X).
% X = 0 ;
% X = 1 ;
% X = 2.
?- [X, Y] ins 0..1, label([X, Y]).
% X = Y, Y = 0 ;
% X = 0, Y = 1 ;
% X = 1, Y = 0 ;
% X = Y, Y = 1.
/* EXAMPLE: factorial */
% factorial/2
n_factorial(0, 1).
n_factorial(N, F) :-
% END: then N has factorial F
N #> 0,
% and F is N times F_1
F #= N * F_1,
% and N_1 is N - 1
N_1 #= N - 1,
% START: if N_1 has factorial F_1
n_factorial(N_1, F_1).
?- n_factorial(3, F). % F = 6 .
?- n_factorial(N, 120). % N = 5 .
?- n_factorial(N, F).
% N = 0, F = 1 ;
% N = F, F = 1 ;
% N = F, F = 2 ;
% N = 3, F = 6 ;
% N = 4, F = 24 ;
% N = 5, F = 120
% ...
/* EXAMPLE: length of list */
% list_length/2
list_length([], 0).
list_length([_|Ls], Length) :-
% END: then [_|Ls] has length Length
% and Length is Length_0 + 1
Length #= Length_0 + 1,
% START: if Ls has length Length_0
list_length(Ls, Length_0).
?- list_length([a, b, c, d], Length). % Length = 4.
?- list_length(Ls, 3). % Ls = [_9006, _9172, _9338] .