制定效应公理

Question

如何使用谓词contains(b,l,t)正确编写空(b,t)-action的效果公理。如果桶b在时间t持有l升水，则该谓词评估为True。

empty(b,t)：在时间t完全清空桶b。转移的效果在时间t+1可见。

transfer(b,b',t)：尽可能多地从桶b向桶b'转移水，而不会溢出，开始时间为t。转移的效果在时间t+1可见。

桶1装满了水，容量为7升。桶2为空，容量为3升。目标状态是b2含有1升水。

我认为正确的解决方案是：

to any b,t,l( empty(b,t) -> contains(b,l,t))

这样做正确吗？或者我应该将升数设置为l=5，例如？

- Mensch

---

至少对于 Prolog 来说，你的问题没有意义。尝试在编程语言中规范化它，以获得线索。 - CapelliC

也许你应该首先解释一下，b、t和l分别代表什么，这个规则的作用是什么。假设t表示一个时间点，b代表一个水桶，l表示水的数量（以升为单位），你说：“如果在某个时间点t，任何一个桶都是空的，那么任何一个桶都有任意数量的水。” 但是，你的公理实例是“在时间t时，如果桶b为空，则桶b包含100升的水。” 这是一个矛盾。因为矛盾的公理可以证明任何事情，所以你不应该使用它们。 - lambda.xy.x

@CapelliC @lambda.xy.x 更新了问题以便更好地理解。 - Mensch

Answer 1

对于这个问题，不需要明确的时间，我们将历史表示为一系列操作列表。另一方面，您需要显式地表示系统状态，即三个桶的当前内容。原因是Prolog数据结构（即项）一旦创建就无法更改。由于有许多无意义的术语，定义数据类型通常是一个好习惯，可以通过is_type/1谓词来实现。因为您在某个时候将使用算术（当您将水从一个桶倒入另一个桶时），所以我会使用算术约束而不是古老的is/2谓词。

:- use_module(library(clpfd)).

首先，我们声明有三个桶，分别由原子b1、b2和b3表示：

is_bucket(b1).
is_bucket(b2).
is_bucket(b3).

然后我们需要定义我们的状态。我们只是使用一个术语 buckets/3，其中第一个参数保存 b1 的容量，同样适用于其他两个参数。

is_state(buckets(X,Y,Z)) :-
    % each bucket contains at least 0 liters
    [X,Y,Z] ins 0 .. sup.

所有容器不能变成负数，因此我们将它们的范围设置为从零到（正）无穷大。

那么什么是action呢？到目前为止，您已经描述了倒空和倒出的操作：

is_action(empty(B)) :-
    is_bucket(B).
is_action(pour(From, To)) :-
    is_bucket(From),
    is_bucket(To).

要清空一个桶，我们只需要知道哪一个。如果我们从一个倒到另一个，我们需要描述两个桶。既然我们已经有了描述桶的谓语，我们可以简单地陈述一个规则，即“如果From和To是桶，那么pour(From, To)就是一个动作。”

现在我们需要解释一个动作如何转换状态。这是旧状态、新状态之间的关系，并且因为我们想知道发生了什么，还涉及历史。

% initial state
state_goesto_action(buckets(7,5,3), buckets(7,5,3), []).

初始状态的转换不改变任何东西，它有一个空的历史记录（[]）。

% state transitions for moving
state_goesto_action(buckets(X,Y,Z), buckets(0,Y,Z), [empty(b1) | History]) :-
    state_goesto_action(_S0, buckets(X,Y,Z), History).

这条规则可以理解为：如果我们有一个来自某个状态 _S0，导致状态 buckets(X,Y,Z) 和一些 History 的动作，那么我们接下来可以执行 empty(b1) 动作，然后我们将到达状态 buckets(0,Y,Z)。换句话说，状态会更新并将动作添加到历史记录中。对于其他的水桶也有类似的规则:

state_goesto_action(buckets(X,Y,Z), buckets(X,0,Z), [empty(b2) | History]) :-
    state_goesto_action(_S0, buckets(X,Y,Z), History).
state_goesto_action(buckets(X,Y,Z), buckets(X,Y,0), [empty(b3) | History]) :-
    state_goesto_action(_S0, buckets(X,Y,Z), History).

我们如何检查这是否有意义？让我们看一下长度为2的历史记录：

?- state_goesto_action(_,S1,[H1,H2]).
S1 = buckets(0, 3, 5),
H1 = H2, H2 = empty(b1) .

非常好，如果两个操作都是empty(b1)，那么第一个桶就是空的，其他桶不受影响。让我们看看更多的解决方案：

S1 = buckets(0, 0, 5),
H1 = empty(b1),
H2 = empty(b2) ;

S1 = buckets(0, 3, 0),
H1 = empty(b1),
H2 = empty(b3) ;

S1 = buckets(0, 0, 5),
H1 = empty(b2),
H2 = empty(b1) ;

S1 = buckets(7, 0, 5),
H1 = H2, H2 = empty(b2) ;

S1 = buckets(7, 0, 0),
H1 = empty(b2),
H2 = empty(b3) ;

S1 = buckets(0, 3, 0),
H1 = empty(b3),
H2 = empty(b1) ;

S1 = buckets(7, 0, 0),
H1 = empty(b3),
H2 = empty(b2) ;

S1 = buckets(7, 3, 0),
H1 = H2, H2 = empty(b3).

看起来我们已经得到了所有清空桶的可能性（仅限于此:-)）。现在您需要添加从一个桶倒入另一个桶的规则。祝你好运！

