-
Notifications
You must be signed in to change notification settings - Fork 9
Euler reasoning algorithm
The following was written by HMC and is explaining the js code at http://sourceforge.net/p/eulersharp/code/HEAD/tree/trunk/2006/02swap/classes/Euler4.js#l456
prove() is the main inference loop includes standard back-chaining reasoning (Robertson) plus a "euler path detection" anti-looping check (Runtime productivity check, ensures termination.)
Inputs:
goal - a rule where the body is the query to be matched
maxNumberOfSteps - limits count of transitivities calculated, allows for an early bail-out. -1 to disable
Returns:
undefined ("false") if the reasoner ran to completion
empty string ("true") if the reasoner terminated early by reaching maxNumberOfSteps
Outputs:
Leaves a trace of the resolution path in the "evidence" array
Function outline:
- First a goal queue is initiated, which is a list of goals yet to be dispatched, structured using "evidence frames" which relate a goal rule to be matched with the already-matched rule that prompted it as a goal. Also stores the active environment and ground state at the time that the frame was created, for evidentiary tracking, to establish the proof trace in evidence.
rule: rule to be matched (body)
src: either an integer reference to a case for the head predicate, or a reference to the rule, from which this frame was created. src=0 indicates the root goal (for euler path)
ind: index of the statement within the rule body that is "next" to be matched (for matching and euler path)
parent: a reference to the parent frame that this frame was derived from (for euler path)
env: the active environment bindings for this frame
ground: the active ground state for this frame
You can think of this queue as the "call stack" for the interpreter. When a new rule is decended into, a new frame is added. When a rule is fully matched and "returns" to the parent rule that induced it a frame is popped (and moved to evidence if it was matched).
-
Initialize a local step counter if there is none defined globally
-
Iterate as long as we continue to have a goal which needs to be matched. This is the main inference loop. It will take the top goal from the queue and attempt to match it. If the goal is already entirely matched (or is empty) then the goal is met, and the frame is moved to evidence. If the goal is matched against a rule head, the statements of the rule's body will be added to queue.
-
Take the top of queue ,duplicate its ground state, increase step counter for bailout.
-
check bailout, return true if we're over step count max
-
check if this frame still has any statements to be matched.
-
if it does not, check if the parent is null indicating root goal
-
this is a root goal, iterate over the final environment and copy our evidence frame information into evidence list
-
evaluate the statement in the enviornment
-
initialize this predicate's evidence list, if necessary
-
add the evidence for this statement
-
this rule is done, leave it popped from queue and continue on with the next queue entry
-
parent is not null, so we continue at this depth, adding this matched rule to ground state
-
construct a new frame at the next index of the parent rule, with a copy of the evidence state
-
unify this new frame with our current environment
-
advance to the next statement in the parent frame
-
add this new "next statement of parent" frame back into queue
-
and iterate, which will cause it to be popped right back off at the top of the loop!
-
This current frame still has statements to be matched, so try to match them, pushing new subgoals if necessary
-
get the statement 't' for "this statement"
-
check to see if this statement can be matched as a builtin predicate
-
if it can and did! Add it as a matched statement to our ground state
-
push a new evidenc frame for the parent rule
-
advance the frame to the next statement in the parent rule
-
push the parent rule back on to queue to continue with it
-
and iterate, again causing this new frame to be popped right back off at the top of the loop!
-
this indicates that it was a builtin but failed to match, so we just continue on
-
check if we have any cases to match against. If not, just continue on.
-
We do have some cases to attempt to match this frame against!
var src = 0 //initialize our index counter //loop over each potential case and add subgoals as necessary for (var k = 0; k < cases[t.pred].length; k++) { //fetch the case 'rl' for "rule" var rl = cases[t.pred][k] //increment index into the cases for this predicate src++ //copy ground state for new frame var g = aCopy(c.ground) //if this rule is a fact then we add it to ground state if (rl.body.length == 0) g.push({src:rl, env:{}}) //Set up this rule as a potential new frame var r = {rule:rl, src:src, ind:0, parent:c, env:{}, ground:g} //check if this rule matches the current subgoal if (unify(t, c.env, rl.head, r.env, true)) { //it does! Check it for a euler path... var ep = c // euler path //Walk up the evidence tree and see if we find a frame already in the tree that is the same as this "potential next frame" //If we do find that this "next" frame was already seen this indicates that we are about to enter a proof state that we have already been in //This would create a non-productive loop, so if we do encounter such a case we simply fail out of the match and continue on while (ep = ep.parent) if (ep.src == c.src && unify(ep.rule.head, ep.env, c.rule.head, c.env, false)) break //Check if we iterated up to the root goal. If so, then we know this next frame is a new proof state that we have not encountered before //and that we should continue resolution trying to match this frame as a new subgoal! if (ep == null) { //Add our new frame to queue queue.unshift(r) if (typeof(trace) != 'undefined') document.writeln('EULER PATH UNSHIFT QUEUE\n' + JSON.stringify(r.rule) + '\n') } } //end specific subgoal } //end iteration of subgoals } //end main loop //if we reach here, then we have completed iteration over the entire query. Anything we matched is not moved over to evidence, with its proof trace. }
The unifier. Attempts to match two statements in corresponding environments. Updates one environment with information from the other if they do match.
Inputs:
s - source statement
senv - source environment
d - destination statement
denv - destination environment. Updated with variable bindings if s does unify with d.
Returns: true if unification happened, false otherwise
Outputs: updates denv
Environment evaluator. Determines the value of an expression within an environment. If the expression is a term we just return the term.
Inputs:
t - term to evaluate
env - environment of variable bindings
Returns: The term with variables replaced, if they were found in the environment. Null otherwise.
Outputs: none
If the predicate is a variable, look up the variable in environment.
if the variable has a value, re-evaluate with the predicate variable replaced, otherwise fail.
The predicate is not a variable and there are no parameters to it, so we are done, return the value
the predicate is not a variable but there are some parameter terms. Evalaute each.
else
loop over arguments
evaluate this argument if we were able to evaluate, so include the value of the argument
if we were not able to evaluate, so leave it as a variable predicate
return the term with variables all replaced