A Complexity Study for Interleaving Search
summary
Formal complexity model for canonical miniKanren, decomposing full-search time into scheduling factor, unification (with separate occurs-check cost), and reification; constructs recursive cost equations from a symbolic scheme built by symbolic execution. Claims: occurs-check often dominates and can raise polynomial degree; recursive-call position drastically alters scheduling so backward execution can be faster; empirical timing on list/number examples matches predictions. Works for full-search and programs meeting two “simple unification” criteria, requires an oracle for subquery answers and is not yet automated.
AI-written summary · about
chapters (18)
- 0:00Intro
- 0:12Motivation
- 1:19A surprising example
- 2:25Cost model for interleaving search
- 4:18Plan of the talk
- 5:03Scheduling time: Basics
- 6:00Scheduling time: Formal definition
- 7:33Unification time: Focus
- 8:48Unification time: Basic operations
- 10:42Unification time: Estimations
- 12:41Symbolic technique: Symbolic variables
- 14:11Symbolic technique: Overview
- 15:18Symbolic technique: Symbolic schemes
- 16:34Symbolic technique: Extracted inequalities
- 17:23Symbolic technique: Current limitations
- 18:15Evaluation Results
- 18:53Evaluation: Observations
- 20:45Takeaways
related talks
14mOn Fair Relational Conjunction
16mMulti-stage Relational Programming
15mAn Empirical Study of Partial Deduction for miniKanren
29mTowards Bottom-Up Enumeration in miniKanren via Pruning and Memoization
22mA Case Study in Functional Conversion and Mode Inference in miniKanren
14mRelational Synthesis for Pattern Matching
20mKanren Light
17mλKanren: Higher-order Logic Programming with Shallow Embedding