|
|
|
|
|
by YeGoblynQueenne
1836 days ago
|
|
Hi, Will. I noticed this: >> Your program can be more efficient, you can have more expressive control but
if you are not careful, your program can be unsound. In other words: there may
be an answer to your query that you do not find. So an analogy would be in a
database lookup. If you are doing a database query, maybe there is actually
information in a table that you should find, but you do not find it. To clarify, that's incompleteness. Unsoundness is when an inference rule returns
wrong results. Incompleteness is where it doesn't return all correct results. As
you say, unification without an occurs check is unsound and Prolog's depth-first
search is incomplete. I wanted to ask, because you brought it up in the interview, how does minikanren
(or minikanrens?) handle the occurs check? You said that you are interested in
trying to push the relational aspect as far as possible, recognising that this
gives up efficiency - can you quantify to what extent minikanren gives up
efficiency and generally say a bit more about the trade-off between (if I
understand it correctly) efficiency and relational (declarative?) purity? |
|
I always read your logicy comments and posts--thank you!
> To clarify, that's incompleteness. Unsoundness is when an inference rule returns wrong results. Incompleteness is where it doesn't return all correct results. As you say, unification without an occurs check is unsound and Prolog's depth-first search is incomplete.
Thank you. Yes, I misspoke.
For anyone interested, this video gives a nice overview of soundness and completeness, in the context of logic: https://www.youtube.com/watch?v=HeQX2HjkcNo
> I wanted to ask, because you brought it up in the interview, how does minikanren (or minikanrens?) handle the occurs check? You said that you are interested in trying to push the relational aspect as far as possible, recognising that this gives up efficiency - can you quantify to what extent minikanren gives up efficiency and generally say a bit more about the trade-off between (if I understand it correctly) efficiency and relational (declarative?) purity?
miniKanren performs unification with the occurs check. This is one of the tradeoffs miniKanren makes: sound unification, but it can be expensive. The interleaving complete search is another tradeoff: the search uses more time and memory than does depth-first-search, in those cases in which DFS would be sufficient. Another tradeoff is that miniKanren avoids the use of non-logical / extra-logical operators. There are no cuts, projected variables, var tests, etc., in the pure parts of the language (which is the version I always use). If you want to perform arithmetic, you either have to encode arithmetic as a pure relation (as Oleg Kiselyov has done), or add a fully-relational constraint system for arithmetic to miniKanren (as we did in cKanren). Or, you can add a delayed goals mechanism, although this can lose completeness.
There are lots of variants of miniKanren at the this point: alphaKanren (nominal logic programming); cKanren (constraints); probKanren (prototype probabilistic Kanren); dbKanren (Greg Rosenblatt's extension to handle graph database operations, used in mediKanren 2); etc. I hope we can integrate all of the features into a single implementation some day.
Cheers,
--Will