Wildcard Logic Variables
summary
Claims a new variable kind that serves as a limited universal quantifier, implemented in OCanren to extend miniKanren style relations and OCaml-to-relational conversion. Wildcards unify with anything without extending substitution and combine with disequality constraints to express statements like “not a quote” and that Peano numbers are below a constructor. Applied to pattern-matching synthesis, it reduces spurious answers for overlapping branches but does not yet prevent exponential example blowup; a working implementation and experiments exist.
AI-written summary · about
chapters (12)
- 0:00Wildcard logic variables intro
- 1:06Quote expressions in Scheme
- 2:34Universal quantifiers in typed languages
- 4:25Piano numbers constraint
- 6:12Wildcard logic variables
- 8:24Unification with wildcards
- 9:50Eigen variables related work
- 11:41miniCovenant language
- 13:33Pattern matching synthesis challenges
- 16:27Wildcards in pattern matching
- 19:00Pattern matching issues
- 20:46Main results and future work
related talks
44mUnconditional Code
18mType-Based Incorrectness Reasoning
42mQuantum program analysis: Verification and Testing
41mRelational Interpreters, Program Synthesis, and Barliman
34mWeak Versions of Extended Resolution
23mLogarithm and Program Testing
51mWhen Types are Not Enough
47mQuickSpec: A Lightweight Theory Exploration Tool (...)