| For anyone who finds this topic interesting, you might be interested in the following resources: http://minikanren.org/ The second edition of `The Reasoned Schemer` (MIT Press, 2018): https://mitpress.mit.edu/books/reasoned-schemer-second-editi... The Clojure/conj 2016 talk Greg Rosenblatt and I gave on Barliman: https://www.youtube.com/watch?v=er_lLvkklsk `A Unified Approach to Solving Seven Programming Problems (Functional Pearl)`, William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, Matthew Might (ICFP 2017) (Open Access): https://dl.acm.org/doi/10.1145/3110252 and the related talk: https://www.youtube.com/watch?v=o3AHnyEf7IE and Nada Amin's interactive version of the paper: http://io.livecode.ch/learn/namin/icfp2017-artifact-auas7pp Cheers, --Will |
>> 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?