|
From: | A-S Saidi |
Subject: | Re: Some clarification |
Date: | Mon, 05 Sep 2005 17:47:12 +0200 |
User-agent: | Mozilla Thunderbird 1.0.2 (X11/20050317) |
Dear Cliff, I'm trying to answer to your question. Suppose the following program : 1) natural(0). 2) natural(succ(N)) :- 3) natural(N). and some questions submitted to the Prolog engine: 4) ? |- natural(0). => yes 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) . => X=0 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. regards. Alex. Cliff Bender a écrit : Hi, -- Aleksander S. Saidi Ecole Centrale de Lyon Département Mathématiques-Informatique Mél : address@hidden Tél : 04.72.18.65.30, Fax : 04.78.33.16.15 |
Alexandre.Saidi.vcf
Description: Vcard
[Prev in Thread] | Current Thread | [Next in Thread] |