Prolog反向查找和输入验证同时进行

我最近开始学习prolog,尽管摆脱函数式编程很令人耳目一新,但事情似乎仍然非常陌生 . 我无法理解如何编写谓词,检查其参数是否符合某一组规则,同时如果给定变量,则将其设置为满足这些规则的可能值 .

我试图解决圆桌座位问题,你可以为人们定义一组让他们坐在一起的条件 . 因此,知识库包含10个人,他们说的语言和目标是让他们坐在一起,使两个坐在一起的人必须说同一种语言 .

我定义了一个谓词 speaksSame(X, Y) ,如果个体X和Y都说同一种语言,则返回true . 现在的目标是编写一个函数表 - 如果列表中彼此相邻的两个人说一个共同语言, table-seating([mark, carl, emily, kevin, oliver]) 返回true . 当然,每个人说不止一种语言 . 还有桌座(L) . 将获得满足条件的可能的 table 座位 .

我看到它的方式是我可以编写一个谓词来检查先前定义的列表是否满足规则,或者根据这些规则构建列表 . 我不明白我如何用一个功能做到这两点 .

任何帮助将非常感谢,谢谢!

回答(2)

2 years ago

我不明白我如何用一个功能做到这两点 .

是的,起初这看起来很奇怪,但是一旦你掌握了它,你会错过其他语言 .

引用它时要记住的词是:mode
有关Mercury编程语言的更多详细信息,另请参阅Mercury Modes reference .

在Prolog中,参数可以是输入,输出,或者两者都可以用作输入或输出,具体取决于它的调用方式 .

Type, mode and determinism declaration headers底部列出了4个例子 .

  • length(List:list,-Length:int)是det .

  • length(?List:list,-Length:int)是nondet .

  • length(?List:list,Length:int)是det .

  • 如果List是长度列表,则为真 .

length/2 的定义显示

length(?List, ?Int)

含义
对于 List 参数,列表可以绑定或不绑定,以及
对于 Int 参数,该值可以是绑定的或未绑定的 .
所以对于有两个选项的两个参数,有四种方法可以使用 length/2

在这里它们再次列出,但在实际使用中 .

1 .

length(+List:list, -Length:int) is det.

在这种情况下,List是绑定的,而Length是未绑定的,总是给出一个答案 .

?- length([1,2,3],N).
N = 3.

2 .

length(?List:list, -Length:int) is nondet.

在这种情况下,List是未绑定的,Length是未绑定的,可以返回任意数量的答案 .

?- length(List,N).
List = [],
N = 0 ;
List = [_5362],
N = 1 ;
List = [_5362, _5368],
N = 2 ;
List = [_5362, _5368, _5374],
N = 3 ;
List = [_5362, _5368, _5374, _5380],
N = 4 ;
List = [_5362, _5368, _5374, _5380, _5386],
N = 5 
...

3 .

length(?List:list, +Length:int) is det.

在这种情况下,List是未绑定的,并且Length已绑定并始终给出一个答案 .

?- length(List,4).
List = [_5332, _5338, _5344, _5350].

4 .

True if List is a list of length Length.

在这种情况下,List被绑定并且Length被绑定并始终充当谓词以返回 truefalse .

?- length([1,2,3],3).
true.

?- length([1,2,3],5).
false.

那怎么可能呢?

Prolog使用syntactic unification(↦)和NOT assignment(=) .

如果我们使用 listing/1 查看 length/2 的源代码,我们得到

?- listing(length/2).
system:length(B, A) :-
        var(A), !,
        '$skip_list'(D, B, C),
        (   C==[]
        ->  A=D
        ;   var(C)
        ->  C\==A,
            '$length3'(C, A, D)
        ;   throw(error(type_error(list, B), context(length/2, _)))
        ).
system:length(B, A) :-
        integer(A),
        A>=0, !,
        '$skip_list'(D, B, C),
        (   C==[]
        ->  A=D
        ;   var(C)
        ->  E is A-D,
            '$length'(C, E)
        ;   throw(error(type_error(list, B), context(length/2, _)))
        ).
system:length(_, A) :-
        integer(A), !,
        throw(error(domain_error(not_less_than_zero, A),
                    context(length/2, _))).
system:length(_, A) :-
        throw(error(type_error(integer, A), context(length/2, _))).

这是太详细,但确实正确地完成了所有4种模式 .

为了便于理解,我们将使用this版本,但它不能正确支持其中一种模式,但它确实可以执行多种模式,因此它可以很好地演示 .

length_2([]     , 0 ).
length_2([_|Xs] , L ) :- 
    length_2(Xs,N),
    L is N+1 .

现在,为了看到行动中的统一,我们将使用SWI-Prolog的trace功能并启用box model使用visible/1的所有端口,以便在运行时使用leash/1不要停止它 .

?- visible(+all),leash(-all).
?- trace.

1 .

