Universal Quantification and Implication in miniKanren
summary
Adds two new miniKanren goal constructors: universal goal (variables, body, domain) and implication goal (antecedent, consequent), with an algorithm that does candidate extraction then builds a relative complement goal and recurses; combines semantic solving for primitive constraints and syntactic pattern-matching/unfolding for user-defined relations. Prototype proves many examples (graph reachability, game-winning, relational interpreter) but program synthesis and sorting scale poorly (lists length >3 often time out). Paper gives a pen-and-paper correctness proof; implementation needs major optimization.
AI-written summary · about
chapters (8)
- 0:00Start
- 1:16Synthesize a Sorting Function
- 3:58Relative Cognition
- 9:10Ways To Solve the Implication
- 13:07Graph Reachability and Game Winning
- 15:50Sorting
- 18:18Constructivity
- 20:26Future Work
related talks
20mKanren Light
40mminiKanren Philosophy
15mAn Empirical Study of Partial Deduction for miniKanren
22mA Case Study in Functional Conversion and Mode Inference in miniKanren
14mRelational Synthesis for Pattern Matching
17mλKanren: Higher-order Logic Programming with Shallow Embedding
24mAll for one and none forall: Compiling polymorphic relations without(…)
14mMicroKanren in J