quelqu'un peut-il m'aider à comprendre cet exemple prologue récursif?

Question

est ici le code, plus que je ne comprends pas

plus(0,X,X):-natural_number(X). 
plus(s(X),Y,s(Z)) :- plus(X,Y,Z). 

tout donné:

natural_number(0). 
natural_number(s(X)) :- natural_number(X). 

Je ne comprends pas ce récursivité. Si j'ai plus(s(0),s(s(s(0))),Z) comment puis-je obtenir la réponse de 1+3=4?

J'ai besoin d'explications sur le premier code. J'essaie que plus(0,X,X) va arrêter la récursivité mais je pense que je le fais mal.

Answer 1

Alors, commençons par natural_number(P). Lisez ceci comme "P est un nombre naturel". On nous donne natural_number(0)., ce qui nous indique que 0 est toujours un nombre naturel (c'est-à-dire qu'il n'y a pas de conditions qui doivent être remplies pour que ce soit un fait). natural_number(s(X)) :- natural_number(X). nous indique que s(X) est un nombre naturel si X est un nombre naturel. C'est la définition inductive normale des nombres naturels, mais écrite "en arrière" comme nous lisons Prolog "Q: = P" comme "Q est vrai si P est vrai".

Maintenant, nous pouvons regarder plus(P, Q, R). Lisez ceci comme "plus est vrai si P plus Q est égal à R". Nous examinons ensuite les cas qu'on nous donne:

1. plus(0,X,X) :- natural_number(X).. Lire comme ajouter 0 à X donne X si X est un nombre naturel. C'est notre cas de base inductif, et c'est la définition naturelle de l'addition. Lire comme "Ajouter le successeur de X à Y donne le successeur Z si l'addition de X à Y est Z." Si on change la notation, on peut la lire algébriquement comme "X + 1 + Y = Z + 1" si X + Y = Z », ce qui est très naturel à nouveau.

donc, pour vous répondre à la question directe: « Si je plus(s(0),s(s(s(0))),z), comment puis-je obtenir la réponse de 1 + 3 = 4? », considérons comment nous pouvons unifier quelque chose avec z chaque étape de l'induction

1. Appliquer la deuxième définition de plus, car il est le seul qui unifie avec la requête. plus(s(0),s(s(s(0))), s(z')) est vrai si plus(0, s(s(s(0))), z') est vrai pour certains z
2. Maintenant, appliquez la première définition de plus, car il est la seule définition fédératrice: plus(0, s(s(s(0))), z') si z' est s(s(s(0))) et s(s(s(0))) est un nombre naturel.Déroulez la définition de natural_number quelques fois sur s(s(s(0))) pour voir que c'est vrai.
3. Donc l'énoncé global est vrai, si s(s(s(0))) est unifié avec z' et s(z') est unifié avec z.

Ainsi, l'interprète retourne vrai, avec z' = s(s(s(0))) et z = s(z'), à savoir z = s(s(s(s(0)))). Donc, z est 4.

Answer 2

Vous n'obtiendrez pas de termes numériques comme 1+3=4, tout ce que vous obtenez est le terme s/1 qui peut s'enfoncer dans n'importe quelle profondeur et ainsi représenter n'importe quel nombre naturel. Vous pouvez combiner ces termes (en utilisant plus/3) et réaliser ainsi la sommation.

Notez que votre définition de plus/3 n'a rien à voir avec SWI-Prolog plus/3 intégré de (qui fonctionne avec des nombres entiers et non avec les s/1 termes):

?- help(plus). 
plus(?Int1, ?Int2, ?Int3) 
    True if Int3 = Int1 + Int2. 
    At least two of the three arguments must be instantiated to integers. 

Answer 3

Ce code est une implémentation simple de addition in Peano arithmetic.

En arithmétique Peano, les nombres naturels sont représentés en utilisant la constante 0 et la fonction unaire s. Alors s(0) est une représentation de 1, s(s(s(0))) est une représentation de 3. Et plus(s(0),s(s(s(0))),Z) vous donnera Z = s(s(s(s(0)))), qui est une représentation de 4.