prolog - 使用属性变量具体化 Prolog 中的基础性

Question

我正在开发自己的 when/2 实现.

在内部，when/2 需要能够——由于缺乏更好的词——“具体化”ground/1。使用属性变量来做到这一点(以 SICStus-Prolog)就是这个问题的全部内容。

我的实现应该像以下“引用”实现一样工作:

ground_t(Term,T) :-
   when(ground(Term), T=true).

出于好奇，我编写了以下小求解器:

:- module(ground_t,[ground_t/2]).

:- use_module(library(atts)).
:- attribute ground_t/1.

ground_t(Term,T) :-
    (  ground(Term)
    -> T = true
    ;  term_variables(Term,Vs),
       create_mutable(Vs,MVs),
       attach_to_new_vars(Vs,MVs,T)
    ).

attach_to_new_vars([],_,_).
attach_to_new_vars([V|Vs],MVs,T) :-
    (  get_atts(V,+ground_t(Cs0))
    -> Cs = Cs0
    ;  Cs = []
    ),
    put_atts(V,+ground_t([MVs-T|Cs])),
    attach_to_new_vars(Vs,MVs,T).

% simple case: unify w/ground term
cliques_var_goals__ground([],_,[]).
cliques_var_goals__ground([MVs-T|Cs],Var,Goals) :-
    get_mutable(Vs0,MVs),
    list_eq_removed_atmost_once(Vs0,Var,Vs1),
    update_mutable(Vs1,MVs),
    (  Vs1 = []
    -> Goals = [T=true|Goals0]
    ;  Goals = Goals0
    ),
    cliques_var_goals__ground(Cs,Var,Goals0).

list_eq_removed_atmost_once([],_,[]).
list_eq_removed_atmost_once([X|Xs],E,Ys) :-
    (  X == E
    -> Ys = Xs         % remove item. do it at most once and stop
    ;  Ys = [X|Ys0],
       list_eq_removed_atmost_once(Xs,E,Ys0)
    ).

% general case: unify w/non-ground term
cliques_var_other__nonvar([],_,_).
cliques_var_other__nonvar([MVs-T|Cs],Var,Other) :-
    get_mutable(Vs0,MVs),
    term_variables(Vs0+Other,Vs1),
    term_variables(Other,New0),
    list_eq_removed_atmost_once(New0,Var,New),
    list_eq_removed_atmost_once(Vs1,Var,Vs2),
    attach_to_new_vars(New,MVs,T),
    update_mutable(Vs2,MVs),
    cliques_var_other__nonvar(Cs,Var,Other).

sort_all([]).
sort_all([MVs-_T|Xs]) :-
    get_mutable(Vs0,MVs),
    term_variables(Vs0,Vs),
    update_mutable(Vs,MVs),
    sort_all(Xs).

merge_cliques_post_unify(Cs0,Cs1,Other) :-
    append(Cs0,Cs1,Cs01),
    sort_all(Cs01),
    put_atts(Other,+ground_t(Cs01)).

verify_attributes(Var,Other,Goals) :-
    (  get_atts(Var,+ground_t(Cs0))
    -> (  ground(Other)
       -> cliques_var_goals__ground(Cs0,Var,Goals)
       ;  nonvar(Other)
       -> cliques_var_other__nonvar(Cs0,Var,Other),
          Goals = []
       ;  get_atts(Other,+ground_t(Cs1))
       -> Goals = [merge_cliques_post_unify(Cs0,Cs1,Other)]
       ;  put_atts(Other,+ground_t(Cs0)),
          Goals = []
       )
    ;  Goals = []
    ).

cliques_to_goal([]) --> [].
cliques_to_goal([MVs-T|Cs]) -->
    { get_mutable(Vs,MVs) },
    (  { Vs = []  } -> []
    ;  { Vs = [V] } -> [ground_t(V ,T)]
    ;                  [ground_t(Vs,T)]
    ),
    cliques_to_goal(Cs).

list_to_commalist([],true).
list_to_commalist([X],Y) :-
    !,
    X = Y.
