A New Higher-order Unification Algorithm for λKanren
summary
A higher-order unifier for λKanren extends Miller’s pattern fragment with a new maybe-var-term rule and enforces a scope-aware representation using static closures paired with brown levels (de Bruijn-like indices) to prevent variable capture and shadowing bugs. It replaces binary binder merging with scope extension checks, accepts more alpha-/beta-equivalences correctly, avoids false positives from naive renaming, and runs on λKanren examples like alpha-equivalence and variable instantiation where the original algorithm fails.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:14What is miniKanren
- 0:56Higherorder Unification
- 1:48Term of Unification
- 2:55lambda current programs
- 4:06millers algorithm
- 5:57Scope restriction
- 7:21Variable capturing problem
- 8:49Brown levels
- 9:31Binary binder merging
- 10:31Name shadowing
- 11:47False positives
- 12:47Static Closure
- 13:14Extend
- 14:07Example
- 16:16Scopes
related talks
17mλKanren: Higher-order Logic Programming with Shallow Embedding
20mKanren Light
14mMicroKanren in J
24mAll for one and none forall: Compiling polymorphic relations without(…)
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
40mμKanren: Running the Little Things Backwards
14mRelational Synthesis for Pattern Matching
16mMulti-stage Relational Programming