Input match substitu-tion and the guard condition

Metamorphosis 93

tions in this way (directed relations), makes the semantics closer to functional lan-guages.

While there is no search beyond the guard, there is still search within the guard as the following GDC program to find a key at the node of a binary tree illustrates:

//onTree(Key, Tree, Found)
onTree(Key,tree(Left,Key1,_),Found)
:- Key=/=Key1, onTree(Key,Left,Found) | true.

of arbitrarily nested guards. As will be explained, nested guard conditions can cause premature binding.

With the logical infix implication symbol, ←, assumed to be left associative, the guarded clause

h←c1, c2,… ←b1, b2,…,bm. (C)
in the program aj=hθ1(for some substitution θ1). If θ1 is an input match substitu-tion and if the guard condition (←c1, c2, …)θ is satisfiable with some substitution of variables θ which is an extension of θ1 (i.e. θ=θ1θ2, juxtaposition denoting composition of substitutions) then the clause is a candidate for committal. If this clause is the one selected, the goal aj is replaced by the body b1, b2, … bm so that the resolvent of the initial goal and the input clause reduces to
← (a1, a2,… b1, b2,… bm,… an)θ

If any of the bindings entailed by θ are due to recursive guards of the resolving clause

There will be no problem if the bindings generated by the guard θ2 do not cause bindings of the variables in the call, the global variables.

aiθ=aiθ2=ai