list_to_commalist([X|Xs],(X,Y)) :-
    list_to_commalist(Xs,Y).

attribute_goals(Var) -->
    { get_atts(Var,+ground_t(Cs)) },
    cliques_to_goal(Cs).

attribute_goal(Var,Goal) :-
    phrase(attribute_goals(Var),Goals),
    list_to_commalist(Goals,Goal).

这是简单部分；现在是困难部分...

在共享术语林中执行变量别名和实例化的多个步骤时，如何测试两个求解器的行为是否等效？

---

以下是我所做的一些简单的手动测试:

| ?- ground_t(X+Y,T1).
| ?- ground_t(X+Y,T1),X=f(U).
| ?- ground_t(X+Y,T1),X=f(U),U=Y.
| ?- ground_t(X+Y,T1),X=f(U),U=Y,Y=y.

| ?- ground_t(X+Y,T1),ground_t(X+Z,T2).
| ?- ground_t(X+Y,T1),ground_t(X+Z,T2),X = -U,Z = +V.
| ?- ground_t(X+Y,T1),ground_t(X+Z,T2),X = -U,Z = +U.
| ?- ground_t(X+Y,T1),ground_t(X+Z,T2),X = -U,Z = +U,U=u.
| ?- ground_t(X+Y,T1),ground_t(X+Z,T2),X = -U,Z = +U,U=u,Y=U.

也许您对一些不错的极端案例有好主意...请分享!

Answer 1

真正困难的部分首先是理解ground_t/2实际上是什么。它没有具体化任何东西，因为不存在假。

这似乎是您需要实现when/2的一些内部辅助谓词。如果它是一个内部谓词，它不需要满足我们对真实约束的所有期望。最值得注意的是，您的实现(以及使用内置 when/2 的引用实现)不会限制所有涉及的变量:

SICStus 4.8.0beta3 (x86_64-linux-glibc2.17): Mon Oct 17 20:11:03 UTC 2022
...
| ?- when(ground(A-B),T=true),copy_term(A,Ac,Ac_0),copy_term(B,Bc,Bc_0).
Ac_0 = prolog:trig_ground(Ac,[_A],[Ac,_A],_B,_B),
Bc_0 = true,
prolog:trig_ground(A,[B],[A,B],_C,_C),
prolog:when(_C,ground(A-B),user:(T=true)) ? ;
no
| ?- ground_t(A-B,T),copy_term(A,Ac,Ac_0),copy_term(B,Bc,Bc_0).
Ac_0 = ground_t:(ground_t([Ac,_A],_B),true),
Bc_0 = ground_t:true ? ;
no
| ?- ground_t(A-B,T).
ground_t([A,B],T) ? ;
no
| ?- 

因此，尽管 ground_t:true 给了我们一个提示，但两者并没有真正约束 B。另外，目标 ground_t([A,B],T) 似乎仅在未使用 copy_term/3 时显示。

考虑到如此宽松的要求，freeze/2 就足够了。根本不需要深入研究全地形车。

myground_t(Term, T) :-
    term_variables(Term, Vs),
    myvars_t(Vs, T).

myvars_t([], true).
myvars_t([V|Vs], T) :-
    freeze(V, myground_t([V|Vs], T)).

| ?- myground_t(A-B,T),copy_term(A,Ac,Ac_0),copy_term(B,Bc,Bc_0).
Ac_0 = prolog:freeze(Ac,user:myground_t([Ac,_A],_B)),
Bc_0 = true,
prolog:freeze(A,user:myground_t([A,B],T)) ? ;
no

(term_variables/2 的良好实现可以避免重新创建相同的列表后缀。不，目前我不知道。) 此实现中缺少什么？

现在来回答有关测试的实际问题。测试协程和约束需要大量计算。因此，人们可能会提前询问要测试的实现是否以某种方式编写，以避免某些错误先验。我没有进一步阅读您的代码 term_variables_set/2它的第二个参数取决于变量的年龄，这意味着它可能适用于一个年龄，但不适用于另一个年龄。 It would not be the first 。因此测试变得更加复杂。为什么会这样？