公式化效应公理

Posted 2023-05-08

【中文标题】公式化效应公理

【英文标题】：Formulating Effect axiom

【发布时间】：2016-12-05 23:41:52

【问题描述】：

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

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

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

桶 1 装满水，可容纳 7 升水。桶 2 是空的，可容纳 3 升。目标状态是 b2 包含 1 升水。

我会说正确的解决方案是：

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

这是正确的还是我应该将升数设置为 l= 5，例如？

【问题讨论】：

至少对于 Prolog，你的问题没有意义。尝试用编程语言将其形式化，以获得线索。

或许您应该先解释一下，b、t 和 l 代表什么以及规则应该做什么。假设 t 是一个时间点，b 代表一个桶，l 是一个水量（以升为单位），你说：“如果在某个点 t，任何桶是空的，那么任何桶都有任意数量的水”。但是，您的公理的一个实例是“在时间 t，如果桶 b 是空的，那么桶 b 包含 100 升水。”这是一个矛盾。由于矛盾的公理证明了什么，你不应该使用它们。

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

【参考方案1】：

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

:- use_module(library(clpfd)).

首先我们声明有 3 个桶，由原子 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.

并非所有容器都变为负数，因此我们将它们的域设置为从零到（正）无穷大。

现在什么是动作？到目前为止，您描述了清空和倾倒：

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).

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

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

【参考方案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.

编辑：移除域约束以加快计算速度（我们从固定状态开始，因此约束将始终是基础的，并且可以在没有标记的情况下传播）。

【参考方案3】：

我认为答案是：

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

【讨论】：

有道理，你能解释一下你的说法吗？您使用哪本书作为参考？