💻 computer science

Towards Bottom-Up Enumeration in miniKanren via Pruning and Memoization

Questo articolo introduce due combinatori della libreria miniKanren, `prune` e `defrel/bank`, che consentono l'enumerazione bottom-up con deduplicazione osservativa e memoizzazione per migliorare significativamente le prestazioni della sintesi di programmi relazionali su target profondi, proponendo anche una variante pesata per affrontare i casi in cui l'ordinamento canonico depth-first fallisce nel trovare rappresentanti compatti.

Autori originali: Nikolai Kudasov

Pubblicato 2026-07-29

📖 7 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Nikolai Kudasov

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di essere un detective che cerca di risolvere un mistero, ma invece di cercare indizi, stai cercando di costruire una macchina capace di svolgere un compito specifico, come trasformare il numero 2 in 4, il 3 in 9 e il 4 in 16. Non conosci la formula esatta che la macchina utilizza; conosci solo i risultati. Questo è chiamato "Programmazione per Esempio". Per trovare la risposta, potresti provare a costruire ogni possibile macchina, una alla volta, partendo dagli ingranaggi e dalle leve più semplici, e testando ognuna per vedere se funziona. È un po' come uno chef che cerca di trovare una ricetta segreta cucinando ogni possibile combinazione di farina, zucchero e uova finché una non risulta giusta.

Nel mondo dell'informatica, esiste un modo speciale di pensare chiamato "programmazione relazionale". Invece di dire al computer esattamente come trovare la risposta passo dopo passo, descrivi cosa deve essere la risposta, e lasci che sia il computer a trovare la strada. È come dire a un robot: "Trovami un percorso attraverso il labirinto", piuttosto che "Gira a sinistra, poi fai tre passi, poi gira a destra". Il computer è bravo a esplorare molti percorsi contemporaneamente, ma ha un'abitudine complicata: tende a esplorare gli stessi vicoli ciechi ripetutamente, o a rimanere bloccato in un tunnel lungo e tortuoso mentre perde di vista una scorciatoia breve e intelligente proprio accanto a sé. Questo articolo affronta questo problema, insegnando al computer come essere un esploratore più intelligente e organizzato.

Il Problee: Perdersi nel Labirinto

Immagina di dover trovare una chiave specifica in una soffitta gigante e disordinata piena di milioni di chiavi. La maggior parte di queste chiavi appare diversa, ma tutte aprono esattamente la stessa porta. Se sei un esploratore maldestro, potresti prendere una chiave, provarla, accorgerti che funziona, e poi passare ore a prendere altre chiavi che sembrano diverse ma che funzionano ugualmente bene, solo per esserne sicuro. Stai sprecando tempo controllando chiavi che fanno esattamente lo stesso lavoro.

Nel mondo dei programmi informatici, questo accade continuamente. Quando un computer cerca di costruire un programma per trasformare degli input in output, genera migliaia di diversi frammenti di codice. Molti di questi frammenti sono "gemelli" travestiti: fanno esattamente la stessa cosa anche se sembrano diversi all'interno. Un metodo di ricerca standard, che lavora come un esploratore che si immerge in profondità, ne controlla uno, poi il successivo, poi il successivo, diventando sempre più lento man mano che la soffitta si ingrandisce. È come cercare un ago in un pagliaio, ma il pagliaio è fatto di milioni di aghi che sembrano tutti leggermente diversi.

La Soluzione: Lo strumento "Prune" e la "Bank"

Gli autori di questo articolo, Nikolai Kudasov, hanno ideato due strumenti ingegnosi per risolvere questo caos. Pensali come un filtro magico e una biblioteca intelligente.

1. Lo strumento "Prune" (Il Filtro)
Immagina di avere un nastro trasportatore di chiavi che esce da una macchina. Lo strumento "Prune" è una guardia in piedi accanto al nastro. Mentre ogni chiave arriva, la guardia controlla quale porta apre. Se la guardia ha già visto una chiave che apre quella stessa porta, semplicemente getta la nuova chiave nel cestino senza nemmeno testarla. Tiene solo la primissima chiave che apre una determinata porta. In questo modo, il nastro trasportatore trasporta solo chiavi uniche e utili. Il computer smette di sprecare tempo su duplicati.

2. Lo strumento "Bank" (La Biblioteca Intelligente)
Ora, immagina che invece di costruire chiavi da zero ogni volta che ne hai bisogno, tu abbia una biblioteca magica. Quando chiedi alla biblioteca una chiave, non ti dà solo una chiave; costruisce un intero scaffale di chiavi uniche una sola volta, partendo dal basso, e le salva. Se chiedi una chiave più tardi, la biblioteca ti consegna semplicemente quella che ha già costruito.

