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 Aug
|10:30 - 11:15|
Petr LozovSain Petersburg State University, SPbGU, Ekaterina VerbitskaiaSaint Petersburg State University, Russia, Dmitri BoulytchevLink to publication
|11:15 - 12:00|
|Link to publication|