Kann mir bitte mal einer erklären, warum die add Rekursion abläuft, wie sie abläuft ?

vielen lieben Dank !

[trace] ?- add(s(s(0)), s(s(s(0))),X). Call: (7) add(s(s(0)), s(s(s(0))), _G325) ? creep Call: (8) add(s(0), s(s(s(0))), _G388) ? creep Call: (9) add(0, s(s(s(0))), _G390) ? creep Exit: (9) add(0, s(s(s(0))), s(s(s(0)))) ? creep Exit: (8) add(s(0), s(s(s(0))), s(s(s(s(0))))) ? creep Exit: (7) add(s(s(0)), s(s(s(0))), s(s(s(s(s(0)))))) ? creep X = s(s(s(s(s(0))))) Yes

Ich versuchs mal grob, das Prädikat hat ja die Form add(A, B, X), womit man X = A+B berechnet. Nun kann man erstmal einfach sagen:
B = 0 + B

Dies sieht man in dem Trace hier:
Exit: (9) add(0, s(s(s(0))), s(s(s(0)))) ? creep

wenn der eine Operand ne 0 ist, ist die Addition trivial. Nun kann man wenn man zwei Zahlen hat so vorgehen:
A + B = ((A-1) + B) + 1
man nimmt also vom ersten Operanden einfach mal einen weg und addiert den am Ende auf. Dieses Wegnehmen sieht man in den ersten Calls:
Call: (7) add(s(s(0)), s(s(s(0))), _G325) ? creep
Call: (8) add(s(0), s(s(s(0))), _G388) ? creep
Call: (9) add(0, s(s(s(0))), _G390) ? creep

Dabei muss natürlich immer notiert werden, wie tief man in der Rekursion schon drin ist. So ist notiert, dass man bei _G325 noch keinen abgewickelt hat, bei _G388 muss einer draufaddiert werden und bei _G390 schon 2.

Bei _G390 kann man dann die erste Regel anwenden, also _G390 mit s(s(s(0))) unifizieren. Dort angekommen können wir nun die rekursion wieder hochkriechen und für jeden Schritt den wir runtergegangen sind wieder einen hoch, so kommen die zwei fehlenden dazu:
Exit: (8) add(s(0), s(s(s(0))), s(s(s(s(0))))) ? creep
Exit: (7) add(s(s(0)), s(s(s(0))), s(s(s(s(s(0)))))) ? creep

HTH

ich dachte immer das der erste ne abbruchbedingung ist?! demnach müsste er schluss machen und die rekursion nicht wieder hochkriechen?!

wieso unifiziert er _G390 mit dem zweiten wert??? kann man hinter de _Gxxx irgendwas erkennen oder sind das "speicheradressen"?

kann man hinter de _Gxxx irgendwas erkennen oder sind das "speicheradressen"?

Die _Gxxx sind variablen, die Maschine grade benutzt, aber variablen sind ja referenzen auf Speicheradressen. Bei jedem Schritt muss er das Zwischenresultat in einer Variable speichern, deswegen unifiziert man.
ich glaube aber dass ich deine Frage falsch verstanden habe oder ?-

nönö der teil war schon richtig… hab ich mir auch so gedacht ;-)

nur warum er unifiziert wüsste ich nu gerne weil ja eben das erste ne abbruchbedingung is soweit ich weiss…

Ja aber ne Abbruchbedingung heisst nur dass er nicht wieder in die Rekursion reingeht. Aber trotzdem muss er unifizieren. z.B Wenn die Abbruchbedingung sum(0,B,B). ist dann unifiziert er Aber bei der Anfrage sagst du z.B sum(0,s(s(0)),X). dann muss er X = s(s(0)) unifizieren.

also unifiziert er wirklich wegen dem ersten prädikat…

also rekursion runter bist bedingung erfüllt und dann rekursion wieder hoch bis ausgang wieder erreicht… z is dann ergebnis

Gib mal

?- guitracer.
vor dem trace an - du bekommst ne schicke kleine GUI, mit der man sich durch die Rekursionsschritte durchklicken kann, samt Übersicht über die Variablenbindungen etc…. Hilft vielleicht beim Verständnis.