Relational Synthesis for Pattern Matching
summary
The work encodes pattern-match synthesis in miniKanren using two relational interpreters and replaces the resulting universal quantifier by enumerating inhabitants up to depth h+1 with a per-type default, producing a finite example set. It adds a branch-and-bound pruning via a new structural constraint primitive to cut searches and uses a size metric: switches count (return = 0, switch = branch count). Small benchmarks synthesize optimal code in seconds (three-Boolean example reaches optimal size 4 after ~2.5s); large cases can need up to 11,000 examples and show scalability limits.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:42Pattern Matching Syntax
- 3:39Synthesis Algorithm
- 4:38Eliminating
- 5:17Example 1: Three Examples is a Complete Set
- 6:15Example 2: Not a Complete Set of Examples
- 6:52Current Algorithm for Examples Generation
- 7:32Improvement: Reducing Examples Set
- 8:20Branch and Bound Optimization
- 8:55Structural constraint
- 10:01Minimization Criterion for Synthesized Program
- 10:42Evaluation: matching three boolean values
- 11:13Performance problem (2/2)
- 12:23Conclusions and Future Work Contributions
related talks
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
16mMulti-stage Relational Programming
22mA Case Study in Functional Conversion and Mode Inference in miniKanren
24mAll for one and none forall: Compiling polymorphic relations without(…)
25mRecursive Program Synthesis using Paramorphisms
47mLogic Programming à la Carte
26mCommitting to the bit: Relational programming with semiring arrays and SAT solving
18mMobius: Synthesizing Relational Queries with Recursive and Invented Predicates