Logic Programming à la Carte
summary
A Haskell logic programming framework guanxi (關係) combines MiniKanren style relational search with SMT/SAT tactics and propagators to scale synthesis; a Scheme interpreter-as-relation proves program synthesis works (list concatenation recovered in ~9 seconds) but search is glacial without learning. Performance gains come from using incremental SMT ideas and a modified union‑find with group actions to collapse equivalences and cut propagator pressure, enabling mixed domains (SAT, ILP, refinements) to cooperate.
AI-written summary · about
chapters (17)
- 0:00Intro
- 1:10Bayesian Reasoning
- 3:08Safety is Tractable
- 3:40Good Hearts Law
- 8:10MiniCameron
- 9:25KenRen
- 12:30Barliman
- 15:35Gershom
- 23:15Logic T
- 24:55Incremental SMT solvers
- 26:40Using machine references
- 28:40Propagators
- 32:05Union Find
- 35:10Group Actions
- 36:30Reflection without remorse
- 38:25Natural domain SMT
- 39:40Abstract interpretation domains
related talks
20mKanren Light
22mCan Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk)
49mCompile-time Logic Programming in Scala: what for?
40mminiKanren Philosophy
32mGranite: Compositional Functional Logic Programming
16mMulti-stage Relational Programming
18mEpistemic Logic for Polyglots (Short Paper)
19mSome Novel miniKanren Synthesis Tasks