>
> You've made some good observations. I haven't thought of this in terms of
> threshold reads before, but what you're describing sounds like the
> implementation of deferred goals in some MK variants.
>
> Deferred goals are resumed when the variables they depend on become known,
> which should be able to support dynamic interleaving, as in your
> interpreter/type-inferencer example.
>
Yep, that sounds like a threshold read. What does "known" mean? Fully
ground, or just non-fresh?
In the former case, the tripwire set would be {{x} | x is any value}; in
the latter case, ignoring constraints for the moment, I think it would be
something like [{x} for all non-compound values x] ++ [{ x | x equals (cons
<anything> <anything>) }], where 'cons' is the only compound-value
constructor.
I suspect it's easy to prove that you can also defer until symbolo/numbero
constraints are applied, if you're happy with a more coarse-grained read;
then the tripwire is [{x | x is a symbol}, {x | x is a number}, {x | x is a
cons}] ++ [{x} for all non-number, non-symbol, non-compound values x].
I guess one immediate conclusion is: if "known" means threshold-reading a
valid tripwire set, Lindsey Kuper has proven that you're free to schedule
goals in any way you like without changing the results of the user's
program. [Completeness of the search still requires attention.]
It's not working well enough to be useful yet.
>
Interesting; what are its shortcomings?
--
You received this message because you are subscribed to the Google Groups
"minikanren" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/minikanren.
For more options, visit https://groups.google.com/d/optout.
