Improving Refutational Completeness of Relational Search via Divergence Test

Research output


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.
Original languageEnglish
Title of host publicationProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming
PublisherAssociation for Computing Machinery
Number of pages20
ISBN (Electronic)978-1-4503-6441-6
Publication statusPublished - 3 Sep 2018

Fingerprint Dive into the research topics of 'Improving Refutational Completeness of Relational Search via Divergence Test'. Together they form a unique fingerprint.

Cite this