|Subject:||Re: Some clarification|
|Date:||Tue, 6 Sep 2005 21:35:51 -0400|
I'm trying to answer to your question.
Suppose the following program :
2) natural(succ(N)) :-
and some questions submitted to the Prolog engine:
4) ? |- natural(0).
Prolog engine compared the "goal" (the question 4) and the "natural" predicate cluases (i.e., the rules 1 & 2). The clause (1) was exactly the same as the goal (4).
One says that Prolog "unified" (1) and (4). Simply speaking, the engine tried to make (1) and (4) lexically the same. During the unification, variables may recieve a "value" (not in this case, see below).
5)- ? |- natural(X) .
Again, the engine unified (5) and (1). This time, X is "associated" (bound) to the constant 0. This is done in order to make them the SAME. The couple [X / 0] is called a "substitution" and X in the goal is "instanciated" to 0.
6) If you hit ';' for more answers, then you'll have :
=> X= succ(0)
Prolog tries to resatsfy the goal. Prolog engine "forgets" the first answer. The effect of the step 6 is thrown away and X in the goal becomes a variable as before but the engine knows that (1) was alreday tried.
This time, (5) is unifed to left part of (2) giving the substitution [ X / succ(N) ]. Then, the engine has to see if the right part of (2) can succeed. Therefor, the new (sub) goal becomes "succ(N)".
As in the above question, this N will capture the value 0 such that the substitution set becomes [ X / succ(N), N / 0 ].
Hence X = succ(0).
This time, X of the "goal" (5) is "instanciated" to succ(0).
6) if you retry ';' again, you'll have the answer succ(succ(0)) and so on (never ends, same as the Natural set which is infinite).
NB : I did not bother here with the "variable renaming" since the example is quite simple. Note that if the goal was "succ(N)" (N instead of X), instances of N in (2) are different from the 'N' in the goal. To avoid this ambiguity, Prolog replaces ("renames") all the variables in the candidate rule (here the rule 2). That is, the inner version of (2) considered is something like :
(2') : natural(succ(N') :- succ(N').
which has the same signification as 2.
Hope this helped.
Cliff Bender a écrit :Hi,
As I read more and try more things, I suspect I'll be asking quite a few questions of everyone. I'd like to thank people in advance for their patience.
Right now, I'd like some clarification on terminology. Specifically, "Goal", "Unify" and "Instantiate". I'm used to programming in php and C/C++, and these concepts are a bit alien to me.
Thanks in advance,
Users-prolog mailing list
Aleksander S. Saidi
Ecole Centrale de Lyon
Mél : address@hidden
Tél : 04.72.18.65.30, Fax : 04.78.33.16.15
|[Prev in Thread]||Current Thread||[Next in Thread]|