我开始学习Prolog,并首先了解了继承符号.
这就是我在Prolog中发现编写Peano公理的地方.
参见PDF的第12页:
sum(0, M, M).
sum(s(N), M, s(K)) :-
sum(N,M,K).
prod(0,M,0).
prod(s(N), M, P) :-
prod(N,M,K),
sum(K,M,P).
Run Code Online (Sandbox Code Playgroud)
我把乘法规则放到了Prolog中.然后我做查询:
?- prod(X,Y,s(s(s(s(s(s(0))))))).
Run Code Online (Sandbox Code Playgroud)
这意味着基本上找到6的因子.
结果如下.
X = s(0),
Y = s(s(s(s(s(s(0)))))) ? ;
X = s(s(0)),
Y = s(s(s(0))) ? ;
X = s(s(s(0))),
Y = s(s(0)) ? ;
infinite loop
Run Code Online (Sandbox Code Playgroud)
这个结果有两个问题:
所以...我的问题是:
我在无限循环中阅读了另一个答案.但我很感激有人根据这个场景做出回答.这对我很有帮助.
prolog infinite-loop successor-arithmetics non-termination failure-slice
到目前为止,我一直坚持 Prolog程序意味着:
如果对于一个查询
Q,有一个subtermS,使得存在一个术语T,使?- S=T, Q.成功虽然?- Q, S=T.失败,然后通过调用一个谓词Q是不踏实.
直觉上,我因此坚定地表示我们不能使用实例化来"欺骗"谓词来提供解决方案,否则这些解决方案不仅不会被给予,而是被拒绝.注意非终止程序的区别!
特别是,至少在我看来,逻辑纯度总是意味着坚定不移.
例子.为了更好地理解坚定性的概念,考虑这个属性的几乎经典的反例,在将高级学生引入Prolog的操作方面时经常引用,使用两个整数之间关系的错误定义及其最大值:
integer_integer_maximum(X, Y, Y) :-
Y >= X,
!.
integer_integer_maximum(X, _, X).
这个中的一个明显错误 - 我们应该说" 摇摆不定 " - 定义当然是以下查询错误地成功:
?- M = 0, integer_integer_maximum(0, 1, M). M = 0. % wrong!
而交换目标产生了正确的答案:
?- integer_integer_maximum(0, 1, M), M = 0. false.
这个问题的一个很好的解决方案是依靠 …
CPDT的第三章简要讨论了为什么在Coq中禁止负归纳类型.如果我们有
Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.
Run Code Online (Sandbox Code Playgroud)
然后我们可以轻松定义一个函数
Definition uhoh (t : term) : term :=
match t with
| Abs f => f t
| _ => t
end.
Run Code Online (Sandbox Code Playgroud)
因此该术语uhoh (Abs uhoh)将是非终止的,"我们将能够证明每个定理".
我理解非终止部分,但我不知道如何用它来证明任何东西.如何False使用term上面定义的证明?
我需要用自然数来创建一个2的幂的Prolog谓词.自然数是:0,s(0),s(s(0))ans等等.
例如:
?- pow2(s(0),P).
P = s(s(0));
false.
?- pow2(P,s(s(0))).
P = s(0);
false.
Run Code Online (Sandbox Code Playgroud)
这是我的代码:
times2(X,Y) :-
add(X,X,Y).
pow2(0,s(0)).
pow2(s(N),Y) :-
pow2(N,Z),
times2(Z,Y).
Run Code Online (Sandbox Code Playgroud)
并且它与第一个示例完美配合,但在第二个示例中进入无限循环.
我该如何解决这个问题?
prolog exponentiation successor-arithmetics non-termination failure-slice
我正在尝试解决这个问题,我已经阅读了这个答案,但我的问题是无限循环,即使我使用了访问节点列表。
让我们看看我的两次尝试:
edge(1,2).
edge(1,4).
edge(1,3).
edge(2,3).
edge(2,5).
edge(3,4).
edge(3,5).
edge(4,5).
% ------ simple path finding in a directed graph
% ----- simple exploration
path0(A,B, Result) :-
path0(A, B, [], Result).
path0(A, B, _, [e(A,B)]):-
edge(A,B).
path0(A, B, Visited, [e(A,X)|Path]):-
edge(A, X), dif(X, B),
\+ member(X, Visited),
path0(X, B, [A|Visited], Path ).
%---- 1. exploration and length
path(A, B, _, [e(A,B)], 1):-
edge(A,B).
path(A, B, Visited, [e(A,X)|Path], Length):-
edge(A, X),
\+ member(X, Visited),
length(Path, L), % ERR: Path refers …Run Code Online (Sandbox Code Playgroud) graph-theory prolog shortest-path non-termination failure-slice
假设我想断言三个列表的长度相同.我可以这样做:
same_length(First, Second, Third) :-
same_length(First, Second),
same_length(Second, Third).
Run Code Online (Sandbox Code Playgroud)
无论是实例化First还是Second实例化,这都是正确的.当所有三个参数都被实例化时它也可以工作!但是,一个调用length(Third, 3), same_length(First, Second, Third)会使它返回正确答案(所有三个列表的长度为3)和一个选择点,然后循环永远生成永远不会匹配的解决方案.
我写过一个版本,我认为在任何情况下都是正确的:
same_length(First, Second, Third) :-
/* naively calling same_length(First, Second), same_length(Second, Third) doesn't work,
because it will fail to terminate in the case where both First and Second are
uninstantiated.
by always giving the first same_length/2 clause a real list we prevent it from
generating infinite solutions */
( is_list(First), same_length(First, Second), same_length(First, Third), !
; is_list(Second), same_length(Second, First), same_length(Second, …Run Code Online (Sandbox Code Playgroud) 我无法弄清楚这出错的地方.请注意,我对Prolog很新,我确定我错过了一些东西 - 不知道那可能是什么.有人可以帮帮我吗?
谢谢,这是我的代码:
printSentence([]).
printSentence([W|[]]) :-
write(W),
write('.'),
nl.
printSentence([W|R]) :-
write(W),
write(' '),
printSentence(R).
transform([], Result).
transform([Word|Rest], Result) :-
replace(Word, Replacement),
append(Result, Replacement, NewResult),
transform(Rest, NewResult).
replace(my, your).
replace(i, you).
replace(you, me).
replace(am, are).
replace(Word, Word).
test :-
X = [you, are, my, only, hope],
transform(X, Result),
printSentence(Result).
Run Code Online (Sandbox Code Playgroud) 我是Prolog的新手,我在检查两个列表是否具有完全相同的元素时遇到了问题.元素可能具有不同的顺序.我有这个代码:
myremove(X, [X|T], T).
myremove(X, [H|T], [H|R]) :-
myremove(X, T, R).
same_elements([], []).
same_elements([H1|T1], L2) :-
myremove(H1, L2, Nl2),
same_elements(T1, Nl2).
Run Code Online (Sandbox Code Playgroud)
它的工作原理除外
?- same_elements([b,c,a], X).
Run Code Online (Sandbox Code Playgroud)
返回第一个结果后导致内存不足错误.那么我试图通过检查列表的长度是否相等并检查H1是L2的成员来缩小结果集:
mylength([], 0).
mylength([_|T], R) :-
mylength(T, Nr),
R is Nr+1.
mymember(X, [X|_]).
mymember(X, [_|T]) :-
mymember(X, T).
same_elements([], []).
same_elements([H1|T1], L2) :-
mylength([H1|T1], X),
mylength(L2, Y),
Y = X,
mymember(H1, L2),
myremove(H1, L2, Nl2),
same_elements(T1, Nl2).
Run Code Online (Sandbox Code Playgroud)
现在两个
?- same_elements([b,c,a], X).
?- same_elements(X, [b,c,a]).
Run Code Online (Sandbox Code Playgroud)
返回所有结果,但之后它们就会挂起.有一个更好的方法吗?
假设我有一个prolog程序来连接这样的列表:
concat([],X,X).
concat([Head|Tail],X,[Head|R]) :- concat(Tail,X,R).
Run Code Online (Sandbox Code Playgroud)
我怎么知道哪些问题会返回有限数量的答案?例如,问
concat(X,Y,[1,2,3,4]).
Run Code Online (Sandbox Code Playgroud)
将返回有限解集:
X = [],
Y = [1, 2, 3, 4] ;
X = [1],
Y = [2, 3, 4] ;
X = [1, 2],
Y = [3, 4] ;
X = [1, 2, 3],
Y = [4] ;
X = [1, 2, 3, 4],
Y = [] ;
false.
Run Code Online (Sandbox Code Playgroud)
在提问时
concat(X,[2,3],Z).
Run Code Online (Sandbox Code Playgroud)
将返回一组无限的解决方案:
X = [],
Z = [1, 2, 3] ;
X = [_G24],
Z = [_G24, 1, 2, 3] ;
X = …Run Code Online (Sandbox Code Playgroud) 所以
?- canCall(mary, Person).
Run Code Online (Sandbox Code Playgroud)
工作并终止,
?- canFind(mary, Person).
Run Code Online (Sandbox Code Playgroud)
也可以工作并终止。但是不知何故
?- canCall(mary, Person), canFind(mary, Person).
Run Code Online (Sandbox Code Playgroud)
不终止。可能是什么原因?
我正在尝试在Prolog中实现Levenshtein距离。
实现非常简单:
levenshtein(W1, W2, D) :-
atom_length(W1, L1),
atom_length(W2, L2),
lev(W1, W2, L1, L2, D),
!.
lev(_, _, L1, 0, D) :- D is L1, !.
lev(_, _, 0, L2, D) :- D is L2, !.
lev(W1, W2, L1, L2, D) :-
lev(W1, W2, L1 - 1, L2, D1),
lev(W1, W2, L1, L2 - 1, D2),
lev(W1, W2, L1 - 1, L2 - 1, D3),
charAt(W1, L1, C1),
charAt(W2, L2, C2),
( C1 = C2 -> T is …Run Code Online (Sandbox Code Playgroud) 我想知道为什么在这些情况下程序会无限递归:
?- love(kay, amanda).
Run Code Online (Sandbox Code Playgroud)
和
?- love(rob, amanda).
Run Code Online (Sandbox Code Playgroud)
这是代码:
love(amanda, kay).
love(kay, geo).
love(geo, rob).
love(X, Y) :-
love(X, Z),
love(Z, Y).
love(X, Y) :-
love(Y, X).
Run Code Online (Sandbox Code Playgroud)