Nel linguaggio dell'articolo, questo è chiamato defrel/bank. Forza il computer a costruire la sua lista di programmi candidati in un modo specifico e organizzato (partendo dai più semplici) e ne salva i risultati. Se il computer ha bisogno di usare un piccolo pezzo di un programma in seguito, non lo ricostruisce; lo prende semplicemente dal "bank". Questo risparmia una quantità enorme di tempo perché il computer non deve mai fare lo stesso lavoro due volte.

Il Colpo di Scena: A volte "Veloce" non significa "Meglio"

Gli autori si sono anche resi conto che essere organizzati non è sempre sufficiente. A volte, la "Bank" costruisce i suoi scaffali in un ordine che è veloce per il computer ma lento per l'essere umano. Ad esempio, la Bank potrebbe costruire tutte le macchine della "moltiplicazione" prima, e solo molto più tardi costruire le macchine dell' "addizione". Se la risposta che stai cercando è una macchina dell' "addizione", il computer potrebbe dover controllare migliaia di macchine della moltiplicazione prima di trovare finalmente quella di cui hai bisogno.

Per risolvere questo, hanno creato un terzo strumento chiamato defrel/bank-w (la Bank "Pesata"). Questo strumento è come un bibliotecario che sa che certi tipi di chiavi hanno più probabilità di essere la risposta. Utilizza un "punteggio" speciale per decidere quali chiavi mostrarti per prime. Cerca di mostrarti le chiavi più semplici e compatte per prime, anche se sono sepolte in profondità nella biblioteca. Questo è ottimo se vuoi la soluzione più elegante, ma può essere più lento se la risposta è in realtà una macchina complessa e profonda.

Cosa hanno scoperto: Velocità vs Strategia

Gli autori hanno testato questi strumenti su un insieme di enigmi matematici e di stringhe (come trasformare "Hello" in "Hello, World!"). Ecco cosa hanno scoperto:

La "Bank" è un fulmine di velocità: Su 6 degli 8 problemi matematici difficili, lo strumento defrel/bank è stato da 9 a 99 volte più veloce del vecchio metodo di ricerca standard. Era così veloce che ha risolto in una frazione di secondo problemi che al vecchio metodo richiedevano minuti per essere completati.
Ma ha un punto cieco: La Bank è così organizzata che a volte manca la risposta se questa è nascosta in una parte della biblioteca che viene visitata tardi. Ad esempio, se la risposta coinvolge l'aggiunta di numeri in un modo specifico (come $(1+x)^5$ ), la Bank potrebbe bloccarsi a controllare migliaia di esempi di moltiplicazione prima. In questi casi, il vecchio metodo, più lento, vince effettivamente perché controlla le cose in un ordine diverso.
La "Bank Pesata" è un compromesso: Lo strumento defrel/bank-w è eccellente nel trovare le risposte più compatte ed eleganti. Ha trovato la risposta corretta per un complicato enigma di stringhe in 10,4 millisecondi, battendo il metodo standard che impiegava 31,5 millisecondi. Tuttavia, per problemi matematici molto profondi, a volte si è bloccato nel tentativo di controllare troppe possibilità e ha terminato il tempo a disposizione (timeout).

Conclusione

Questo articolo non sostiene di aver risolto ogni problema dell'informatica. Invece, dimostra che aggiungendo un po' di "pruning" (filtraggio dei duplicati) e di "banking" (salvataggio del lavoro per il futuro), possiamo rendere i programmi informatici che costruiscono altri programmi molto, molto più veloci.

Gli autori suggeriscono che, se state costruendo un sistema per risolvere enigmi, dovreste usare lo strumento Bank come predefinito perché è solitamente il più veloce. Tuttavia, se state cercando una soluzione molto specifica e compatta, o se il problema è superficiale e semplice, potreste voler usare la Bank Pesata o anche il vecchio metodo. Non si tratta di avere uno strumento perfetto; si tratta di avere lo strumento giusto per la forma dell'enigma che si sta cercando di risolvere. L'articolo si conclude suggerendo che i lavori futuri testeranno questi strumenti su enigmi ancora più complessi, come la costruzione di programmi che comprendono liste o dati tipizzati, per vedere se questo aumento di velocità regge nel mondo reale.

Sintesi Tecnica: Verso l'Enumerazione Bottom-Up in miniKanren tramite Pruning e Memoizzazione

Problema

I moderni sintetizzatori di Programma-per-Esempio (PBE) si affidano tipicamente all'enumerazione bottom-up con deduplicazione osservazionale. Questo approccio mantiene una lista di lavoro di espressioni candidate, deduplica le stesse in base al loro comportamento su esempi di input e le espande livello per livello fino a quando non viene trovata una corrispondenza. Sebbene altamente efficace in contesti imperativi e funzionali, questa strategia si colloca in modo scomodo nella programmazione relazionale (specificamente in miniKanren), dove la disciplina di ricerca naturale è la risoluzione top-down contro un flusso equo di candidati.

