Search papers, labs, and topics across Lattice.
This paper introduces two combinators for miniKanren that enable bottom-up enumeration with observational deduplication, enhancing its utility in program-by-example (PBE) synthesis. The first combinator, prune, effectively deduplicates answer streams based on user-defined keys, while the second, defrel/bank, memoizes relations to optimize the enumeration process. Experimental results indicate that defrel/bank significantly outperforms traditional depth-bounded methods in most deep synthesis tasks, although it struggles with certain cases where depth-first enumeration is more efficient.
Bottom-up enumeration in miniKanren can now achieve superior performance in program synthesis by leveraging pruning and memoization techniques.
We present two small library combinators on top of plain miniKanren, designed to bring bottom-up enumeration with observational deduplication, the standard tool in non-relational program-by-example (PBE) synthesizers, into the relational setting. The first combinator, prune, deduplicates an answer stream by a user-supplied key, typically the input/output behavior of the candidate. The second, defrel/bank, memoizes a relation against canonical fresh variables so that a single pruned answer stream is built bottom-up and replayed at every call site. We also discuss a weighted variant, defrel/bank-w, which attaches admissible upper bounds to immature streams to recover best-first enumeration in cases where the natural depth-first canonical order misses compact representatives. On a preliminary PBE benchmark of arithmetic and string synthesis targets, defrel/bank substantially outperforms the depth-bounded baseline on most deep targets, while losing on a small family where the canonical depth-first enumeration order misses compact representatives. We leave a broader empirical evaluation to an extended version of this paper.
