> > 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. >
I'm not familiar with this Haskell library, but our implementations use an immutable data structure for the store. Barliman's implementation uses an array-mapped-trie (no hashing necessary, variables are created with unique indices). You're right that this makes disjunction pretty easy. > 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. > These projects sound pretty interesting. I'm interested in hearing about them in more detail, if you're willing to share. A lot of it sounds on-topic for this group. -- 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.
