Pourquoi fonctionne ce prédicat Prolog?

Question

Je le code suivant: Gardez à l'esprit que, si ce code fonctionne sur les listes, ces listes représentent des ensembles, donc [1,1,2,2,3,3] et [1,2,3] devrait être équivalent.

%contains(L1, L2), returns true if L1 contains L2
contains(_, []).
contains(L1, [Head|Tail]) :- member(Head, L1), contains(L1, Tail).
%equals(L1, L2), returns true if L1 is equal to L2
equals([X|L1],[X|L2]) :- equals(L1, L2).
equals(L1, L2) :- contains(L1, L2), contains(L2, L1).

L'idée est que equals ([1,2,3], [1,2,1,3]) doit renvoyer true. Toutefois, selon la définition ci-dessus ce que j'attendre à passer est le suivant:

1. est égal à ([1,2,3], [1,2,1,3]) correspond à la première règle, et fait appel égal à égal ([2,3], [2,1,3]]).
2. est égal à ([2,3], [2,1,3]]) correspond à la seconde règle et contient invoque ([2,3], [2,1,3]), contient ([2,1,3], [2,3]).
3. contient ([2,3], [2,1,3]) tombe en panne, et est égal à n ° rendements

Et pourtant, cela fonctionne encore. Et ainsi faire d'autres tentatives de le confondre. Quelqu'un peut-il me l'expliquer?

(mise en œuvre Prolog: SWI-Prolog Version 2.7.12)

Answer 1

Prolog utilise une technique appelée "retours en arrière".

Jetez un oeil à la première étape, l'étape 1.

Prolog a deux règles qu'il peut utiliser ici, si elle utilise la règle que vous avez choisi dans votre explication, il échouera toujours. Mais une fois qu'il a échoué, Prolog revenir en arrière et essayer l'autre règle:

equals ([1,2,3], [1,2,1,3]): - contient ([1,2,3], [1,2,1,3]), contient ([1 , 2,1,3] [1,2,3])

Par retour en arrière à plusieurs reprises après avoir trouvé des réponses fausses, éventuellement Prolog trouve une solution qui est vrai, et donc il connaît la réponse est vrai.

Si si essayé tous les moyens possibles d'appliquer les règles, sans trouver une vraie réponse, la réponse doit être fausse.

Ceci est une partie fondamentale de Prolog. Je suis surpris que vous avez obtenu jusqu'ici sans le comprendre.

Answer 2

Votre code est très étrange, mais je peux vous recommander d'utiliser prédicat trace à des fins de test. Voici l'exemple:

4 ?- trace([equals,contains]).
%         equals/2: [call, redo, exit, fail]
%         contains/2: [call, redo, exit, fail]
true.

[debug] 5 ?- equals([1,2,3],[1,2,1,3]).
 T Call: (7) equals([1, 2, 3], [1, 2, 1, 3])
 T Call: (8) equals([2, 3], [2, 1, 3])
 T Call: (9) equals([3], [1, 3])
 T Call: (10) contains([3], [1, 3])
 T Fail: (10) contains([3], [1, 3])
 T Fail: (9) equals([3], [1, 3])
 T Redo: (8) equals([2, 3], [2, 1, 3])
 T Call: (9) contains([2, 3], [2, 1, 3])
 T Call: (10) contains([2, 3], [1, 3])
 T Fail: (10) contains([2, 3], [1, 3])
 T Fail: (9) contains([2, 3], [2, 1, 3])
 T Fail: (8) equals([2, 3], [2, 1, 3])
 T Redo: (7) equals([1, 2, 3], [1, 2, 1, 3])
 T Call: (8) contains([1, 2, 3], [1, 2, 1, 3])
 T Call: (9) contains([1, 2, 3], [2, 1, 3])
 T Call: (10) contains([1, 2, 3], [1, 3])
 T Call: (11) contains([1, 2, 3], [3])
 T Call: (12) contains([1, 2, 3], [])
 T Exit: (12) contains([1, 2, 3], [])
 T Exit: (11) contains([1, 2, 3], [3])
 T Exit: (10) contains([1, 2, 3], [1, 3])
 T Exit: (9) contains([1, 2, 3], [2, 1, 3])
 T Exit: (8) contains([1, 2, 3], [1, 2, 1, 3])
 T Call: (8) contains([1, 2, 1, 3], [1, 2, 3])
 T Call: (9) contains([1, 2, 1, 3], [2, 3])
 T Call: (10) contains([1, 2, 1, 3], [3])
 T Call: (11) contains([1, 2, 1, 3], [])
 T Exit: (11) contains([1, 2, 1, 3], [])
 T Exit: (10) contains([1, 2, 1, 3], [3])
 T Exit: (9) contains([1, 2, 1, 3], [2, 3])
 T Exit: (8) contains([1, 2, 1, 3], [1, 2, 3])
 T Exit: (7) equals([1, 2, 3], [1, 2, 1, 3])
true