Bottom-up-Enumeration in miniKanren: Pruning und Memoization beschleunigen die Synthese
Towards Bottom-Up Enumeration in miniKanren via Pruning and Memoization
Zwei kleine Bibliotheks-Kombinatoren für miniKanren ermöglichen Bottom-up-Enumeration mit Beobachtungs-Deduplizierung, ein Standardwerkzeug in nicht-relationalen PBE-Synthesizern. Der erste Kombinator, prune, dedupliziert einen Antwortstrom anhand eines benutzerdefinierten Schlüssels, typischerweise das Ein-/Ausgabeverhalten des Kandidaten. Der zweite, defrel/bank, memoisiert eine Relation mit kanonischen frischen Variablen, sodass ein einziger bereinigter Antwortstrom bottom-up aufgebaut und an jedem Aufrufort wiedergegeben wird. Eine gewichtete Variante, defrel/bank-w, fügt unreifen Strömen zulässige obere Schranken hinzu, um eine Bestensuche zu ermöglichen. In einer vorläufigen PBE-Benchmark übertrifft defrel/bank die tiefenbegrenzte Basislinie bei den meisten tiefen Zielen deutlich.
Wir präsentieren zwei kleine Bibliotheks-Kombinatoren auf Basis von einfachem miniKanren, die darauf ausgelegt sind, Bottom-up-Enumeration mit Beobachtungs-Deduplizierung, das Standardwerkzeug in nicht-relationalen Programm-durch-Beispiel-Synthesizern, in den relationalen Kontext zu bringen.