Thanks, Raph.
Is it fair to say that the behavior you describe is specific to SearchAll and that one could write some other meta-function that behaves differently? Or is this understood to be built into the Oz semantics at some deeper level?
For example one could write a variant of SearchAll in which unification with external variables proceeded as any other unification but in which all such unifications are noted. At the end, the list of results would include for each result a list of the external variable bindings that it requires. Any result whose conditions included one or more that had since become impossible would be dropped from the list.
The preceding paragraph sounds very similar to what you describe except that it terminates and returns conditional results rather than waiting to see if the conditions are satisfied.
-- Russ
On 10/9/05, Raphael Collet <[EMAIL PROTECTED]> wrote:
Russ Abbott wrote:
> Thanks to everyone who clarified the issue of references to external
> variables. If an attempt to unify a value with an external variable
> suspends, it's not clear to me why the following program produces an
> output before suspending.
>
> local X in
> {Browse {SearchAll fun {$} X = x {Browse X} X end}}
> end
>
> I get an x in the browser--but no output from SearchAll.
Here comes an official explanation ;-)
Actually the unification inside the space does not block. It is given a
chance, but the binding of X is marked as "speculative". A speculative
binding has the property that the space might fail if the variable is
bound by its owner. In the example,
- if X is bound to 'x', the space succeeds;
- if X is bount to another value than 'x', the space fails.
In order to avoid a race condition, we say that the space is "unstable".
That is, an external binding may change its status. The operation
Space.ask (which is used by SearchAll) blocks until the space becomes
stable. Without stability, SearchAll would produce inconsistent output
results.
In the first example below, the search terminates because the constraint
Root=X is satisfied, whatever the value of X.
local X in
{Browse {SearchAll proc {$ Root} Root=X end}}
end
In the next example, the search completes too, showing no solution. The
speculative binding allows to detect failures earlier.
local X in
{Browse {SearchAll proc {$ Root} Root=X Root=1 X=2 end}}
end
Cheers,
raph
_________________________________________________________________________________
mozart-users mailing list [email protected]
http://www.mozart-oz.org/mailman/listinfo/mozart-users
--
_____________________________________________
Professor, Computer Science
California State University, Los Angeles
o Check out my blog at http://russabbott.blogspot.com/
_________________________________________________________________________________ mozart-users mailing list [email protected] http://www.mozart-oz.org/mailman/listinfo/mozart-users