（编辑：错别字，第二条规则错误）

- lambda.xy.x

Answer 2

我保留原回答，因为它提供了一些值得思考的部分（而且问题只涉及实现空操作）。这里提供完整的实现：

:- use_module(library(clpfd)).

bucket_capacity(b1,7).
bucket_capacity(b2,3).
bucket_capacity(b3,5).

% projections to a single bucket
state_bucket_value(buckets(X, _, _),b1,X).
state_bucket_value(buckets(_, Y, _),b2,Y).
state_bucket_value(buckets(_, _, Z),b3,Z).

% state update relation by a single bucket
state_updated_bucket_value(buckets(_, Y, Z), buckets(X0, Y,  Z ), b1, X0).
state_updated_bucket_value(buckets(X, _, Z), buckets(X,  Y0, Z ), b2, Y0).
state_updated_bucket_value(buckets(X, Y, _), buckets(X,  Y,  Z0), b3, Z0).


% initial state
state_goesto_action(S0, S0, []) :-
    S0 = buckets(X,Y,Z),
    bucket_capacity(b1,X),
    bucket_capacity(b2,Y),
    bucket_capacity(b3,Z).
% state transition for emptying
state_goesto_action(S1, S2, [empty(Bucket) | History]) :-
    state_updated_bucket_value(S1, S2, Bucket, 0),
    state_goesto_action(_S0, S1, History).
% state transition for pouring
state_goesto_action(S1, S3, [pour(From,To) | History]) :-
    bucket_capacity(b1,Max),
    state_bucket_value(S1,From,X),
    state_bucket_value(S1,To,Y),
    From0 #= min(X+Y, Max),
    To0 #= max(X-Y, 0),
    state_updated_bucket_value(S1, S2, From, From0),
    state_updated_bucket_value(S2, S3, To, To0),
    state_goesto_action(_S0, S1, History).

要找出一个恰好有一升水的桶，我们可以列举所有可能的情况：

?- length(L,_), state_bucket_value(S,_,1), state_goesto_action(_, S, L).
L = [pour(b1, b3), pour(b1, b2), empty(b1), pour(b1, b3)],
S = buckets(5, 0, 1) ;
L = [pour(b1, b3), pour(b1, b2), pour(b1, b1), pour(b1, b3)],
S = buckets(5, 0, 1) ;
L = [pour(b1, b3), pour(b1, b2), pour(b2, b1), empty(b1)],
S = buckets(7, 0, 1) ;
L = [pour(b1, b3), pour(b1, b2), pour(b2, b1), pour(b1, b1)],
[...].

为了检查谓词是否可逆：

?- L = [pour(b1, b3), pour(b1, b2), empty(b1), pour(b1, b3)], state_goesto_action(_, S, L).
L = [pour(b1, b3), pour(b1, b2), empty(b1), pour(b1, b3)],
S = buckets(5, 0, 1) ;
false.

编辑：为了加快计算速度，删除了域限制（我们从一个固定的状态开始，所以限制条件总是具有确定的值，并且可以在不进行标记的情况下传播）。

- lambda.xy.x

Answer 3

我认为答案应该是：

Empty(b,t) => Contains(b,0,t+1)

- Azade Farshad

---

有道理，你能解释一下你的陈述吗？你参考的是哪本书？ - Mensch