Du commentaire:

Comment le résultat de R est-il correct, parce que si vous regardez ma course d'un appel de programme, la valeur de Xs n'est pas [1,3], c'est ce qu'elle finalement les sorties; c'est plutôt [3] qui unifie à R (clairement je suis il manque quelque chose en cours de route, mais je ne sais pas ce que c'est).

Ceci est correct:

val_and_remainder(X,[Y|Ys],[Y|R])

cependant Prolog n'est pas comme les autres langages de programmation où vous entrez avec une entrée et sortez avec une sortie à une instruction de retour. Dans Prolog, vous avancez dans les instructions de prédicat en unifiant et en continuant avec des prédicats qui sont vrais, et lors du retour en arrière, unifiez également les variables indépendantes. (Ce n'est pas techniquement correct mais c'est plus facile à comprendre pour certains si vous y pensez de cette façon.)

Vous n'avez pas pris en compte les variables indépendantes qui sont maintenant liées au retour en arrière. P >

Lorsque vous atteignez le cas de base Xs était lié à [3 ,

mais lorsque vous revenez en arrière, vous regardez p >

val_and_remainder(2, [1,2,3], R).

et en particulier [1 | R] pour le troisième paramètre.

Puisque Xs a été unifié avec R dans l'appel au cas de base, c'est-à-dire que

val_and_remainder(2, [1|[2,3]], [1|R])

R a maintenant [3] .

Maintenant, la troisième position du paramètre dans

val_and_remainder(X,[X|Xs],Xs).

est [1 | R] qui est [1 | [3]] qui en tant que sucre syntaxique est [1,3] et pas seulement [3 .

Maintenant lors de l'exécution de la requête

val_and_remainder(2, [1|[2,3]], [1|R])

, le troisième paramètre de la requête R était unifié avec le troisième paramètre du prédicat

% Initial call
val_and_remainder(2, [1,2,3], R).

val_and_remainder(2, [1|[2,3]], [1|R]) :- val_and_remainder(2, [2,3], R).

% Hits base case
val_and_remainder(2, [2|[3]], [3]).

donc R a été unifié avec [Y | R] whi ch unpon backtracking est [1,3] et donc la valeur liée à la variable de requête R est [1,3edral

Dans Prolog, vous devez considérer les prédicats pas comme des fonctions comme vous le feriez normalement dans d’autres langues. Les prédicats décrivent des relations qui peuvent inclure des arguments qui aident à définir cette relation.

Par exemple, prenons ce cas simple:

val_and_remainder(X, [Y|Ys], [Y|R]) :- 
    val_and_remainder(X, Ys, R).

Ceci est un prédicat qui définit une relation entre deux arguments. Grâce à l ' unification , cela signifie que le premier et le deuxième arguments sont les mêmes s'ils sont unifiés (et cette définition est à nous, les auteurs du prédicat). Ainsi, same_term (a, a) réussira, same_term (a, b) échouera et same_term (a, X) réussira avec X = a .

Vous pouvez également écrire ceci sous une forme plus explicite:

val_and_remainder(X, [H|T], R) :-
    X = H,
    R = T.

Regardons maintenant votre exemple, val_and_remainder / 3 . Tout d'abord, qu'est-ce que cela signifie?

val_and_remainder(X,[X|Xs],Xs).

Cela signifie que X est un élément de List et Rest est une liste composée de tous les autres éléments (sans X ). (REMARQUE: vous n'avez pas expliqué cette signification tout de suite, mais je détermine cette signification à partir de l'implémentation de votre exemple.)

Nous pouvons maintenant écrire pour décrire les règles. Tout d'abord, un cas de base simple:

val_and_remainder(X, List, Rest)

Ceci dit que:

Xs est le reste de la liste [X | Xs] sans X .

Cette déclaration devrait être assez évidente par la définition de la syntaxe [X | Xs] pour une liste dans Prolog. Vous avez besoin de tous ces arguments car le troisième argument Xs doit s'unifier avec la queue (reste) de la liste [X | Xs] , qui est alors aussi Xs (les variables du même nom sont, par définition, unifiées). Comme précédemment, vous pouvez écrire ceci plus en détail comme suit:

same_term(X, Y) :-
    X = Y.  % X and Y are the same if they are unified

Mais la forme courte est en fait plus claire.

Maintenant, la clause récursive dit:

same_term(X, X).

Cela signifie donc:

[Y | R] est le reste de la liste [Y | Ys] sans X si R est le reste de la liste Ys sans l'élément X .

Vous devez réfléchir à cette règle pour vous convaincre qu'elle est logiquement vraie. Le Y est le même dans le deuxième et le troisième arguments car ils font référence au même élément, ils doivent donc s'unifier.

Ces deux clauses de prédicat forment donc deux règles qui couvrent les deux cas . Le premier cas est le cas simple où X est le premier élément de la liste. Le second cas est une définition récursive pour quand X n'est pas le premier élément.

Lorsque vous faites une requête, telle que val_and_remainder (2, [1,2, 3], R). Prolog cherche à voir s'il peut unifier le terme val_and_remainder (2, [1,2,3], R) avec un fait ou la tête de l'une de vos clauses de prédicat. Il échoue dans sa tentative d'unification avec val_and_remainder (X, [X | Xs], Xs) car il aurait besoin d'unifier X avec 2 , ce qui signifie qu'il faudrait unifier [1,2,3] avec [2 | Xs] qui échoue depuis le premier élément de [1,2, 3] vaut 1, mais le premier élément de [2 | Xs] est 2.

Donc Prolog avance et unifie avec succès val_and_remainder (2, [1,2,3], R) avec val_and_remainder (X, [Y | Ys], [Y | R]) en unifiant X avec 2 , Y avec 1, Ys avec [2,3] et R avec [Y | R] (REMARQUE, ceci est important, la variable R dans votre appel n'est PAS la même que la variable R dans la définition du prédicat, nous devrions donc nommer ce R1 pour éviter cette confusion). Nous nommerons votre R R1 et dirons que R1 est unifié avec [Y | R] .

Lorsque le corps de la deuxième clause est exécuté, il appelle val_and_remainder (X, Ys, R). ou, en d'autres termes, val_and_remainder (2, [2, 3], R) . Cela s'unifiera maintenant avec la première clause et vous donnera R = [3] . Lorsque vous détendez tout cela, vous obtenez, R1 = [Y | [3]] , et en vous rappelant que Y était lié à 1, le résultat est R1 = [1,3] .

La reproduction par étapes du mécanisme de Prolog conduit souvent à plus de confusion qu’elle n’aide. Vous avez probablement des notions comme «renvoyer» signifiant quelque chose de très spécifique - plus approprié aux langages impératifs.

Voici différentes approches que vous pouvez toujours utiliser:

Posez la requête la plus générale

... et laissez Prolog vous expliquer de quoi il s'agit.

| ?- val_and_remainder(x, [x,a,x], Ys).
     Ys = [a,x]
  ;  Ys = [x,a]
  ;  false.

Ainsi, Xs et Ys partagent un préfixe de liste, Xs a ensuite un X , suivi d'un repos commun. Cette requête continuerait à produire des réponses supplémentaires. Parfois, vous voulez voir toutes les réponses, alors vous devez être plus précis. Mais ne soyez pas trop précis:

| ?- val_and_remainder(X, Xs, Ys), val_and_remainder(X, Xs, Ys2), dif(Ys,Ys2).
     Xs = [X,_A,X|_B],
     Ys = [_A,X|_B],
     Ys2 = [X,_A|_B],
     dif([_A,X|_B],[X,_A|_B])
  ;  ...

Nous avons donc ici toutes les réponses possibles pour une liste à quatre éléments. Tous.

Tenez-vous en aux objectifs au sol lorsque vous passez par des inférences spécifiques

Donc, au lieu de val_and_remainder (2, [1,2,3], R). code> (qui a évidemment fait tourner la tête) plutôt considérer val_and_remainder (2, [1,2,3], [1,3]). puis val_and_remainder (2, [2,3], [3]) . De ce côté, cela devrait être évident.

Lire les règles Prolog de droite à gauche

Voir les règles Prolog comme règles de production. Ainsi, chaque fois que tout tient du côté droit d'une règle, vous pouvez conclure ce qui est sur la gauche. Ainsi, le : - est une représentation du début des années 1970 d'un ←

Plus tard, vous voudrez peut-être aussi réfléchir à des questions plus complexes. Comme

Dépendances fonctionnelles

Le premier et le deuxième argument déterminent-ils de manière unique le dernier? Est-ce que X , Xs → Ys est valable?

Voici un exemple de requête qui demande que Ys et Ys2 soient différents pour les mêmes X et Xs .

| ?- Xs = [_,_,_,_], val_and_remainder(X, Xs, Ys).
     Xs = [X,_A,_B,_C],
     Ys = [_A,_B,_C]
  ;  Xs = [_A,X,_B,_C],
     Ys = [_A,_B,_C]
  ;  Xs = [_A,_B,X,_C],
     Ys = [_A,_B,_C]
  ;  Xs = [_A,_B,_C,X],
     Ys = [_A,_B,_C]
  ;  false.

Donc, apparemment, il y a des valeurs différentes pour Ys pour un X et un Xs . Voici un exemple concret:

| ?- val_and_remainder(X, Xs, Ys).
     Xs = [X|Ys]
  ;  Xs = [_A,X|_B],
     Ys = [_A|_B]
  ;  Xs = [_A,_B,X|_C],
     Ys = [_A,_B|_C]
  ;  Xs = [_A,_B,_C,X|_D],
     Ys = [_A,_B,_C|_D]
  ;  Xs = [_A,_B,_C,_D,X|_E],
     Ys = [_A,_B,_C,_D|_E]
  ; ...

Il n'y a pas de retour classique ici. Il ne revient pas une mais deux fois. C'est plus un yield .

Pourtant, il y a en fait une dépendance fonctionnelle entre les arguments! Peux-tu le trouver? Et pouvez-vous le prouver du point de vue de Prolog (autant que Prolog peut en faire une preuve)?

Je ne comprends pas le nom de votre prédicat. C'est de toute façon une distraction. La dénomination non uniforme des variables est également une distraction. Utilisons des noms neutres et courts d'une syllabe pour nous concentrer sur le code lui-même dans sa forme la plus claire:

2 ?- proof(2).
true.

3 ?- proof(3).
true.

4 ?- proof(4).
true.

5 ?- proof(5).
true.

Il s'agit donc du select / 3 . Yay !..

Maintenant vous posez la question sur la requête foo (2, [1,2,3], R) et comment R obtient sa valeur définie correctement. La principale chose qui manque dans votre récapitulatif est le changement de nom des variables lorsqu'une clause correspondante est sélectionnée. La résolution de la requête est la suivante:

ground_list(LEN,L):-
  findall(N, between(1,LEN,N), NS), 
  member(N,NS),
  length(L,N), 
  maplist( \A^member(A,NS), L).

bcs(N, BCS):- 
  bagof(B-C, A^(ground_list(N,B),ground_list(N,C),foo(A,B,C)), BCS).

as(N, AS):- 
  bagof(A, B^C^(ground_list(N,B),ground_list(N,C),foo(A,B,C)), AS).

proof(N):-
  as(N,AS), bcs(N,BCS), 
  length(AS,N1), length(BCS, N2), N1 =:= N2.

Les objectifs entre | - et ? sont la résolvante , les équations à l'intérieur de {} sont la substitution . La base de connaissances (KB) est implicitement à gauche de | - dans son intégralité.

A chaque étape, le but le plus à gauche dans la résolvante est choisi, une clause avec la tête correspondante est choisie parmi celles de la KB ^{(en renommant strong> toutes les variables de la clause de manière cohérente, de sorte qu'aucune variable dans la résolution ne soit utilisée par la clause renommée, donc il n'y a pas de capture de variable accidentelle)} , et l'objectif choisi est remplacé dans le résolvant avec le corps de cette clause, tandis que l'unification réussie est ajoutée à la substitution. Lorsque la résolvante est vide, la requête a été prouvée et ce que nous voyons est celle qui réussit et -branch dans l'ensemble et-ou arbre .

Voici comment une machine pourrait faire il. Les étapes de "réécriture" sont introduites ici pour faciliter la compréhension humaine.

Nous pouvons donc voir ici que la première sélection de clause réussie aboutit à l'équation

28 ?- length(BB,NN), foo(AA,BB,CC), XX=[AA,BB,CC], numbervars(XX), 
      writeln(XX), (NN>3, !, fail).
[A,[A],[]]
[A,[A,B],[B]]
[A,[B,A],[B]]
[A,[A,B,C],[B,C]]
[A,[B,A,C],[B,C]]
[A,[B,C,A],[B,C]]
[A,[A,B,C,D],[B,C,D]]
false.

29 ?- length(BB,NN), foo(AA,BB,CC), foo(AA2,BB,CC), 
      XX=[AA,AA2,BB,CC],  numbervars(XX), writeln(XX), (NN>3, !, fail).
[A,A,[A],[]]
[A,A,[A,B],[B]]
[A,A,[A,A],[A]]
[A,A,[A,A],[A]]
[A,A,[B,A],[B]]
[A,A,[A,B,C],[B,C]]
[A,A,[A,A,B],[A,B]]
[A,A,[A,A,A],[A,A]]
[A,A,[A,A,B],[A,B]]
[A,A,[B,A,C],[B,C]]
[A,A,[B,A,A],[B,A]]
[A,A,[A,A,A],[A,A]]
[A,A,[B,A,A],[B,A]]
[A,A,[B,C,A],[B,C]]
[A,A,[A,B,C,D],[B,C,D]]
false.

, et le second, -

10 ?- dif(A1,A2), foo(A1,B,C), foo(A2,B,C).
Action (h for help) ? abort
% Execution Aborted

, qui ensemble impliquent

2 ?- foo( A, [0,1,2,1,3], [0,2,1,3]).
A = 1 ;
false.

3 ?- foo( A, [0,1,2,1,3], [0,1,2,3]).
A = 1 ;
false.

4 ?- foo( A, [0,1,2,1,3], [0,1,2,4]).
false.

f ?- foo( A, [0,1,1], [0,1]).
A = 1 ;
A = 1 ;
false.

Cette instanciation / optimisation progressive descendante -en dehors des listes est une manière très caractéristique de Prolog de faire les choses.

En réponse au défi de la prime, concernant la dépendance fonctionnelle dans la relation foo / 3 (ie select / 3 ): dans foo (A, B, C) , deux valeurs au sol quelconques pour B et C déterminent de manière unique la valeur de A ( ou son absence):

     R = [1,        3]

Tentative de réfuter par un contre-argument:

              R1 = [3]

Le prologue ne parvient pas à trouver un contre-argument.

Liens pour voir de plus près ce qui se passe, avec un approfondissement itératif:

     R = [1 | R1     ]

AA et AA2 code> sont toujours instanciés sur la même variable.

Il n'y a rien de spécial à propos du nombre 3, il est donc prudent de conjecturer par généralisation qu'il en sera toujours ainsi, quelle que soit la longueur essayée.

Une autre tentative de preuve Prolog -wise:

|-  foo( 2, [1,2,3], R) ? { } 
  %% SELECT -- 1st clause, with rename
  |-  ?  { foo( H1, [H1|T1], T1) = foo( 2, [1,2,3], R) }
         **FAIL** (2 = 1)
         **BACKTRACK to the last SELECT**
  %% SELECT -- 2nd clause, with rename
  |-  foo( X1, T1, R1) ?
         { foo( X1, [H1|T1], [H1|R1]) = foo( 2, [1,2,3], R) }
         **OK**
    %% REWRITE
    |-  foo( X1, T1, R1) ?
          { X1=2, [H1|T1]=[1,2,3], [H1|R1]=R }
    %% REWRITE
    |-  foo( 2, [2,3], R1) ?  { R=[1|R1] } 
      %% SELECT -- 1st clause, with rename
      |-  ? { foo( H2, [H2|T2], T2) = foo( 2, [2,3], R1), R=[1|R1] }
             ** OK ** 
        %% REWRITE
        |-  ? { H2=2, T2=[3], T2=R1, R=[1|R1] }
        %% REWRITE
        |-  ? { R=[1,3] }
        %% DONE

Ceci compare le nombre de combinaisons BC réussies dans l'ensemble avec le nombre de Un s qu'ils produisent. L'égalité signifie une correspondance un à un.

Et donc nous avons,

foo( H, [H | T], T).                          % 1st clause

foo( X, [H | T], [H | R]) :- foo( X, T, R).   % 2nd clause

Et donc pour tout N qu'il contient . De plus en plus lent. Une requête générale et illimitée est simple à écrire, mais le ralentissement semble exponentiel.