An Empirical Study of Partial Deduction for miniKanren
summary
Presents an implemented specializer that combines partial deduction and supercompilation into a conservative partial deduction for miniKanren, plus a last-branching heuristic that picks the relation call that most narrows the search. Evaluated against classic CPD and a conjunctive PD on four benchmarks (two eval implementations, a unifier, and a path search finding five paths of length 7 in a 20-vertex, 30-edge graph). Empirical claim: conservative PD produces faster residuals on 3 of 4 cases, CPD times out (>30s) or makes code larger in some cases.
AI-written summary · about
chapters (19)
- 0:00Partial Deduction: a Method to Improve Logic Programs
- 1:38Partial Deduction for MINIKANREN: Bird's-eye View
- 2:23Driving Unfolding
- 4:15Conjunctive Partial Deduction: Left-to-right Unfolding
- 5:00CPD Split is Necessary
- 5:40Split: Which Way is the Right Way?
- 6:05Decisions in Partial Deduction
- 7:08Evaluator of Logic Formulas: Unfolding Step 2
- 8:52Unfolding of Boolean Connectives
- 9:07Unfolding Boolean Connectives First
- 9:30Evaluator of Logic Formulas Conservative PD
- 10:11Conservative Partial Deduction
- 11:37Less-branching Heuristics
- 12:31Evaluator of Logic Formulas Order of Calls
- 12:48Evaluator of Logic Formulas: Compexity of Relations
- 13:34Evaluator of Logic Formulas: Evaluation
- 14:22Path Search
- 14:33Evaluation Results
- 14:53Conclusion
related talks
22mA Case Study in Functional Conversion and Mode Inference in miniKanren
16mMulti-stage Relational Programming
29mTowards Bottom-Up Enumeration in miniKanren via Pruning and Memoization
40mminiKanren Philosophy
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
24mAll for one and none forall: Compiling polymorphic relations without(…)
01h 01mA partial history of partial evaluation
26mCommitting to the bit: Relational programming with semiring arrays and SAT solving