通过剪枝和记忆化实现miniKanren中的自底向上枚举
Towards Bottom-Up Enumeration in miniKanren via Pruning and Memoization
AI总结:
该研究在miniKanren基础上提出两个库组合子,prune用于答案流去重,defrel/bank可记忆化关系实现自底向上枚举,还有加权变体defrel/bank-w。在初步PBE基准测试中,defrel/bank多数情况下表现良好,部分情况欠佳,更广泛评估待扩展版本。
AI中文摘要:
我们在普通miniKanren之上提出了两个小型库组合子,旨在将带有观察去重的自底向上枚举(非关系型示例编程(PBE)合成器中的标准工具)引入关系设置。第一个组合子prune通过用户提供的键(通常是候选者的输入/输出行为)对答案流进行去重。第二个defrel/bank针对规范的新鲜变量记忆化一个关系,以便自底向上构建单个剪枝后的答案流并在每个调用点重放。我们还讨论了加权变体defrel/bank-w,它为未成熟流附加可接受的上限,以便在自然深度优先规范顺序错过紧凑代表的情况下恢复最佳优先枚举。在算术和字符串合成目标的初步PBE基准测试中,defrel/bank在大多数深度目标上显著优于深度受限基线,但在规范深度优先枚举顺序错过紧凑代表的小家族中表现不佳。我们将更广泛的实证评估留到本文的扩展版本中。
英文摘要:
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.