miniKanren
summary
Live demo of miniKanren shows relations translated from functions (appen with an extra answer arg) and an interpreter that can run backward generation to synthesize code — example: search for programs that evaluate to 6 and try to recover factorial(5) = 120. A constraint layer adds finite-domain constraints plus disequality and all-different so cryptarithmetic (SEND+MORE=MONEY) and 8-queens run (returns 92 solutions, ~1.7s here). A scoping bug in env lookup is fixed by adding a disequality constraint; demos are interactive and working.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 2:08A Pen
- 8:37Will Bird Law
- 15:34Writing an interpreter
- 22:04Recursion
- 26:09CK
- 28:49Operators
- 40:45Logic
- 41:27Reply Info
- 42:02Let Program
- 44:34Theorem Prover
related talks
40mμKanren: Running the Little Things Backwards
43mAn Imperishable Wonderland of Infinite Fun
52mStrange Dreams of Stranger Loops
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
47mSemi-Automated Direction-Driven Functional Conversion
01h 01mLearning Propositional Logic with Logic Programming
33mAnalyzing Functional Programs
20mInteractive Haskell Type Inference Exploration (Extended Abstract)