Può uno aiutarmi a capire questo esempio prologo ricorsivo?

Question

qui è la più codice che non capisco

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

mentre dato:

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

Non capisco questo ricorsione. Se ho plus(s(0),s(s(s(0))),Z) come posso ottenere la risposta di 1+3=4?

Ho bisogno di qualche spiegazione per il primo codice. Provo che plus(0,X,X) fermerà la ricorsione, ma penso che lo faccio di sbagliato.

Answer 1

Quindi, cominciamo con natural_number(P). Leggere questo come "P è un numero naturale". Stiamo dato natural_number(0)., che ci dice che 0 è sempre un numero naturale (vale a dire non ci sono le condizioni che devono essere soddisfatte per essere un dato di fatto). natural_number(s(X)) :- natural_number(X). ci dice che s(X) è un numero naturale se X è un numero naturale. Questa è la definizione induttiva normale dei numeri naturali, ma scritte "a ritroso", come si legge Prolog "Q: = P". Come "Q è vero se P è vera"

Ora si può guardare plus(P, Q, R). Leggere questo come "plus è vero se P oltre a Q come R". Abbiamo poi guardiamo i casi stiamo dato:

1. plus(0,X,X) :- natural_number(X).. Leggi come l'aggiunta di 0 a X risultati in X se X è un numero naturale. Questo è il nostro caso base induttiva, ed è la definizione naturale aggiunta.
2. plus(s(X),Y,s(Z)) :- plus(X,Y,Z). Leggi come "Aggiungere il successore di X ai risultati Y nel successore Z se l'aggiunta di X a Y è Z'. Se cambiamo la notazione, si può leggerlo algebricamente come "X + 1 + Y = Z + 1 se X + Y = Z", che è ancora molto naturale.

Quindi, per rispondere si domanda diretta "Se ho plus(s(0),s(s(s(0))),z), come posso ottenere la risposta di 1 + 3 = 4?", Prendiamo in considerazione come possiamo unire qualcosa con z ogni passo dell'induzione

1. Applicare la seconda definizione di plus, in quanto è l'unico che unifica con la query. plus(s(0),s(s(s(0))), s(z')) è vero se plus(0, s(s(s(0))), z') è vero per alcuni z
2. Ora applicare la prima definizione di più, in quanto è la definizione solo unificando:. plus(0, s(s(s(0))), z') se z' è s(s(s(0))) e s(s(s(0))) è un numero naturale
3. Svolgere la definizione di natural_number un paio di volte su s(s(s(0))) per vedere che è vero.
4. Quindi, l'affermazione generale è vero, se s(s(s(0))) è unificato con z' e s(z') è unificato con z.

Quindi, l'interprete restituisce true, con z' = s(s(s(0))) e z = s(z'), vale a dire z = s(s(s(s(0)))). Quindi, z è 4.

Answer 2

Questo codice è un'implementazione semplice di Oltre a Peano .

In Peano, numeri naturali sono rappresentati utilizzando la costante 0 e la funzione s unaria. Così s(0) è una rappresentazione di 1, s(s(s(0))) è la rappresentazione di 3. E plus(s(0),s(s(s(0))),Z) vi darà Z = s(s(s(s(0)))), che è una rappresentazione di 4.

Answer 3

Non si ottiene termini numerici come 1+3=4, tutti si ottiene è il termine s/1 che si può incorporare a qualsiasi profondità e quindi può rappresentare qualsiasi numero naturale. È possibile combinare tali termini (utilizzando plus/3) e, quindi, ottenere sommando.

Si noti che la tua definizione di plus/3 non ha nulla a che fare con di SWI-Prolog built-in plus/3 (che lavora con numeri interi e non con i termini s/1):

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