On Fair Relational Conjunction
summary
Presents a new symmetric conjunction evaluator for miniKanren that switches conjuncts based on a structural recursion predicate (postpone a conjunct until its structurally recursive arguments become free). Implements both a naive interleaving with an unfolding bound n (example: n=11 fixes a sort that otherwise didn't complete in five minutes) and the dynamic predicate-based switch. Evaluated on five benchmarks (list reverse, sort, Tower of Hanoi, bridge and torch, water pouring). Shows same convergence as naive fair interleaving and much better performance than left-biased conjunction on pessimistic orders.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 2:52Disjunction
- 3:06Unfolding Bound
- 4:29Summary
- 5:07Dynamically determinate
- 5:39Structural Recursion
- 8:24Switch Conjunction
- 9:30Conclusions
- 10:09Evaluation
- 10:52Complex benchmarks
- 13:04Conclusion
related talks
22mA Case Study in Functional Conversion and Mode Inference in miniKanren
16mMulti-stage Relational Programming
24mAll for one and none forall: Compiling polymorphic relations without(…)
26mCommitting to the bit: Relational programming with semiring arrays and SAT solving
01h 05mControl Flow Obfuscation for Featherweight Java + Efficient Fair Conjunction
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
40mminiKanren Philosophy
47mLogic Programming à la Carte