Relational Interpreters for Search Problems
We address the problem of constructing a solver for a certain search problem from its solution verifier. The main idea behind the approach we advocate is to consider a verifier as an interpreter which takes a data structure to search in as a program and a candidate solution as this program’s input. As a result the interpreter returns “true” if the candidate solution satisfies all constraints and “false” otherwise. Being implemented in a relational language, a verifier becomes capable of finding a solution as well. We apply two techniques to make this scenario realistic: relational conversion and supercompilation. Relational conversion makes it possible to convert a first-order functional program into relational form, while supercompilation (in the form of conjunctive partial deduction (CPD)) — to optimize out redundant computations. We demonstrate our approach on a number of examples using a prototype tool for OCanren — an implementation of miniKanren for OCaml, — and discuss the results of evaluation.
Thu 22 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
|Relational Interpreters for Search Problems|
Petr Lozov Sain Petersburg State University, SPbGU, Ekaterina Verbitskaia Saint Petersburg State University, Russia, Dmitri BoulytchevLink to publication
|Relational Processing for Fun and Diversity: Simulating a CPU relationally with miniKanren|
miniKanrenLink to publication