82 lines
2.2 KiB
Prolog
82 lines
2.2 KiB
Prolog
% Peano axioms in Prolog
|
|
%% Definition of a natural number
|
|
nat(o).
|
|
nat(succ(N)) :- nat(N).
|
|
|
|
%% Operations
|
|
|
|
add(X, o, X) :- nat(X), !. % X + o = X
|
|
add(X, succ(Y), succ(R)) :- add(X, Y, R). % X + succ(Y) = X + Y
|
|
|
|
mul(X, o, o) :- nat(X), !. % X * o = o
|
|
mul(X, succ(Y), R) :- % X * succ(Y) = X + (X * Y)
|
|
mul(X, Y, Tmp),
|
|
add(X, Tmp, R).
|
|
|
|
% https://math.stackexchange.com/a/461959
|
|
sub(X, o, X) :- nat(X), !. % X - o = X
|
|
sub(succ(X), succ(Y), R) :- sub(X, Y, R). % succ(X) - succ(Y) = X - Y
|
|
% sub(succ(succ(o)), succ(o), R)
|
|
% sub(succ(o), o, R)
|
|
% nat(succ(o))
|
|
% R = succ(o)
|
|
|
|
fact(N, R) :- fact(N, succ(o), R).
|
|
fact(o, R, R) :- !.
|
|
fact(N, Acc, R) :-
|
|
sub(N, succ(o), NN),
|
|
mul(Acc, N, AccN),
|
|
fact(NN, AccN, R).
|
|
|
|
peano2dec(N, R) :- peano2dec(N, 0, R).
|
|
peano2dec(o, R, R) :- !.
|
|
peano2dec(N, C, R) :- % "list length"
|
|
sub(N, succ(o), NN), % cdr
|
|
CC is C + 1,
|
|
peano2dec(NN, CC, R).
|
|
|
|
dec2peano(N, R) :- dec2peano(N, o, R).
|
|
dec2peano(0, R, R) :- !.
|
|
dec2peano(N, Acc, R) :- % "list of N elements"
|
|
add(Acc, succ(o), AccX), % cons
|
|
NN is N - 1,
|
|
dec2peano(NN, AccX, R).
|
|
|
|
:- begin_tests(peano).
|
|
|
|
test(addition) :-
|
|
add(o, o, R1), R1 = o,
|
|
add(succ(o), o, R2), R2 = succ(o),
|
|
add(succ(succ(o)), succ(succ(o)), R3), R3 = succ(succ(succ(succ(o)))).
|
|
|
|
test(multiplication) :-
|
|
mul(o, o, R1), R1 = o,
|
|
mul(succ(succ(o)), o, R2), R2 = o,
|
|
Nine = succ(succ(succ(succ(succ(succ(succ(succ(succ(o))))))))),
|
|
mul(succ(succ(succ(o))), succ(succ(succ(o))), R3), R3 = Nine.
|
|
|
|
test(substraction) :-
|
|
sub(o, o, R1), R1 = o,
|
|
sub(succ(succ(succ(o))), succ(succ(o)), R2), R2 = succ(o),
|
|
sub(succ(succ(succ(o))), succ(succ(succ(o))), R3), R3 = o.
|
|
|
|
test(peano_to_decimal) :-
|
|
peano2dec(succ(succ(o)), R1), R1 =:= 2,
|
|
peano2dec(o, R2), R2 =:= 0,
|
|
peano2dec(succ(succ(succ(succ(o)))), R3), R3 =:= 4.
|
|
|
|
test(decimal_to_peano) :-
|
|
dec2peano(3, R1), R1 = succ(succ(succ(o))),
|
|
dec2peano(0, R2), R2 = o,
|
|
dec2peano(4, R3), R3 = succ(succ(succ(succ(o)))).
|
|
|
|
test(factorial_p) :-
|
|
fact(succ(succ(succ(succ(succ(o))))), PR),
|
|
peano2dec(PR, DR),
|
|
DR =:= 120.
|
|
|
|
test(extra) :-
|
|
Num is 5,
|
|
dec2peano(Num, PN), fact(PN, PR), peano2dec(PR, DN), DN =:= 120.
|
|
|
|
:- end_tests(peano).
|