[trace] ?- length_2([1,2,3],N).
   Call: (8) length_2([1, 2, 3], _2352)
   Unify: (8) length_2([1, 2, 3], _2352)
   Call: (9) length_2([2, 3], _2580)
   Unify: (9) length_2([2, 3], _2580)
   Call: (10) length_2([3], _2580)
   Unify: (10) length_2([3], _2580)
   Call: (11) length_2([], _2580)
   Unify: (11) length_2([], 0)
   Exit: (11) length_2([], 0)
   Call: (11) _2584 is 0+1
   Exit: (11) 1 is 0+1
   Exit: (10) length_2([3], 1)
   Call: (10) _2590 is 1+1
   Exit: (10) 2 is 1+1
   Exit: (9) length_2([2, 3], 2)
   Call: (9) _2352 is 2+1
   Exit: (9) 3 is 2+1
   Exit: (8) length_2([1, 2, 3], 3)
N = 3.

2 .

[trace] ?- length_2(List,N).
   Call: (8) length_2(_2296, _2298)
   Unify: (8) length_2([], 0)
   Exit: (8) length_2([], 0)
List = [],
N = 0 ;
   Redo: (8) length_2(_2296, _2298)
   Unify: (8) length_2([_2528|_2530], _2298)
   Call: (9) length_2(_2530, _2550)
   Unify: (9) length_2([], 0)
   Exit: (9) length_2([], 0)
   Call: (9) _2298 is 0+1
   Exit: (9) 1 is 0+1
   Exit: (8) length_2([_2528], 1)
List = [_2528],
N = 1 ;
   Redo: (9) length_2(_2530, _2550)
   Unify: (9) length_2([_2534|_2536], _2556)
   Call: (10) length_2(_2536, _2556)
   Unify: (10) length_2([], 0)
   Exit: (10) length_2([], 0)
   Call: (10) _2560 is 0+1
   Exit: (10) 1 is 0+1
   Exit: (9) length_2([_2534], 1)
   Call: (9) _2298 is 1+1
   Exit: (9) 2 is 1+1
   Exit: (8) length_2([_2528, _2534], 2)
List = [_2528, _2534],
N = 2 ;
   Redo: (10) length_2(_2536, _2556)
   Unify: (10) length_2([_2540|_2542], _2562)
   Call: (11) length_2(_2542, _2562)
   Unify: (11) length_2([], 0)
   Exit: (11) length_2([], 0)
   Call: (11) _2566 is 0+1
   Exit: (11) 1 is 0+1
   Exit: (10) length_2([_2540], 1)
   Call: (10) _2572 is 1+1
   Exit: (10) 2 is 1+1
   Exit: (9) length_2([_2534, _2540], 2)
   Call: (9) _2298 is 2+1
   Exit: (9) 3 is 2+1
   Exit: (8) length_2([_2528, _2534, _2540], 3)
List = [_2528, _2534, _2540],
N = 3

3 .

[trace] ?- length_2(List,3).
   Call: (8) length_2(_5534, 3)
   Unify: (8) length_2([_5724|_5726], 3)
   Call: (9) length_2(_5726, _5746)
   Unify: (9) length_2([], 0)
   Exit: (9) length_2([], 0)
   Call: (9) 3 is 0+1
   Fail: (9) 3 is 0+1
   Redo: (9) length_2(_5726, _5746)
   Unify: (9) length_2([_5730|_5732], _5752)
   Call: (10) length_2(_5732, _5752)
   Unify: (10) length_2([], 0)
   Exit: (10) length_2([], 0)
   Call: (10) _5756 is 0+1
   Exit: (10) 1 is 0+1
   Exit: (9) length_2([_5730], 1)
   Call: (9) 3 is 1+1
   Fail: (9) 3 is 1+1
   Redo: (10) length_2(_5732, _5752)
   Unify: (10) length_2([_5736|_5738], _5758)
   Call: (11) length_2(_5738, _5758)
   Unify: (11) length_2([], 0)
   Exit: (11) length_2([], 0)
   Call: (11) _5762 is 0+1
   Exit: (11) 1 is 0+1
   Exit: (10) length_2([_5736], 1)
   Call: (10) _5768 is 1+1
   Exit: (10) 2 is 1+1
   Exit: (9) length_2([_5730, _5736], 2)
   Call: (9) 3 is 2+1
   Exit: (9) 3 is 2+1
   Exit: (8) length_2([_5724, _5730, _5736], 3)
List = [_5724, _5730, _5736] 
Action (h for help) ? abort

% Execution Aborted

4 .

[trace] ?- length_2([1,2,3],3).
   Call: (8) length_2([1, 2, 3], 3)
   Unify: (8) length_2([1, 2, 3], 3)
   Call: (9) length_2([2, 3], _2058)
   Unify: (9) length_2([2, 3], _2058)
   Call: (10) length_2([3], _2058)
   Unify: (10) length_2([3], _2058)
   Call: (11) length_2([], _2058)
   Unify: (11) length_2([], 0)
   Exit: (11) length_2([], 0)
   Call: (11) _2062 is 0+1
   Exit: (11) 1 is 0+1
   Exit: (10) length_2([3], 1)
   Call: (10) _2068 is 1+1
   Exit: (10) 2 is 1+1
   Exit: (9) length_2([2, 3], 2)
   Call: (9) 3 is 2+1
   Exit: (9) 3 is 2+1
   Exit: (8) length_2([1, 2, 3], 3)
