A Pruning Conditional Operator for miniKanren

Ben Baskin

25 September 2018 at 10:00AM WVH 166/168

Abstract

Because miniKanren programs can run forwards and backwards, interpreters written in miniKanren can perform program synthesis. Because program synthesis for dependently typed languages is also proof synthesis, miniKanren implementations of dependently typed languages can be used for proof search. Unfortunately, conde’s unaided complete interleaving depth-first search does not yield a practical proof search due to the sheer amount of computation required. A new conditional operator, called condp, gives users a means to drop irrelevant goals from search. We demonstrate that condp provides sufficient control over the search process to perform synthesis far more quickly, using the lightweight dependently typed language Pie as an example.

A relevant paper can be found here, which gives a great flavor for the kinds of things that miniKanren can be used for:

https://dl.acm.org/citation.cfm?id=3110252

A unified approach to solving seven programming problems (functional pearl), by William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might

And much more about miniKanren can be found at minikanren.org.