¿Alguien puede ayudarme a comprender este ejemplo recursivo de Prolog?

Question

Aquí está el código más que no entiendo

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

Mientras se le da:

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

No entiendo esta recursión. Si tengo plus(s(0),s(s(s(0))),Z) ¿Cómo puedo obtener la respuesta de 1+3=4?

Necesito alguna explicación para el primer código. Lo intento plus(0,X,X) Detendré la recursión, pero creo que lo hago mal.

Answer 1

Entonces, comencemos con natural_number(P). Lea esto como "P es un número natural". Fueron dados natural_number(0)., que nos dice que 0 es siempre un número natural (es decir, no hay condiciones que se deben cumplir para que sea un hecho). natural_number(s(X)) :- natural_number(X). nos dice que s(X) es un número natural si X es un número natural. Esta es la definición inductiva normal de números naturales, pero escrito "hacia atrás" mientras leemos Prolog "Q: = P" como "Q es verdadero si P es verdadero".

Ahora podemos mirar plus(P, Q, R). Lea esto como "plus es cierto si P Plus Q es igual a R ". Luego miramos los casos que se nos dan:

1. plus(0,X,X) :- natural_number(X).. Lea como agregar 0 a x resultados en x si x es un número natural. Este es nuestro caso de base inductiva, y es la definición natural de adición.
2. plus(s(X),Y,s(Z)) :- plus(X,Y,Z). Leer como "Agregar el sucesor de X a Y da como resultado el sucesor z si agregar x a y es z '. Si cambiamos la notación, podemos leerlo algebraicamente como" x + 1 + y = z + 1 si x + y = Z ", que es muy natural nuevamente.

Entonces, para responderle una pregunta directa "si tengo plus(s(0),s(s(s(0))),z), ¿cómo puedo obtener la respuesta de 1+3 = 4? ", Consideremos cómo podemos unificar algo con z cada paso de la inducción

1. Aplicar la segunda definición de plus, ya que es el único que unifica la consulta. plus(s(0),s(s(s(0))), s(z')) es cierto si plus(0, s(s(s(0))), z') es cierto para algunos z
2. Ahora aplique la primera definición de Plus, ya que es la única definición unificadora: plus(0, s(s(s(0))), z') si z' es s(s(s(0))) y s(s(s(0))) es un número natural.
3. Descansar la definición de natural_number unas pocas veces en s(s(s(0))) Ver eso es cierto.
4. Entonces la declaración general es cierta, si s(s(s(0))) está unificado con z' y s(z') está unificado con z.

Entonces el intérprete devuelve verdadero, con z' = s(s(s(0))) y z = s(z'), es decir z = s(s(s(s(0)))). Asi que, z es 4.

Answer 2

Ese código es una implementación directa de Adición en aritmética de manio.

En la aritmética del manista, los números naturales se representan utilizando la constante 0 y la función unaria s. Asi que s(0) es una representación de 1, s(s(s(0))) es representación de 3. y plus(s(0),s(s(s(0))),Z) Te regalaré Z = s(s(s(s(0)))), que es una representación de 4.

Answer 3

No obtendrá términos numéricos como 1+3=4, todo lo que obtienes es el término s/1 que puede incrustarse en cualquier profundidad y, por lo tanto, puede representar cualquier número natural. Puede combinar tales términos (usando plus/3) y así lograr sumando.

Tenga en cuenta que su definición de plus/3 no tiene nada que ver con el incorporado de SWI-Prolog plus/3 (que funciona con enteros y no con el s/1 términos):

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