true.

[trace] ?- length_2([1,2,3],5).
   Call: (8) length_2([1, 2, 3], 5)
   Unify: (8) length_2([1, 2, 3], 5)
   Call: (9) length_2([2, 3], _2442)
   Unify: (9) length_2([2, 3], _2442)
   Call: (10) length_2([3], _2442)
   Unify: (10) length_2([3], _2442)
   Call: (11) length_2([], _2442)
   Unify: (11) length_2([], 0)
   Exit: (11) length_2([], 0)
   Call: (11) _2446 is 0+1
   Exit: (11) 1 is 0+1
   Exit: (10) length_2([3], 1)
   Call: (10) _2452 is 1+1
   Exit: (10) 2 is 1+1
   Exit: (9) length_2([2, 3], 2)
   Call: (9) 5 is 2+1
   Fail: (9) 5 is 2+1
   Fail: (8) length_2([1, 2, 3], 5)
false.

并关闭轨迹

[trace] ?- notrace.
true.

[debug] ?- nodebug.
true.

我不会浏览跟踪输出中的每一行,但如果您理解语法统一并且可以跟踪跟踪,那么在完成给出的示例之后,您将看到Prolog中的变量如何统一,从而导致与命令相比时的不同模式节目 .

请记住,变量仅在Prolog中绑定一次,并且从不重新分配,并且括号中的跟踪左侧的数字,例如, (10),是堆栈级别,所以当再次调用谓词时,一组新的变量可用,虽然看起来正在重新分配一个值,但它实际上是堆栈中的另一个变量,只是在另一个stack frame .

顺便说一下,在学习Prolog的时候,我给出的一条建议是,如果你把你对命令式和函数式编程的了解放在一边,除了可能的递归之外,它更容易学习,并从头开始统一然后backward chaining .

如果您可以阅读OCaml,here是统一和反向链接的简化版本 . 请注意,这不是Prolog,因为它没有列表或切割运算符,但如果您能理解它,那么统一和反向链接的方式就变得明显了 .

我必须补充一点,我对我的答案并不完全满意,因为我知道你是初学者而且这个回答是需要消化的大量信息,需要您做很多工作才能完成4个跟踪示例 . 然而它确实回答了这个问题,并提供了一个实际的例子,骨头上的肉足够多了 . 我正在努力想出一个更好的例子,其中包括logical purity,这表明不仅统一而且关系是如何在一个谓词中完成多个模式的关键 . 很高兴我没有使用广义相对论作为相对主义者约翰阿奇博尔德·惠勒的翻译, spacetime tells matter how to move; matter tells spacetime how to curve .

2 years ago

我已经做了几年的Prolog,我觉得我对不同实例化模式的安慰和理解已经分成几个步骤 . 第一个重要的障碍当然是递归,这是你真正需要解决这个问题 . 基本上,你知道如果他们说同一种语言你的两个人的表分配是正确的,所以这是你的基本情况:

table_seating([X,Y]) :- speaksSame(X, Y).

那么,如果你添加第三个人怎么办?你会做这样的事情:

% for exposition only; do not include this clause
table_seating([A,X,Y]) :- speaksSame(A,X), speaksSame(X, Y).

现在希望你注意到你的新作品是 speaksSame(A,X) 但你的旧作仍然保持不变 . 让我们担心我们可以为列表的其余部分处理它的新人和信任 .

table_seating([X,Y,Z|Rest]) :- 
   speaksSame(X, Y),
   table_seating([Y,Z|Rest]).

我们在这里做的是说,假设列表中至少有三个项目 . 然后,如果前两个说同一种语言,接下来的两个加上其余的就可以坐下,那么他们都可以坐下来 . 如果他们的语言与 table 前面的人说的语言相同,您可以随时拿一张正确放置的 table 并将一个人添加到 table 的前面 .

递归几乎总是有这样的味道:我如何设置最小的正确情况,基本情况,然后,我如何才能正确地添加一个东西呢?

现在有趣的是,如果你为这个谓词提供一些长度的列表,它将“正常工作”并产生该长度的解 . 试试吧:

?- length(L, 6), table_seating(L).

您可能会得到解决方案(我假设 speaksSame/2 将生成解决方案) . 这是因为所有Prolog都知道这些变量,它知道因为你的 speaksSame/2 谓词 . 因此,只要您在谓词中使用具有许多实例化模式的谓词,并且不强制分配事物或奇怪地命令事物,通常您的谓词将继承这些模式 . 这是我建议人们使用 succ/2 而不是 N is N0 + 1N0 is N - 1 的原因,因为 succ/2 定义了两个数字之间的关系而不是执行某些算术(clpfd更多地采用了这个想法) .