Hi Will :-)
> I agree with you that there seem to be many similarities between LVars
> and miniKanren! I think you could build a miniKanren-like system on
> top of an LVars-like system, and also, as you point out, mix ideas
> between the two systems.
I see two potential benefits: either an *extremely* short MK implementation
(because MK is basically LVars plus conde minus threshold reads), or a
better and more capable MK.
The one thing that's not clear to me is how you do disjunction and multiple
results. Can you clone the store? IIRC the Haskell library implements the
key data structures backend by mutable data on the plain ol' heap, which
suggests "no".
The key concepts of LVars could be implemented by an
alist/path-copying-HAMT/etc. backing; in that case disjunction appears
easier.
> the concepts of lattices ... [static analysis] [...]
Oh yeah, I vaguely remember that class. Thanks for prodding at my memory.
> When I was looking for connections with Lindsey and Ryan, years ago ...
That's the repo I linked to?
> the LVars formalism was missing a feature or two that I wanted for
> implementing miniKanren-in-LVars.
>
Something to do with disjunction? Or something else?
> I agree with Greg that there is a connection between these ideas and
> delayed goals
Sure sounds like it to me :) One can rephrase "blocking threshold read" as "
*delay* until the value is above any one of {x, y, z}, then tell me which",
so... yeah.
> This is definitely worth thinking about more! Here is my challenge to
> you: using the latest version of LVish, implement miniKanren (or
> microKanren) using LVars! I'll bet you can do it now!
>
I appreciate the encouragement, but it'll have to come after my current toy
projects, which are (1) a miniKanren in TypeScript (working-but-messy, but
for one well-understood bug); (2) a miniKanren search tree visualizer,
perhaps growing out of no. 1; and (3) some kind of propositional calculus
workbench, with a theorem prover, axiom independence prover and soundness
checker, tautology enumerator just for shits and giggles, perhaps some
flavor of datalog to query streams of formulae; all it needs is a raison
d'être and plenty of time :D
I think it would be interesting to combine the top-down proof search
strategy of my current theorem prover with the bottom-up approach of
BFS-ish iterated condensed detachment. Anyways, that's veering off topic.
Cheers,
Jonas
--
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.
