Improving Refutational Completeness of Relational Search via Divergence Test

Research outputpeer-review

Abstract

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

Computer programming languages
Semantics
Specifications

Cite this

Булычев, Д. Ю., & Rozplokhas, D. (2018). Improving Refutational Completeness of Relational Search via Divergence Test. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming Association for Computing Machinery.
Булычев, Дмитрий Юрьевич ; Rozplokhas, Dmitri. / Improving Refutational Completeness of Relational Search via Divergence Test. Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. Association for Computing Machinery, 2018.
@inproceedings{0fd398463bd24951bb34da32a81af560,
title = "Improving Refutational Completeness of Relational Search via Divergence Test",
abstract = "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.",
author = "Булычев, {Дмитрий Юрьевич} and Dmitri Rozplokhas",
year = "2018",
month = "9",
day = "3",
language = "English",
booktitle = "Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming",
publisher = "Association for Computing Machinery",
address = "United States",

}

Булычев, ДЮ & Rozplokhas, D 2018, Improving Refutational Completeness of Relational Search via Divergence Test. in Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. Association for Computing Machinery.

Improving Refutational Completeness of Relational Search via Divergence Test. / Булычев, Дмитрий Юрьевич; Rozplokhas, Dmitri.

Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. Association for Computing Machinery, 2018.

Research outputpeer-review

TY - GEN

T1 - Improving Refutational Completeness of Relational Search via Divergence Test

AU - Булычев, Дмитрий Юрьевич

AU - Rozplokhas, Dmitri

PY - 2018/9/3

Y1 - 2018/9/3

N2 - 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.

AB - 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.

M3 - Conference contribution

BT - Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming

PB - Association for Computing Machinery

ER -

Булычев ДЮ, Rozplokhas D. Improving Refutational Completeness of Relational Search via Divergence Test. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. Association for Computing Machinery. 2018