我在教程中遇到了逻辑数的自然数评估,这让我有些头疼:
natural_number(0).
natural_number(s(N)) :- natural_number(N).
规则大致说:如果
N
是0
它是自然数,如果不是我们尝试将s/1
的内容递归地发送回规则直到内容是0
,那么它是一个自然数如果不是那么它不是。
所以我测试了上面的逻辑实现,心想,如果我想将
s(0)
表示为 1
并将 s(s(0))
表示为 2
,那么这行得通,但我希望能够转换 s(0)
改为1
。
我想到了基本规则:
sToInt(0,0). %sToInt(X,Y) Where X=s(N) and Y=integer of X
所以这是我的问题:如何将 s(0) 转换为 1 并将 s(s(0)) 转换为 2?
已回复
编辑: 我在实施中修改了基本规则,我接受的答案指向我:
decode(0,0). %was orignally decode(z,0).
decode(s(N),D):- decode(N,E), D is E +1.
encode(0,0). %was orignally encode(0,z).
encode(D,s(N)):- D > 0, E is D-1, encode(E,N).
所以我现在可以像我想的那样使用它了,谢谢大家!
library(clpfd)
“双向”工作的解决方案
:- use_module(library(clpfd)).
natsx_int(0, 0).
natsx_int(s(N), I1) :-
I1 #> 0,
I2 #= I1 - 1,
natsx_int(N, I2).
没问题与元谓词
nest_right/4
串联
Prolog lambdas!
:- use_module(library(lambda)).
:- use_module(library(clpfd)).
:- meta_predicate nest_right(2,?,?,?).
nest_right(P_2,N,X0,X) :-
zcompare(Op,N,0),
ord_nest_right_(Op,P_2,N,X0,X).
:- meta_predicate ord_nest_right_(?,2,?,?,?).
ord_nest_right_(=,_,_,X,X).
ord_nest_right_(>,P_2,N,X0,X2) :-
N0 #= N-1,
call(P_2,X1,X2),
nest_right(P_2,N0,X0,X1).
示例查询:
?- nest_right(\X^s(X)^true,3,0,N).
N = s(s(s(0))). % succeeds deterministically
?- nest_right(\X^s(X)^true,N,0,s(s(0))).
N = 2 ; % succeeds, but leaves behind choicepoint
false. % terminates universally
这是我的:
实际上更适合Prolog的Peano数,以列表的形式。
为什么列出?
s
并终止于空列表s
终止于符号zero
我们开始吧,中间有一个小谜语我不会 解决(使用带注释的变量,也许?)
% ===
% Something to replace (frankly badly named and ugly) "var(X)" and "nonvar(X)"
% ===
ff(X) :- var(X). % is X a variable referencing a fresh/unbound/uninstantiated term? (is X a "freshvar"?)
bb(X) :- nonvar(X). % is X a variable referencing an nonfresh/bound/instantiated term? (is X a "boundvar"?)
% ===
% This works if:
% Xn is boundvar and Xp is freshvar:
% Map Xn from the domain of integers >=0 to Xp from the domain of lists-of-only-s.
% Xp is boundvar and Xn is freshvar:
% Map from the domain of lists-of-only-s to the domain of integers >=0
% Xp is boundvar and Xp is boundvar:
% Make sure the two representations are isomorphic to each other (map either
% way and fail if the mapping gives something else than passed)
% Xp is freshvar and Xp is freshvar:
% WE DON'T HANDLE THAT!
% If you have a freshvar in one domain and the other (these cannot be the same!)
% you need to set up a constraint between the freshvars (via coroutining?) so that
% if any of the variables is bound with a value from its respective domain, the
% other is bound auotmatically with the corresponding value from ITS domain. How to
% do that? I did it awkwardly using a lookup structure that is passed as 3rd/4th
% argument, but that's not a solution I would like to see.
% ===
peanoify(Xn,Xp) :-
(bb(Xn) -> integer(Xn),Xn>=0 ; true), % make sure Xn is a good value if bound
(bb(Xp) -> is_list(Xp),maplist(==(s),Xp) ; true), % make sure Xp is a good value if bound
((ff(Xn),ff(Xp)) -> throw("Not implemented!") ; true), % TODO
length(Xp,Xn),maplist(=(s),Xp).
% ===
% Testing is rewarding!
% Run with: ?- rt(_).
% ===
:- begin_tests(peano).
test(left0,true(Xp=[])) :- peanoify(0,Xp).
test(right0,true(Xn=0)) :- peanoify(Xn,[]).
test(left1,true(Xp=[s])) :- peanoify(1,Xp).
test(right1,true(Xn=1)) :- peanoify(Xn,[s]).
test(left2,true(Xp=[s,s])) :- peanoify(2,Xp).
test(right2,true(Xn=2)) :- peanoify(Xn,[s,s]).
test(left3,true(Xp=[s,s,s])) :- peanoify(3,Xp).
test(right3,true(Xn=3)) :- peanoify(Xn,[s,s,s]).
test(f1,fail) :- peanoify(-1,_).
test(f2,fail) :- peanoify(_,[k]).
test(f3,fail) :- peanoify(a,_).
test(f4,fail) :- peanoify(_,a).
test(f5,fail) :- peanoify([s],_).
test(f6,fail) :- peanoify(_,1).
test(bi0) :- peanoify(0,[]).
test(bi1) :- peanoify(1,[s]).
test(bi2) :- peanoify(2,[s,s]).
:- end_tests(peano).
rt(peano) :- run_tests(peano).
不使用 clp:
peano_int(P, I) :-
% Check integer, if provided
( nonvar(I)
-> integer(I),
I @>= 0
; true
),
% 2nd arg is Peano, counting down
peano_int_(0, s(P), P, 0, I).
peano_int_(PU, s(PD), P, IU, I) :-
( ( PD == 0
; IU == I
)
% Finished
-> Eq = true
; true
),
peano_int_eq_(Eq, PU, PD, P, IU, I).
peano_int_eq_(true, P, 0, P, I, I).
peano_int_eq_(false, PU, PD, P, IU, I) :-
IU1 is IU + 1,
peano_int_(s(PU), PD, P, IU1, I).
在所有方向上都是确定性的:
?- peano_int(P, 3).
P = s(s(s(0))).
?- peano_int(s(s(s(0))), I).
I = 3.
?- peano_int(s(s(0)), 2).
true.