我有一个非常简单的问题:编写一个实现 append Prolog 函数的 Prolog 程序,它连接两个字符串并以下列方式工作:
- 追加([a,b],[c,d],X)。---> X = [a,b,c,d]
- 追加([a,b],X,[a,b,c,d])。---> X = [c,d]
- 追加([a,b],[X,d],[a,b,c,d])。---> X=c
- 追加(X,Y,[a,b,c,d])。---> X=[] 和 Y=[a,b,c,d)
所以我有以下两种解决方案,我不太确定我的声明性解释是否正确:
1)解决方案1:
myappend1([],L,L).
myappend1([X|L1],L2,[X|L3]) :- myappend1(L1,L2,L3).
我认为我可以以声明性方式阅读它,如下所示:
事实是:如果第一个列表 (L1) 为空且第二个列表 (L2) 不为空,则L1*L2 的串联为 L2为 TRUE
如果事实不正确,则意味着第一个列表不为空,因此第一个列表和第二个列表的连接不正确,即第二个列表
所以,让我称第一个列表 L1、第二个列表 L2 和第三个列表 L3 如果 L3 是 L1 和 L2 的串联,则规则响应 TRUE,否则返回 false
我认为这条规则的声明性含义是:如果规则的主体为真,则规则的头部为真。
- 在头部从L1列表和L3列表中提取第一个X元素(并尝试统一,如果匹配则继续,否则意味着第三个列表它不是第一个和第二个列表的串联)
- 在正文中调用第一个没有 X 元素的列表、第二个列表和 L3 列表(表示连接)上的函数
当它达到我已证明的事实myappend1([],L,L) 的基本情况时。这是真的,程序在前一个过去进行回溯,并且因为第一个列表的 X 元素与第三个列表的 X 元素统一它可以做到这一点,这个计算通过它是 TRUE 并返回直到到达第一个断言
这是一个正确的声明性解释吗?
2)第二种解决方案:
myappend2([],L,L).
myappend2(L1,L2,L3) :- L1=[X|T], % Dimostra questo predicato AND
L3=[X|L4], % Dimostra questo predicato AND
myappend2(T,L2,L4). % Dimostra questa funzione
与前面的解决方案一样,事实简单地说:如果第一个列表 (L1) 为空且第二个列表 (L2) 不为空,则L1*L2 的串联为 L2为 TRUE
如果事实不正确,则意味着第一个列表不为空,因此第一个列表和第二个列表的连接不正确,即第二个列表
如果事实不正确,则 Prolog 调用规则,该规则意味着:如果规则主体为真,则规则的头部为真。
在这种情况下,我可以这样阅读:
如果满足以下条件,则 L1 和 L2 的串联 L3 为 TRUE:
- L1 的当前第一个 X 元素与连接列表的当前第一个元素和 myappend2 在第一个子列表、L2 和第三个子列表上调用它是 true
这是对的吗?
对我来说,以声明的方式进行推理是如此困难:-(