Le esistenti ricette miniKanren per la PBE, come scrivere un interprete relazionale ed eseguirlo "all'indietro" o utilizzare un approccio "enumera-e-testa" con limiti di profondità, soffrono di inefficienze significative a profondità di ricerca realistiche. Il problema primario è che l'albero di ricerca contiene molte espressioni comportamentalmente equivalenti. Un enumeratore ingenuo limitato dalla profondità crea una nuova tabella di deduplicazione ad ogni livello ricorsivo, fallendo nel riutilizzare il lavoro svolto ai livelli precedenti. Ciò porta a un'esplosione esponenziale dello spazio di ricerca in cui candidati comportamentalmente identici vengono rivalutati ripetutamente.

Metodologia

Gli autori propongono due piccoli combinatori di libreria costruiti sopra un nucleo $\mu$ Kanren non modificato per colmare il divario tra l'enumerazione bottom-up della PBE e la programmazione relazionale. Questi combinatori introducono l'enumerazione bottom-up e la deduplicazione osservazionale senza alterare la disciplina di ricerca ospite.

1. Il combinatore `prune`

Il primo combinatore, prune, filtra uno stream di risposte basandosi su una funzione di chiave fornita dall'utente.

Meccanismo: Avvolge un obiettivo (goal) ed emette al massimo un elemento per ogni valore distinto della funzione chiave (ad esempio, il comportamento input/output di un'espressione candidata).
Gestione delle Variabili Logiche: Per gestire i casi in cui la chiave dipende da variabili logiche non vincolate, prune utilizza un valore sentinella (skip-prune). Se una chiave non può essere computata perché un termine non è ancora ground, lo stato viene emesso senza essere registrato nella tabella di deduplicazione. È soggetto a deduplicazione solo una volta che la variabile viene vincolata e il termine diventa ground.
Ambito: La deduplicazione è strettamente per-chiamata. Una nuova tabella hash viene creata per ogni invocazione di prune per evitare di confondere un "visto come variabile esterna" con un "visto come variabile interna", il che romperebbe la completezza nelle definizioni ricorsive.

2. Il combinatore `defrel/bank`

Il secondo combinatore, defrel/bank, estende prune per ottenere una vera enumerazione bottom-up con deduplicazione condivisa tra tutte le chiamate al sito di una relazione.

Variabili Canoniche: Memoizza una relazione rispetto a variabili fresche canoniche (le prime $N$ variabili fresche di uno stato vuoto), che rappresentano la chiamata più generale della relazione.
La "Banca" (Bank): Il corpo della relazione viene eseguito una sola volta contro queste variabili canoniche per produrre uno stream canonico (la "banca"). Questo stream è costruito bottom-up e contiene esattamente un rappresentante per classe di equivalenza (determinata dalla chiave #:prune).
Riproduzione (Replay): Le chiamate successive alla relazione non rieseguono il corpo. Invece, riproducono lo stream canonico contro gli argomenti specifici del chiamante. Ciò comporta il percorso della sostituzione canonica, la rinomina delle variabili interne nello namespace del chiamante e l'unificazione dei risultati con gli argomenti del chiamante.
Efficienza: Questo approccio garantisce che il lavoro di deduplicazione venga eseguito una sola volta per ogni query (run ...), indipendentemente da quante volte la relazione viene chiamata ricorsivamente.

3. La variante `defrel/bank-w` (Best-First)

Il defrel/bank standard utilizza la ricorsione depth-first, il che influenza l'ordine di enumerazione (ad esempio, favorendo catene di moltiplicazione a destra rispetto all'addizione). Per affrontare i casi in cui la soluzione target si trova in profondità nell'ordine canonico, gli autori introducono defrel/bank-w.

Stream Pesati: Questa variante attacca limiti superiori ammissibili (pesi) alle celle immature dello stream.
Decadimento della Profondità (Depth-Decay): Un fattore di decadimento viene applicato ai pesi nei siti di chiamata ricorsiva. Ciò assicura che i rappresentanti più superficiali abbiano pesi inferiori ed siano emessi per primi dalla logica di fusione ordinata (mplus-w).
Euristiche Lazy: Il sistema utilizza una disciplina di "limite lazy" (lazy-ceiling) dove i pesi vengono sbirciati senza forzare il thunk sottostante, impedendo loop infiniti durante la costruzione dello stream canonico. Questo implementa una ricerca di tipo A* dove il limite del peso funge da euristica ammissibile.

Contributi Chiave

prune: Un combinatore generico di deduplicazione dello stream di risposte basato su funzioni chiave fornite dall'utente, supportato da helper (ground-key, when-ground) per elevare le funzioni a livello di termine in chiavi di pruning.
defrel/memo e defrel/bank: Combinatori per la memoizzazione della relazione rispetto alle variabili fresche canoniche. defrel/bank fornisce specificamente l'enumerazione bottom-up con deduplicazione condivisa, traspiantando efficacementamente il pattern standard del "worklist" della PBE nel contesto relazionale.
defrel/bank-w: Una variante best-first con decadimento della profondità che utilizza pesi sugli stream immaturi per recuperare l'enumerazione best-first, permettendo al sistema di trovare rappresentanti compatti anche quando l'ordine depth-first naturale li manca.
Trucchi di Implementazione: Il paper dettaglia ottimizzazioni ingegneristiche, come l'uso di pairing heaps per le fusioni ordinate e tecniche di "thunk-collapse", per garantire che l'approccio memoizzato sia competitivo con i baseline limitati dalla profondità.

Risultati

Gli autori presentano una valutazione empirica preliminare su benchmark PBE aritmetici e di stringhe (profondità 0–6).

Guadagni di Prestazioni: Su 6 dei 8 target aritmetici profondi, defrel/bank è da 9 a 99 volte più veloce del baseline limitato dalla profondità (bounded). Questo perché bank evita di ri-pruningare le sotto-espressioni ad ogni livello ricorsivo.
Bias dell'Ordine di Enumerazione: Le prestazioni di defrel/bank dipendono fortemente dall'ordine di enumerazione. Eccelle quando la soluzione target si trova precocemente nell'ordine depth-first canonico (ad esempio, $x^k$ o $x^k + c$ ). Tuttavia, fatica o va in timeout su target come $(1+x)^k$ , che appaiono molto tardi nello stream canonico (ad esempio, posizione 243.158 per profondità 4).
Compromessi Best-First: defrel/bank-w trova con successo rappresentanti compatti per target come $(1+x)^k$ precocemente nella ricerca. Tuttavia, incorre in un "costo breadth-first": l'emissione di una cella di profondità $K$ richiede l'emissione di tutte le celle di profondità $<K$ . Su spazi comportamentali ampi (migliaia di comportamenti distinti a profondità 3), ciò porta a timeout su target aritmetici profondi dove defrel/bank ha successo.
Confronto con il Baseline dell'Host: Un baseline non relazionale del linguaggio ospite (host-bank) performa bene su target superficiali e famiglie $(1+x)^k$ , ma fallisce catastroficamente su target a destra-spine profondi a causa del costo di costruire una banca esaustiva al di fuori del motore relazionale. defrel/bank mantiene l'interfaccia relazionale pur recuperando gran parte del miglioramento di velocità del host-bank laddove il bias di enumerazione è favorevole.

Significato e Rivendicazioni

Il paper sostiene che questi combinatori riescono a portare lo strumento standard dell'enumerazione bottom-up con deduplicazione osservazionale nel contesto relazionale senza lasciare il paradigma relazionale o cambiare la disciplina di ricerca dell'host.

Semantica Opt-in: L'approccio è strettamente opt-in. Non altera la semantica delle relazioni standard di miniKanren; la deduplicazione si applica solo alle relazioni esplicitamente avvolte in prune o definite tramite defrel/bank.
Completezza: Gli autori sostengono che il pruning preserva la completezza rispetto all'equivalenza fornita dall'utente. Per ogni comportamento, viene trovato almeno un rappresentante.
Limitazioni: Sono modesti riguardo all'ambito, notando che la valutazione è preliminare, limitata a due domini (aritmetica e stringhe) e si basa su una specifica grammatica. Riconoscono che defrel/bank non è una soluzione universale; il suo successo dipende dall'interazione tra la forma del target e l'ordine di enumerazione. Affermano esplicitamente che la congiunzione equa non può risolvere il bias di enumerazione di defrel/bank perché il bias risiede in quali celle esistono nella banca, non in come esse siano intercalate.
Lavoro Futuro: Il paper identifica diverse direzioni per il lavoro futuro, tra cui l'approfondimento iterativo (iterative deepening) sul corpo canonico per correggere il bias di $(1+x)^k$ senza costi breadth-first, la rilevazione della saturazione e l'estensione dell'approccio a store di vincoli più ricchi e altri domini PBE (ad esempio, bit-vector, liste).

In sintesi, il paper dimostra che, memoizzando le relazioni rispetto alle variabili canoniche e applicando il pruning tramite equivalenza osservazionale, si possono ottenere significativi guadagni di prestazione nella sintesi PBE relazionale, a patto che l'ordine di enumerazione si allinei con la struttura del target.