如何检查变量是否在水星中实例化

Question

我是水星语言的完全初学者，虽然我以前学过Prolog。水星的一个新的方面是脱轨主义。main函数必须是确定性的。为了做到这一点，我必须检查变量是否被统一/绑定到一个值，但我无法找到如何做到这一点。特别请参阅守则：

main(!IO) :-
mother(X,"john"),
( if bound(X)    <-----this is my failed try; how to check if X is unified?
  then
    io.format("%s\n", [s(X)], !IO)
  else
    io.write_string("Not available\n",!IO)
).

这样的main不可能失败，即它将满足确定性约束。因此，问题是如何检查一个变量是否被绑定。

Answer 1

我已经将这个家族树从这一边找到的一个Prolog example中翻译出来，以作比较。我已经说明了所有的事实(人)及其相互之间的关系，以及几个助手谓词。请注意，这个类型的版本确实找到了您在顶部答案：female(jane).中看到的错误。

主谓词不必是确定性的，它也可以是cc_multi，这意味着水星将提交(而不是尝试其他)它所拥有的选项；您可以通过用parent替换mother来验证这一点。

您也不必检查变量的有界性，而只需在if子句中使用任何不确定的项，在继承时，该部分将有保证的绑定变量，或者在其他部分中没有绑定。

如果希望此示例更动态，则必须使用lexer或term模块将输入解析为person原子。

如果您想要所有的解决方案，您应该检查solution模块。

%-------------------------------%
% vim: ft=mercury ff=unix ts=4 sw=4 et
%-------------------------------%
% File: relationship.m
%-------------------------------%
% Classical example of family relationship representation,
% based on: https://stackoverflow.com/questions/679728/prolog-family-tree
%-------------------------------%

:- module relationship.

:- interface.

:- import_module io.

%-------------------------------%

:- pred main(io::di, io::uo) is cc_multi.

%-------------------------------%
%-------------------------------%

:- implementation.

:- type person
    --->    john
    ;       bob
    ;       bill
    ;       ron
    ;       jeff
    ;       mary
    ;       sue
    ;       nancy
    ;       jane
    .

:- pred person(person::out) is multi.

person(Person) :- male(Person).
person(Person) :- female(Person).

:- pred male(person).
:- mode male(in) is semidet.
:- mode male(out) is multi.

male(john).
male(bob).
male(bill).
male(ron).
male(jeff).

:- pred female(person).
:- mode female(in) is semidet.
:- mode female(out) is multi.

female(mary).
female(sue).
female(nancy).
female(jane).

:- pred parent(person, person).
:- mode parent(in, in) is semidet.
:- mode parent(in, out) is nondet.
:- mode parent(out, in) is nondet.
:- mode parent(out, out) is multi.

parent(mary, sue).
parent(mary, bill).
parent(sue, nancy).
parent(sue, jeff).
parent(jane, ron).

parent(john, bob).
parent(john, bill).
parent(bob, nancy).
parent(bob, jeff).
parent(bill, ron).

:- pred mother(person, person).
:- mode mother(in, in) is semidet.
:- mode mother(in, out) is nondet.
:- mode mother(out, in) is nondet.
:- mode mother(out, out) is nondet.

mother(Mother, Child) :-
    female(Mother),
    parent(Mother, Child).

:- pred father(person, person).
:- mode father(in, in) is semidet.
:- mode father(in, out) is nondet.
:- mode father(out, in) is nondet.
:- mode father(out, out) is nondet.

father(Father, Child) :-
    male(Father),
    parent(Father, Child).

%-------------------------------%

main(!IO) :-
    Child = john, % try sue or whatever for the first answer
    ( if mother(Mother, Child) then
        io.write(Mother, !IO),
        io.print(" is ", !IO),
        io.write(Child, !IO),
        io.print_line("'s mother", !IO)
    else
        io.write(Child, !IO),
        io.print_line("'s mother is unknown", !IO)
    ).

%-------------------------------%
:- end_module relationship.
%-------------------------------%

Answer 2

您不需要检查变量的实例化状态。我从来没有这样做，在几乎10年的使用汞每天的基础上。对于每个谓词和谓词的模式，水星在程序中的每个点静态地知道每个变量的实例化。所以用你的例子：

% I'm making some assumptions here.
:- pred mother(string::out, string::in) is det.

main(!IO) :-
    mother(X,"john"),
    io.format("%s\n", [s(X)], !IO).

对母亲的声明说，它的第一个参数是输出参数，这意味着在调用母亲之后，它的价值将成为基础。这样就可以印出来了。如果您确实使用了var谓词(标准库中有一个)，那么它总是会失败的。

为了做到这一点，水星对程序员提出了其他要求。例如。

(
    X = a,
    Y = b
;
    X = c
)
io.write(Y, !IO)

上述代码是非法的。因为Y是在第一种情况下产生的，而不是在第二种情况下产生的，所以它的基础没有得到很好的定义。编译器还知道，分离是一个开关(当X已经接地时)，因为只有一个分离可能是真。因此，它只能给出一个答案。

当你有一个多模式的谓词时，这个静态的背景就会变得很棘手。水星可能需要重新排序你的连词，以使程序模式正确:如使用变量后，它的生产。然而，变量的使用和实例化状态始终是静态的。

我知道这与Prolog有很大的不同，可能需要大量的取消学习。

希望这能帮上忙，万事如意。

Answer 3

main(!IO) :-
  mother(X,"john"),
  ( if bound(X)    <-----this is my failed try; how to check if X is unified?
    then
      io.format("%s\n", [s(X)], !IO)
    else
      io.write_string("Not available\n",!IO)
  ).

这段代码在水星里没有多大意义。如果X是来自mother的标准输出变量，那么它将永远不会在X未绑定的情况下成功。

如果mother在这种模式下是确定性的(det)，那么总是会为X提供一个单一的值。在这种情况下，不需要检查任何东西；mother(X, "john")给你约翰的母亲，故事的结尾，所以没有必要“没有可用的情况”。

由于您试图编写案例来处理mother给您提供的东西和它没有处理的情况，所以我假设mother不是确定性的。如果它是semidet，那么就有两种可能；它成功地将X绑定到某个东西，或者失败了。如果不绑定X，它将不会成功。

您的代码没有提到如果main失败，mother (总是成功所必需的)是如何成功的。请记住，逗号是逻辑连接(和)。您的代码说：“如果main成功，mother(X, "john")就会成功(if .. then ... else ...) succeeds)”。但是如果mother失败了，那又如何呢？编译器将基于这个原因拒绝您的代码，即使您的其余代码是有效的。

但是，if ... then ... else ...结构的设计正好允许您检查可能成功或失败的目标，并指定目标何时成功的情况和失败时的情况，这样整个if/then/else总是成功的。因此，您所需要做的就是将mother(X, "john")放在if/if/else的条件下。

在水星，你不会打开变量，要么是绑定的，要么是未绑定的。相反，只需检查绑定变量的目标是成功还是失败。