We describe a search optimization technique for implementation of relational programming language miniKanren which makes more queries converge. Specifically, we address the problem of conjunction non-commutativity. Our technique is based on a certain divergence criterion that we use to trigger a dynamic reordering of conjuncts. We present a formal semantics of a miniKanren-like language and prove that our optimization does not compromise already converging programs, thus, being a proper improvement. We also present the prototype implementation of the improved search and demonstrate its application for a number of realistic specifications.
|Title of host publication||Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming|
|Publisher||Association for Computing Machinery|
|Number of pages||20|
|Publication status||Published - 3 Sep 2018|