Towards Bottom-Up Enumeration in miniKanren via Pruning and Memoization

# Towards Bottom-Up Enumeration in miniKanren via Pruning and Memoization
Source: [https://arxiv.org/html/2607.25373](https://arxiv.org/html/2607.25373)
\(2026\)

###### Abstract\.

We present two small library combinators on top of plainminiKanren, designed to bring bottom\-up enumeration with observational deduplication, the standard tool in non\-relational program\-by\-example \(PBE\) synthesizers, into the relational setting\. The first combinator,prune, deduplicates an answer stream by a user\-supplied key, typically the input/output behavior of the candidate\. The second,defrel/bank, memoizes a relation against canonical fresh variables so that a single pruned answer stream is built bottom\-up and replayed at every call site\. We also discuss a weighted variant,defrel/bank\-w, which attaches admissible upper bounds to immature streams to recover best\-first enumeration in cases where the natural depth\-first canonical order misses compact representatives\. On a preliminary PBE benchmark of arithmetic and string synthesis targets,defrel/banksubstantially outperforms the depth\-bounded baseline on most deep targets, while losing on a small family where the canonical depth\-first enumeration order misses compact representatives\. We leave a broader empirical evaluation to an extended version of this paper\.

miniKanren, relational programming, program synthesis, programming by example, bottom\-up enumeration, observational equivalence

††copyright:none††journalyear:2026††ccs:Software and its engineering Constraint and logic languages††ccs:Software and its engineering Automatic programming## 1\.Introduction

Bottom\-up enumeration with observational deduplication is the standard approach in modern program\-by\-example \(PBE\) synthesizers\(Albarghouthi et al\.,[2013](https://arxiv.org/html/2607.25373#bib.bib2); Alur et al\.,[2017](https://arxiv.org/html/2607.25373#bib.bib3); Barke et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib5); Odena et al\.,[2021](https://arxiv.org/html/2607.25373#bib.bib23)\)\. The recipe is to maintain a growing worklist of candidate expressions, deduplicate the worklist by behavior on the example inputs, and extend it level by level until some candidate matches the specification\. While this approach has been very effective in imperative and functional settings, it sits awkwardly inminiKanren\-style relational programming\(Byrd,[2009](https://arxiv.org/html/2607.25373#bib.bib6); Hemann and Friedman,[2013](https://arxiv.org/html/2607.25373#bib.bib14)\), where the natural search discipline is top\-down resolution against a fair stream of candidates\.

Indeed, severalminiKanrenrecipes have been developed for PBE\-style synthesis\. The dominant one is to write a relational interpreter for the target language and run it “backwards” against the input/output examples\(Byrd et al\.,[2017](https://arxiv.org/html/2607.25373#bib.bib7); Byrd and Rosenblatt,[2017](https://arxiv.org/html/2607.25373#bib.bib8)\); subsequent work has pursued, among other directions, neural guidance\(Zhang et al\.,[2018](https://arxiv.org/html/2607.25373#bib.bib31)\), multi\-stage programming\(Ballantyne et al\.,[2025](https://arxiv.org/html/2607.25373#bib.bib4)\), and concrete applications such as pattern\-matching compilation\(Kosarev et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib19)\),JavaScriptsynthesis\(Chirkov et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib10)\), and type inference\(Domoratskiy and Boulytchev,[2024](https://arxiv.org/html/2607.25373#bib.bib11)\)\. A simpler enumerate\-and\-test recipe writes a relation\(expr e\)that enumerates candidate expressions viaconde, conjoins it with a predicate that testseagainst the input/output examples by unification, and issues arun 1query to obtain the first matching candidate\. Both recipes work at toy depths \(or narrow search spaces\) and quickly drown at realistic ones\. The underlying issue, in the enumerate\-and\-test recipe that we focus on in this paper, is that the search tree contains many behaviorally\-equivalent expressions, and a fresh deduplication table created at each recursive level cannot reuse the work performed at the previous level\.

We aim to close this gap with two small library combinators on top of an unmodifiedμ\\upmuKanrencore\. The first,prune, filters an answer stream by a user\-supplied key \(typically the input/output behavior of a candidate\), keeping one representative per equivalence class\. The second,defrel/bank, memoizes a relation against canonical fresh variables, so that a single pruned answer stream is built*once*per\(run …\)and replayed at every call site\. Together, these combinators recover bottom\-up enumeration without leaving the relational setting and without changing the host search discipline\.[Figure1](https://arxiv.org/html/2607.25373#S1.F1)shows the resulting API: a complete arithmetic\-PBE expression enumerator in six lines, with no depth parameter and no per\-call deduplication plumbing\.

\(defrel/bank\(arith\-banke\)

\#:prune\(arith\-keye\)

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)

\(conde\[\(==e‘\(plus,l,r\)\)\]

\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-bankl\)\(arith\-bankr\)\)\]\)\)

Figure 1\.An arithmetic\-PBE expression enumerator usingdefrel/bank\. The\#:pruneclause attaches an observational key to the relation; the body is ordinaryminiKanrenwith no depth parameter\. The depth\-bounded equivalent \(in[Figure3](https://arxiv.org/html/2607.25373#S3.F3)\) requires an extra integer argument, a base case, and an explicit\(prune key …\)wrapper at every recursive level\.### 1\.1\.Contribution

Specifically, our contribution is as follows:

1. \(1\)In[Section3](https://arxiv.org/html/2607.25373#S3), we introduceprune, an answer\-stream deduplication combinator keyed on a user\-supplied function, together with theground\-keyandwhen\-groundhelpers that lift term\-level functions on ground terms into prune keys\.
2. \(2\)In[Section4](https://arxiv.org/html/2607.25373#S4), we presentdefrel/memoanddefrel/bank, two combinators for relation memoization against canonical fresh variables\. The latter further provides bottom\-up enumeration with shared deduplication across all call sites of a relation\. We also discuss the lazy\-template and thunk\-collapse tricks that allow recursive memoized relations to perform competitively\.
3. \(3\)In[Section5](https://arxiv.org/html/2607.25373#S5), we discussdefrel/bank\-w, a depth\-decayed best\-first variant whose weights live on*immature*streams\. This variant uses the lazy\-thunk weight ceiling as an A\*\-style admissible heuristic, allowing us to avoid forcing the very recursion the memoized stream is in the middle of building\.
4. \(4\)In[Section6](https://arxiv.org/html/2607.25373#S6), we report a preliminary empirical evaluation of all three variants on arithmetic and string PBE benchmarks up to depth 6\. In particular,defrel/bankis 9–99×\\timesfaster than depth\-boundedminiKanrenon 6 out of 8 deep arithmetic targets, and we characterize the two cases it loses\. We keep the benchmark suite small and plan a more thorough evaluation, including additional PBE domains and a comparison with bottom\-up SyGuS111Syntax\-Guided Synthesissolvers, for an extended version of this paper\.

The implementation of our combinators, together with the benchmark drivers used to produce[Table1](https://arxiv.org/html/2607.25373#S6.T1), is included in the Appendix \([AppendixA](https://arxiv.org/html/2607.25373#A1)\) and maintained at[https://github\.com/fizruk/prune\-kanren](https://github.com/fizruk/prune-kanren)\.

## 2\.Background

In this section, we briefly recall the standardμ\\upmuKanrencore that we build upon, set up the program\-by\-example setting we use as a running example throughout the paper, and explain why a naïveminiKanrenenumeration blows up at realistic depths\.

### 2\.1\.Theμ\\upmuKanrenCore

We assume the standardμ\\upmuKanrencore of Hemann and Friedman\(Hemann and Friedman,[2013](https://arxiv.org/html/2607.25373#bib.bib14)\): equality==, fresh\-variable introductioncall/fresh, disjunctiondisj, conjunctionconj, and an inverse\-η\\etadelay222Sometimes referred to asZzzin the literature\.that schedules recursive calls fairly\. Recall that, in this setting, a*goal*is a function from a state \(a substitution paired with a fresh\-variable counter\) to a stream of states, that is, of typestate→\\tostream of states\. Each state in the resulting stream represents one way in which the goal succeeds, recording the substitution extensions and any new fresh variables introduced along the way\. Answer streams themselves are either finite lists, immature thunks, or interleavings thereof, and the operatorpullrepeatedly forces thunks until a cons cell or an empty cell is exposed\. Variadic surface forms such asconde,fresh,run, andrun\*are defined as wrappers over these primitives in the usual way\.

It is important to note that we work with this minimal core deliberately: our prototype supports neither disequality constraints, nor symbolic or finite\-domain constraints, nor any other extension of the standardμ\\upmuKanrensubstitution\. Equality constraints, introduced by==and resolved by ordinary unification, are the only constraints that goals in our setting can impose on a state\. The combinators of[Sections3](https://arxiv.org/html/2607.25373#S3),[4](https://arxiv.org/html/2607.25373#S4)and[5](https://arxiv.org/html/2607.25373#S5)are designed against this minimal core\.

We believe this restriction is a matter of engineering rather than of principle\. On the memoization side, replay \([Section4](https://arxiv.org/html/2607.25373#S4)\) renames canonical bindings into the caller’s namespace, and the same renaming could be applied to a constraint store attached to each canonical cell\. On the pruning side, keys computed from ground terms that capture the entire answer, as in our PBE examples, appear unproblematic\. In general, however, more care is needed\. Two states that agree on the prune key may carry different constraint stores\. Thus, dropping one of them may lose answers unless the key is chosen to respect the constraints\. We have not implemented either part, and leave the interaction of pruning and memoization with richer constraint stores to future work\.

Our reimplementation ofμ\\upmuKanrenis in the modulesmicrokanren\.rktandwrappers\.rkt, listed in[SectionsA\.5\.1](https://arxiv.org/html/2607.25373#A1.SS5.SSS1)and[A\.5\.2](https://arxiv.org/html/2607.25373#A1.SS5.SSS2)\.

### 2\.2\.Programming by Example

Programming by example \(PBE\) is a form of program synthesis in which the specification is a small set of input/output examples rather than a full functional specification\(Gulwani,[2011](https://arxiv.org/html/2607.25373#bib.bib12)\)\. The synthesizer fixes a grammar of candidate programs and searches for*any*program that agrees with every example\. For instance, given the examples2↦42\\mapsto 4,3↦93\\mapsto 9, and4↦164\\mapsto 16over the arithmetic grammar of[Fig\.1](https://arxiv.org/html/2607.25373#S1.F1), a PBE synthesizer is expected to return\(times x x\)\. Any expression with the same behavior, such as\(times x \(times x 1\)\), is equally acceptable, since the examples do not distinguish them\. Indeed, a handful of examples underdetermines the target\. Thus, PBE systems typically return the first program found, and the user refines the examples if the result is not the intended one\. The flagship application of this workflow is string transformation in spreadsheets\(Gulwani,[2011](https://arxiv.org/html/2607.25373#bib.bib12)\), where an end user supplies a couple of before/after pairs instead of writing a formula\. The string domain in[Section6](https://arxiv.org/html/2607.25373#S6)is in this style\.

Throughout the paper, we use a single running setting: synthesize an arithmetic expression over a single variablexxand the constants 0 and 1 from a handful of input/output examples\. The grammar of such expressions is given in[Fig\.1](https://arxiv.org/html/2607.25373#S1.F1), with atomsx,0, and1, and the binary operatorsplusandtimes\. A relation\(expr e\)enumerates candidate expression terms; a predicate\(matches eio\)succeeds when the terme, evaluated on each example input inio, produces the expected output\. The expression

\(run 1 \(e\) \(expr e\) \(matches eio\)\)

then returns the first matching candidate\. Our target set, drawn from the benchmark modules \([SectionsA\.5\.9](https://arxiv.org/html/2607.25373#A1.SS5.SSS9)and[A\.5\.10](https://arxiv.org/html/2607.25373#A1.SS5.SSS10)\), ranges fromx2x^\{2\}\(with examples\(2,4\)\(2,4\),\(3,9\)\(3,9\),\(4,16\)\(4,16\)\) up throughx7x^\{7\}and\(1\+x\)5\(1\+x\)^\{5\}\.

In many uses of relational programming, e\.g\. when running a relational interpreter backwards, one is interested in the full multiplicity of answers, and collapsing behaviorally equivalent programs would be inappropriate\. The PBE query above is different\. It asks for*some*program consistent with the examples\. Thus, one representative per behavior suffices, and the remaining members of each equivalence class are pure search overhead\. For these reasons, our combinators are strictly opt\-in\. Deduplication applies only to relations that the user explicitly wraps inpruneor defines viadefrel/bank, and only with respect to the equivalence the user supplies\. The rest of the program retains the usualminiKanrensemantics\.[Section3](https://arxiv.org/html/2607.25373#S3)makes the induced completeness guarantee precise\.

### 2\.3\.Why Naïve Enumeration Blows Up

The number of syntactically distinct expression terms grows exponentially in the depth bound, but the number of distinct*behaviors*, that is, output tuples on the example inputs, grows much more slowly\. By depth 3, over the grammar of[Fig\.1](https://arxiv.org/html/2607.25373#S1.F1), there are several thousand candidate terms but only a few dozen distinct behaviors\. For example, the terms\(times x x\),\(times \(times x 1\) x\),\(times x \(times x 1\)\),\(times 1 \(times x x\)\), and many others all compute the same outputs on any input, and are therefore interchangeable for any PBE query\. A search that prunes by syntactic equality misses these collapses entirely\. What we need is*observational*deduplication, keyed by the behavior tuple rather than by the syntactic shape of the term\. This is the main trick of bottom\-up synthesizers\(Albarghouthi et al\.,[2013](https://arxiv.org/html/2607.25373#bib.bib2); Barke et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib5); Odena et al\.,[2021](https://arxiv.org/html/2607.25373#bib.bib23); Alur et al\.,[2017](https://arxiv.org/html/2607.25373#bib.bib3)\)\. In the next two sections, we transplant it intominiKanren\.

## 3\.ThepruneCombinator

The first combinator we introduce,prune, wraps a goal and filters its answer stream so that at most one state is emitted per distinct value of a user\-supplied*key*function\. Specifically, its signature is

prune : \(state→\\toany\)→\\togoal→\\togoal\.

The equivalence used to prune is chosen*per call*, so that the user is free to pick the equivalence appropriate to the problem at hand\. Typical choices include the behavior on the example inputs for PBE, the shape moduloα\\alpha\-renaming for relational interpreters, and syntactic identity for plain deduplication\.[Figure2](https://arxiv.org/html/2607.25373#S3.F2)gives the entire implementation ofprune\.

\(defineskip\-prune’skip\-prune\)

\\par\(define\(prunekeyg\)

\(lambda\(s/c\)

\(prune\-streamkey\(make\-hash\)\(gs/c\)\)\)\)

\\par\(define\(prune\-streamkeyseen$\)

\(cond

\[\(null?$\)’\(\)\]

\[\(procedure?$\)\(lambda\(\)\(prune\-streamkeyseen\($\)\)\)\]

\[else

\(let\*\(\[s/c\(car$\)\]\[k\(keys/c\)\]\)

\(cond

\[\(eq?kskip\-prune\)

\(conss/c\(prune\-streamkeyseen\(cdr$\)\)\)\]

\[\(hash\-has\-key?seenk\)

\(prune\-streamkeyseen\(cdr$\)\)\]

\[else

\(hash\-set\!seenk\#t\)

\(conss/c\(prune\-streamkeyseen\(cdr$\)\)\)\]\)\)\]\)\)

Figure 2\.Theprunecombinator\. The deduplication table is created fresh on each call and captured by the stream’s lazy thunks, so the deduplication state survives the inverse\-η\\etadelay used bymplusandbind\.### 3\.1\.Theskip\-pruneSentinel

A key function that depends on the value of a logic variable cannot produce a meaningful key when that variable is still fresh\. To handle this case, we introduce a sentinel valueskip\-prune, which tellsprune\-streamto emit the current state without recording it; that state will be revisited later, once the variable is bound\. Two small helpers package the common case in which the key is computed from a term once it has been instantiated\. First,ground\-key v fwalksvin the current substitution and appliesfif the result is ground, returningskip\-pruneotherwise\. Second,when\-ground v predis the predicate\-as\-goal companion that succeeds whenvwalks to a ground term satisfyingpred\.

Note that a state is subject to deduplication only when its key is computed, andground\-keycomputes a key only when the term is ground\. Thus, candidate terms that still contain logic variables are never recorded in the table and never dropped\. They pass throughpruneunfiltered and become subject to deduplication only once instantiated\. In particular, while the enumerators in this paper happen to produce fully ground candidates,pruneitself does not rely on this property\.

### 3\.2\.A Worked Example

For the arithmetic\-PBE setting of[Section2\.2](https://arxiv.org/html/2607.25373#S2.SS2), the behavior key takes the form

\(ground\-key e \(lambda \(t\) \(map \(lambda \(i\) \(arith\-interp t i\)\) inputs\)\)\),

whereinputsis the list of example inputs \(for instance,\(2,3,4\)\(2,3,4\)\), andarith\-interpis the host \(non\-relational\) interpreter for arithmetic expressions\. The depth\-bounded enumerator that we use as a baseline throughout the paper is shown in[Fig\.3](https://arxiv.org/html/2607.25373#S3.F3)\. Wrapping it with the behavior key above keeps exactly one representative per behavior tuple: of the many depth\-3 terms that compute\(4,9,16\)\(4,9,16\)forx∈\{2,3,4\}x\\in\\\{2,3,4\\\}, only the first one encountered is emitted, and the rest are silently dropped\.

\(define\(arith\-boundededepth\)

\(prune\(arith\-keye\)

\(cond

\[\(zero?depth\)

\(conde\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]\)\]

\[else

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)

\(conde\[\(==e‘\(plus,l,r\)\)\]

\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-boundedl\(\-depth1\)\)

\(arith\-boundedr\(\-depth1\)\)\)\]\)\]\)\)\)

Figure 3\.The depth\-bounded baseline enumerator for arithmetic PBE\. The integerdepthis decremented at each recursive call and a base case is taken when it reaches zero\. The body is wrapped in\(prune \(arith\-key e\) …\)at every level, so a fresh deduplication hash is allocated at every recursive call site\. We use this enumerator as theboundedengine in our evaluation \([Section6](https://arxiv.org/html/2607.25373#S6)\)\.
### 3\.3\.Completeness

Pruning never removes an equivalence class, only its non\-first representatives\. That is, for each key value,prune\-streamemits the first state and drops the subsequent states with the same key\. Therefore, for every statesof the unpruned goal there is a states′of the pruned goal withkey\(s′\) = key\(s\)\. A caller that observes states only throughkey\(which is the case for PBE, wherematchesconsumes only the behavior tuple\) thus sees a complete answer set up to the equivalence induced bykey\.

### 3\.4\.Why the Hash is Per\-Call

Usingprunein a recursive definition \(e\.g\. in[Figure3](https://arxiv.org/html/2607.25373#S3.F3)\) leads to many calls toprune, each with its own hash table and deduplication work\. A natural\-looking optimization is to thread a single deduplication table across all nestedprunes via a parameter, in the hope of amortizing the work across recursive levels\. Unfortunately, this breaks completeness\. With one shared table, the outer prune emitting\(== e ’x\)marks the behavior\(2,3,4\)\(2,3,4\)as seen; the recursive subgoal\(arith\-bounded l …\)can then no longer emitl = ’x, because that same behavior is already in the table\. As a consequence, the candidate\(times x x\), which depends onl = ’x, becomes unreachable\. In other words, the shared hash captures “seen as the outere” and conflates it with “seen as the innerl”\. A per\-call hash avoids this conflation\. We preserve a witness of this issue in the moduleshared\-table\-witness\.rktlisted in[SectionA\.5\.8](https://arxiv.org/html/2607.25373#A1.SS5.SSS8)\. The relational generalization that we present in[Section4](https://arxiv.org/html/2607.25373#S4)sidesteps the issue entirely by pruning at the level of*canonical*variables, where the variable identity is fixed\.

## 4\.Frompruneto Bottom\-Up Enumeration:defrel/bank

Wrapping a depth\-bounded enumerator withprune\([Section3](https://arxiv.org/html/2607.25373#S3)\) deduplicates within each call, but the deduplication work is not shared across calls\. In the arithmetic recursion of[Fig\.3](https://arxiv.org/html/2607.25373#S3.F3), the outer prune over\(arith\-bounded e depth\)and the recursive prune over\(arith\-bounded l \(\- depth 1\)\)each allocate a fresh hash, and the depth\-1 subgoal re\-pruning the same expression terms that the depth\-2 subgoal just pruned is, in fact, pure overhead\. What we want instead is a single stream of representatives \(a “bank”\), built once, shared across all call sites of the relation, and grown bottom\-up as new representatives become available\. This is the standard layout of non\-relational bottom\-up synthesizers\(Albarghouthi et al\.,[2013](https://arxiv.org/html/2607.25373#bib.bib2); Alur et al\.,[2017](https://arxiv.org/html/2607.25373#bib.bib3); Barke et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib5); Odena et al\.,[2021](https://arxiv.org/html/2607.25373#bib.bib23)\), and we obtain it inminiKanrenby memoizing the relation against*canonical*fresh variables\.

### 4\.1\.Canonical Variables and Replay with Renaming

Our first idea is to memoize a relation against*canonical variables*\. For a relation of arityNN, the canonical variables are its parameters, instantiated as the firstNNfresh variables\(var 0\), …,\(var N\-1\)of an otherwise empty state\. Intuitively, they represent the*most general call*of the relation\. Running the body once against the canonical variables produces the*canonical stream*, that is, the answer stream of the most general call\. Its cells are state/counter pairs in which the parameters are bound to answer terms, with internal fresh variables counting upward fromNN\. We refer to one such cell as a*canonical cell*\. Readers familiar with tabledminiKanren\(Byrd,[2009](https://arxiv.org/html/2607.25373#bib.bib6), Part IV\)may read a canonical cell as the analogue of a cache entry, for a cache keyed on the most general call\. We return to this analogy in[Section7](https://arxiv.org/html/2607.25373#S7)\. The stream is stored in a per\-\(run …\)cache, which we expose as thecurrent\-memoparameter; each subsequent call\(rela1a\_\{1\}…aNa\_\{N\}\)then replays the canonical stream against the caller’s arguments\. The replay is itself a stream of caller states, computed cell by cell\. For each canonical cell\(σc,cc\)\(\\sigma\_\{c\},c\_\{c\}\)and each input positioni∈\{0,…,N−1\}i\\in\\\{0,\\ldots,N\-1\\\}, the canonical valueσc\\sigma\_\{c\}assigns to\(var i\)is walked, then renamed \(input variables\(var i\)fori<Ni<Nare replaced by the caller’saia\_\{i\}, and canonical internal fresh variables\(var j\)forj≥Nj\\geq Nare shifted into the caller’s namespace by adding the caller’s counter offset\), and finally unified into the caller’s substitution\. A canonical cell survives the replay only when every renamed value unifies with its corresponding caller argument; otherwise that cell is silently dropped\. As a consequence, structured caller arguments such as\(times a b\)are handled by unification “for free”: if the canonical value at positioniiwalks to\(timeslcl\_\{c\}rcr\_\{c\}\)for somelc,rcl\_\{c\},r\_\{c\}, then unifying against\(times a b\)either succeeds and extends the caller’s substitution with bindings foraandb, or fails because the heads disagree\. No special case is needed\.

To make this concrete, consider running the relationarith\-bankof[Fig\.1](https://arxiv.org/html/2607.25373#S1.F1)against the canonical variable\(var 0\)\. The body produces an infinite sequence of cells, the first few of which are summarized in the second column of[Fig\.4](https://arxiv.org/html/2607.25373#S4.F4)\. Now suppose a caller makes the structured call\(arith\-bank \(times a b\)\), whereaandbare fresh logic variables in the caller’s namespace\. The third column of[Fig\.4](https://arxiv.org/html/2607.25373#S4.F4)shows what the replay does for each canonical cell: it walks\(var 0\)inσc\\sigma\_\{c\}, observes the canonical value \(no renaming of internal vars is needed here, since each pruned canonical cell walks to a ground term\), and unifies the result with\(times a b\)\. Three of the first four cells fail the head\-mismatch check immediately and are dropped, and only thetimes\-headed cells survive and propagate bindings foraandbback to the caller\.

Figure 4\.A worked walk\-through of replay\. The middle column shows the value to which\(var 0\)walks in the first few canonical cells ofarith\-bank; the right column shows what the replay does for each cell when the caller’s argument is the structured term\(times a b\)\. Only thetimes\-headed cells survive and add to the caller’s substitution; the rest are silently dropped by unification\.We definedefrel/memohelper to enable relations with memoization against canonical variables and replay\.

### 4\.2\.Termination of Recursive Memoized Relations

It is important to note that a naïve ordering would force the body before installing the cache cell, in which case recursive calls would re\-enter the body and diverge\. We avoid this by installing the cache cell*first*and only then evaluating the body\. The recursive calls inside the body are wrapped by the inverse\-η\\etadelay of[Section2\.1](https://arxiv.org/html/2607.25373#S2.SS1), so that each one is a thunk that fires only when the answer stream is forced\. By the time the stream is forced, the cache cell is already in place, and the recursive call returns the canonical stream itself\.

### 4\.3\.Memoization With Canonical Pruning

We now have a single canonical stream that is shared across all call sites, but it is still unpruned\. To get a pruned canonical stream, we simply wrap the body inpruneat canonical\-stream construction time\. In the surface syntax,defrel/bank333We choose*bank*rather than*tabled*or*memo*to emphasize that the cached structure is not a tabling table, but a set of*representatives*pruned by observational equivalence\. The term is borrowed from the non\-relational bottom\-up PBE literature \(see[Section7](https://arxiv.org/html/2607.25373#S7)\), where it denotes a worklist of representative programs grown level by level\. Using*tabled*would mislead, since tabledminiKanrenpreserves every syntactically distinct answer \(up to variable renaming\), while the bank keeps one representative per*semantic*class; using*memo*would underspell, since pure memoization without pruning is the weaker construct that we calldefrel/memo\.is essentially justdefrel/memoplus a\#:pruneclause supplying a deduplication key:

\(defrel/bank \(rel x …\) \#:prune key\-expr body …\)\.

Thekey\-expris evaluated in the scope of the relation parameters and may therefore refer to them\. For our running example, the key is\(arith\-key e\)from[Section2\.2](https://arxiv.org/html/2607.25373#S2.SS2)\. At canonical\-stream construction time, the body is wrapped in\(prune key\-expr …\), so that the resulting canonical bank already contains exactly one representative per behavior, and every replay automatically inherits the deduplication\. In particular, the teaser in[Fig\.1](https://arxiv.org/html/2607.25373#S1.F1)is precisely this combination applied to the arithmetic grammar\. Importantly, pruning at the canonical level also sidesteps the shared\-table anti\-pattern of[Section3\.4](https://arxiv.org/html/2607.25373#S3.SS4)\. Indeed, the canonical input variables\(var 0\), …,\(var N\-1\)are fixed across all call sites, so that “seen as the outere” and “seen as the innerl” are no longer distinct concepts; they are the same canonical\(var 0\)\.

### 4\.4\.Implementation Notes

Two small engineering tricks make the scheme perform competitively with the depth\-bounded baseline of[Fig\.3](https://arxiv.org/html/2607.25373#S3.F3)\. First, replay walks each input variable in the canonical substitution and unifies the result, rather than iterating all bindings of the canonical substitution \(most of which are internal\-to\-internal and invisible to the caller\)\. Thiswalk\*\-based replay roughly halves the cost of replay\. Second, when forcing an immature canonical thunk during replay, we keep forcing through any chain of nested thunks until a concrete cons cell appears\. This is analogous topullon the consumer side\. Applying forcing on the producer side as well, we observe that the per\-target thunk\-force count drops from∼330 000\\sim\\\!330\\,000to∼3500\\sim\\\!3500on the hard arithmetic targets, bringingdefrel/bankwithin1\.5×1\.5\\timesof the depth\-bounded baseline before pruning’s algorithmic advantage takes over\. We refer the reader to[SectionA\.5\.4](https://arxiv.org/html/2607.25373#A1.SS5.SSS4)for the full implementation ofmemo\.rkt; a complete walkthrough is deferred to a future extended version of this paper\.

## 5\.Best\-First Variant:defrel/bank\-w

The canonical stream ofdefrel/bankis built by ordinary depth\-first recursion throughcondeandconj, so it emits cells roughly in the order the body explores them\. For the arithmetic grammar of[Fig\.1](https://arxiv.org/html/2607.25373#S1.F1), this means that the stream emitsx,\(times x x\),\(times x \(times x x\)\), and so on \(a long right\-spine oftimeschains\) well before anything starting with\(plus 1 x\)\. Behaviors such as\(1\+x\)k\(1\+x\)^\{k\}then sit far down the bank, and targets that require them become practically unreachable: the search has to drain thousands of intervening representatives first\. Naturally, increasing the depth bound does not help, since the bias lies in*which cells the bank emits first*, rather than in which cells it could in principle contain\.

What we want is a best\-first enumeration: emit shallow representatives before deep ones, regardless of the order the body happens to walk them\. We obtain such an enumeration by attaching weights to immature stream cells and givingmplusa sorted\-merge discipline\.

### 5\.1\.Weights on Immature Streams

The core data and themplus\-wrule are shown in[Fig\.5](https://arxiv.org/html/2607.25373#S5.F5)\. The structure\(lazy weight thunk\)represents an immature stream paired with an upper bound on the weight of any cell it could ever emit\. The functionpeek\-weightreturns this bound without forcing, andmplus\-wapplied to two immature streams returns a single immature stream whose ceiling is the maximum of the two\. Only when the consumer pulls doesmplus\-wdescend into the side whose ceiling could still produce the next winning cell\. The lazy’s ceiling plays the role of an admissible heuristic in A\*\-style search\(Hart et al\.,[1968](https://arxiv.org/html/2607.25373#bib.bib13)\): it never under\-estimates the true weight, so a side that loses on peek can be safely deferred\. The design choice of carrying the heuristic on*immature*stream cells, so that one side can win a comparison without ever being forced, is inspired by best\-first proof\-search tactics, in particular Lean 4’s Aesop\(Limperg and From,[2023](https://arxiv.org/html/2607.25373#bib.bib20)\)\.

Internally,mplus\-wkeeps the alternatives of nested merges in a pairing max\-heap keyed bypeek\-weight, hidden behind the ordinary stream interface\. Thus, nested merges meld their heaps in constant time, and emitting the next cell costs amortized logarithmic time in the number of suspended alternatives\. This matters in practice\. An earlier version of our implementation built nests of binary merges, and re\-traversing the frontier of suspended alternatives on every pull dominated the run time of best\-first search \(see[Section6](https://arxiv.org/html/2607.25373#S6)\)\.

\(structlazy\(weightthunk\)\);ceilingonwhat

;thunkcanemit

\\par\(define\(peek\-weight$\)

\(cond\[\(null?$\)\-inf\.0\]

\[\(lazy?$\)\(lazy\-weight$\)\]

\[else\(car\(car$\)\)\]\)\);weightedcell

\\par\(define\(mplus\-w$1$2\)

;;n\-arysortedmerge:alternativesarekeptina

;;pairingmax\-heapkeyedbypeek\-weight;never

;;forcesalazythatlosesonpeek\.

…\)

Figure 5\.The weighted\-stream core\.lazycells advertise an admissible upper bound, andmplus\-wmerges them by peek without forcing\.
### 5\.2\.Why Peek\-Without\-Force Matters

It is important thatpeek\-weightdoes not force its argument\. Indeed, a naïve sorted merge that forces both heads in order to read their weights would re\-enter the very canonical stream thatdefrel/bank\-wis in the middle of building\. To see this, observe that forcing the head of an immature canonical thunk hitsmemo\-thunk, which calls back into the canonical body, which recurses into the relation, which asks for the next cell of the canonical stream, and so on, in an unbounded cycle\. The lazy\-ceiling discipline cuts the cycle: the ceiling is fixed at the moment thelazyis constructed \(withZzz\-wdefaulting to1\.01\.0\), and this is enough to order merges without forcing anything\.

### 5\.3\.Depth\-Decayed Best\-First Enumeration

The user\-facing form,defrel/bank\-w444The suffix\-wstands for*weighted*and matches our convention throughout the paper, where weighted analogues of the standardminiKanrencombinators are suffixed with\-w\(conde\-w,fresh\-w,mplus\-w, and so on\)\., extendsdefrel/bankwith a decay factor:

\(defrel/bank\-w \(rel x …\) \#:prune key\-expr \#:decay d body …\)\.

The body uses the weighted versions of standard combinators \(conde\-w,fresh\-w, andconj\-w\+\), and the recursive call sites apply\(scale\-w d\)to their immature streams, multiplying the ceiling by the decay factor \(which defaults to0\.50\.5\)\. The exponential depth decay gives shallow representatives the smallest ceilings, so they emerge from the sorted merge first\. With this discipline, the canonical bank emitsx, then\(plus x x\),\(times x x\), and\(plus 1 x\)together at depth 1, then all the depth\-2 representatives, and so on\. This is precisely the order needed to find\(plus 1 x\)2early\.

### 5\.4\.The Trade\-Off

Of course, best\-first enumeration finds compact representatives, but it pays breadth\-first costs: emitting any depth\-KKcell requires first emitting*all*cells of depth<K<K\. For PBE behavior spaces with thousands of distinct behaviors at depth 3, this is much slower thandefrel/bank’s depth\-first drilling\. Neither variant dominates, and[Section6](https://arxiv.org/html/2607.25373#S6)shows that they trade places across the benchmark suite\.

## 6\.Evaluation

The evaluation that follows is deliberately preliminary\. Our goal here is to establish thatpruneanddefrel/bankyield substantial speedups on a representative slice of PBE problems, and to surface the regimes in which each variant succeeds or fails, so that the choice of engine is informed\. We make the limitations of this evaluation explicit at the end of this section, together with the future evaluations they call for\.

The benchmarks we use are drawn from the modulesshallow\-bench\.rkt\(which provides broad coverage of arithmetic targets at depths 0–3 and string PBE targets at depths 2–3\) anddeep\-bench\.rkt\(which focuses on deep arithmetic targets at depths 4–6\)\. Each target consists of three input/output examples and a minimum search depth, that is, the smallest depth at which a solution exists\. The minimum depth is used to set the bound for the depth\-bounded engine\. All measurements are end\-to\-endrun 1times, that is, the wall\-clock time from query submission to the first matching candidate\. The benchmarks were executed with Racket 9\.1 \(CS\) on an Apple M4 Pro with 24 GB of memory, running macOS 26\.5\. The methodology differs slightly between the two benchmark scripts\. For the shallow targets, each cell is the mean per\-iteration time over 50–1000 iterations \(the iteration count is chosen per target to keep total bench time manageable\)\. For the deep arithmetic targets, the search times can vary by orders of magnitude across the engines, so each cell is a single run prefixed by a forced garbage collection, with per\-target timeouts of 30 seconds for targets at depths≤5\\leq 5and 60 seconds for those at depth 6\.

### 6\.1\.Engines

We compare four engines:

1. \(1\)bounded, the depth\-bounded enumerator of[Fig\.3](https://arxiv.org/html/2607.25373#S3.F3), given the minimum depth for each target asdd\.
2. \(2\)bank, thedefrel/bankof[Section4](https://arxiv.org/html/2607.25373#S4), that is, a depth\-first canonical enumeration with shared deduplication\.
3. \(3\)bank\-w, thedefrel/bank\-wof[Section5](https://arxiv.org/html/2607.25373#S5)with default decay0\.50\.5, providing depth\-decayed best\-first enumeration\.
4. \(4\)host\-bank, a non\-relational host\-language baseline \(modulebank\.rkt,[SectionA\.5\.5](https://arxiv.org/html/2607.25373#A1.SS5.SSS5)\) that builds an exhaustive deduplicated bank in Racket up to the target’s minimum depth and then exposes its membership predicate to a single relationalrun 1query viamembero\. Unlikedefrel/bank, the bank is built outside the relational engine and does not compose with arbitrary relational goals\.

##### A note on search order\.

The four engines above differ not only in their raw machinery, but also in the*order*in which they enumerate candidate programs:boundedfollows the naturalcondeorder capped by an explicit depth bound;defrel/bankemits cells in canonical recursion order \(depth\-first, biased toward the right spine of thecondebody\);defrel/bank\-wuses depth\-decayed best\-first ordering; andhost\-bankenumerates the bank level by level\. Since each measurement is the time to find the*first*matching candidate, the absolute numbers in[Table1](https://arxiv.org/html/2607.25373#S6.T1)reflect the interaction between an engine’s enumeration order and where the target’s representative happens to sit in that order, rather than the engines’ raw throughput\. A representative that lies early in one engine’s enumeration may lie arbitrarily deep in another’s, so the speedup ratios that follow are best read as characterizing the regimes \(target shape×\\timesenumeration discipline\) in which each engine wins, rather than as universal performance numbers\. To make this interaction explicit, each cell of[Table1](https://arxiv.org/html/2607.25373#S6.T1)is annotated with the position at which the first matching candidate appears in that engine’s enumeration order\.

Table 1\.End\-to\-endrun 1search times, including any bank build cost\. Bold marks the fastest engine per row; TO denotes a timeout \(30 seconds for arithmetic targets at depths≤5\\leq 5, 60 seconds for depth 6, and 30 seconds forbank\-won string targets\)\. The four engines use different enumeration orders \(see the discussion above\), so the times here measure the \(target×\\timesorder\) interaction rather than engine speed in isolation\. To make the interaction visible, each cell is annotated with \(\#nn\), the 1\-based position of the first matching candidate in that engine’s enumeration order\. The indices are deterministic and are produced by the moduleorder\-bench\.rkt\.

### 6\.2\.Discussion of the Results

We now discuss the results in[Table1](https://arxiv.org/html/2607.25373#S6.T1)engine by engine\.

##### bounded: predictable, but rate\-limited by depth\.

The depth\-bounded enumerator is the only engine that never times out on the deep arithmetic targets, including the hard\(1\+x\)k\(1\+x\)^\{k\}row\. Indeed, pruning at every recursive level is correct, and the cheap depth cut keeps the candidate frontier bounded\. The cost, however, shows up in absolute terms: at depths 5 and 6,boundedis consistently one to three orders of magnitude slower thanbankon the targets they both solve\. This is because every call site allocates a fresh deduplication hash and re\-prunes the same sub\-expressions that the previous level has already pruned\.

##### bank: roughly 9–99×\\timesfaster on 6 out of 8 deep arithmetic targets, except the\(1\+x\)k\(1\+x\)^\{k\}family\.

On the deep arithmetic suite,defrel/bankis between roughly9×9\\timesand99×99\\timesfaster thanboundedon every target whose representative lies along the right\-spine of thecondebody, that is, thexkx^\{k\}andxk\+cx^\{k\}\+cfamily\. We stress, however, that these ratios are a property of the \(target, enumeration\-order\) pair rather than ofdefrel/bankitself, sincedefrel/bankandboundedexplore the candidate space in different orders\. For the right\-spine family, the bank’s canonical enumeration places the answer very early; for the\(1\+x\)k\(1\+x\)^\{k\}family of the same depth, the same canonical enumeration places the answer very late, and the ratio inverts\. Specifically, the bank either loses by a wide margin \(at depth 4,\(1\+x\)4\(1\+x\)^\{4\}is solved by the bank in1\.991\.99seconds versus139139ms forbounded\) or times out altogether \(at depth 5,\(1\+x\)5\(1\+x\)^\{5\}is found byboundedin6\.586\.58s while both the bank and the weighted variant time out\)\. The reason is that the canonical bank emits right\-spinetimeschains long before anything starting with\(plus 1 x\)\. Indeed, the representative of\(1\+x\)2\(1\+x\)^\{2\}sits at position 143 in the bank, that of\(1\+x\)3\(1\+x\)^\{3\}at position 3691, and that of\(1\+x\)4\(1\+x\)^\{4\}at position 243 158 \(see the indices in[Table1](https://arxiv.org/html/2607.25373#S6.T1)\)\. We have also verified that fair conjunction in the style of Kiselyov, Shan, Friedman, and Sabry\(Kiselyov et al\.,[2005](https://arxiv.org/html/2607.25373#bib.bib18)\)does*not*fix this: an experimentalconj\-ivariant \(mplus\-i/bind\-iwith diagonal pairing\) reproduces the same first 30 canonical cells as the standardconj\. The bias lies in*which cells exist*in the bank, not in*how pairs of cells are formed*, which is a problem fair conjunction cannot address\.

##### bank\-w: compact representatives, competitive on wide\-but\-shallow behavior spaces\.

The weighted variantdefrel/bank\-wreverses the trade\-off\. Whenever it terminates, it returns the most compact representative of the target behavior\. For example, for\(1\+x\)3\(1\+x\)^\{3\}it finds\(times \(times \(plus 1 x\) \(plus 1 x\)\) \(plus 1 x\)\), wherebankreturns a sprawling depth\-8 term\. Its enumeration indices are correspondingly small \(\#29 for\(1\+x\)2\(1\+x\)^\{2\}and \#107 for\(1\+x\)3\(1\+x\)^\{3\}, versus \#143 and \#3691 forbank\)\. On the string suite,bank\-wis competitive across the board and wins the depth\-3 row outright \(10\.410\.4ms versus31\.531\.5ms forbounded\)\. On deep arithmetic, however, emitting any depth\-KKcell still requires emitting every lighter cell first, and the four hardest rows time out\. We seebank\-was the right tool when the behavior space is wide but the target is shallow, and when obtaining the compact representative matters\.

Our original expectation forbank\-wwas more optimistic\. We hoped that best\-first enumeration would neutralize the enumeration\-order bias ofdefrel/bankat an acceptable cost, makingbank\-wthe default engine\. In the version of this paper submitted for review, this expectation failed badly\. There,bank\-wtimed out on all arithmetic targets except\(1\+x\)2\(1\+x\)^\{2\}andx5x^\{5\}, and also on the depth\-3 string target\. A reviewer asked us to explain why\. Investigating the question revealed an implementation artifact rather than a fundamental limit\. The enumeration indices show that the number of*emitted*cells is modest, since pruning keeps one representative per behavior\. However, our originalmplus\-wbuilt nests of binary merges, so emitting each cell re\-traversed the entire frontier of suspended alternatives\. For example, on\(1\+x\)2\(1\+x\)^\{2\}, emitting 34 cells cost6666ms, roughly22ms per cell\.555The count differs from the \(\#29\) reported in[Table1](https://arxiv.org/html/2607.25373#S6.T1)because the pairing\-heap merge breaks ties within an equal\-weight class differently than the binary nests did\. Both orders are deterministic\.This is three orders of magnitude more thanbank’s per\-cell cost on the same target\. Replacing the nests with the pairing\-heap merge of[Section5](https://arxiv.org/html/2607.25373#S5)improvedbank\-wby one to three orders of magnitude across the suite:\(1\+x\)2\(1\+x\)^\{2\}from6666ms to1616ms,x5x^\{5\}from4\.14\.1s to126126ms,\(1\+x\)3\(1\+x\)^\{3\}and three depth\-5 targets from timeout to seconds, and the depth\-3 string target from timeout to10\.410\.4ms\.[Table1](https://arxiv.org/html/2607.25373#S6.T1)reports the heap\-based numbers\. What remains is the genuine breadth\-first cost\. Every cell of a weight class must be emitted before any cell of a lower class, and the class sizes grow with the number of distinct behaviors per level \(already thousands at depth 3 for arithmetic\)\. This is why the deepest arithmetic rows still time out\.

##### The decay factor\.

A natural question is how sensitivebank\-wis to the value of the decay factordd\. In exact arithmetic, it is not sensitive at all\. With a uniform decay applied at every recursive call, the weight of every canonical cell isdnd^\{n\}, wherenncounts the decay applications in the cell’s derivation\. For everyd∈\(0,1\)d\\in\(0,1\),dnd^\{n\}is monotone innn\. Thus, the pairwise comparisons made bymplus\-wreduce to comparisons of derivation sizes, and the enumeration order does not depend ondd\. In floating\-point arithmetic, the picture is subtler\. We verified it empirically ford∈\{0\.9,0\.75,0\.5,0\.25,0\.1\}d\\in\\\{0\.9,0\.75,0\.5,0\.25,0\.1\\\}\(moduledecay\-bench\.rkt\)\. The sequence of*weight classes*in the first 50 canonical cells is identical for all five values\. However, the order*within*an equal\-weight class is perturbed ford=0\.9d=0\.9andd=0\.1d=0\.1, whose powers are not exactly representable in double precision\. Indeed, the observed divergence points sit exactly at class boundaries\. The valuesd∈\{0\.75,0\.5,0\.25\}d\\in\\\{0\.75,0\.5,0\.25\\\}, whose powers are exactly representable at these sizes, produce literally identical orders\. The within\-class order can matter in practice\. For example, on the\(1\+x\)2\(1\+x\)^\{2\}target, the accidental order induced byd=0\.9d=0\.9finds the target roughly6×6\\timesfaster than the exact\-arithmetic order \(2\.82\.8ms versus1717ms\)\. This is luck rather than principle\. Thus, the decay knob becomes meaningful only once different productions carry different weights \(e\.g\. Probe\-style learned weights\(Barke et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib5)\)\), which we leave to future work\.

##### host\-bank: complementary strengths, but non\-compositional\.

The non\-relationalhost\-bankbaseline exhibits a behavior that is, in many ways, complementary todefrel/bank\. On shallow targets, the host bank is the fastest engine\. In particular, on the\(1\+x\)k\(1\+x\)^\{k\}family fork∈\{2,3\}k\\in\\\{2,3\\\},host\-bankfinds the compact representative in fractions of a millisecond, wheredefrel/bankeither ties or loses by an order of magnitude\. At depth 4,host\-banksolves\(1\+x\)4\(1\+x\)^\{4\}in165165ms, comparable tobounded’s141141ms and an order of magnitude better thandefrel/bank’s1\.991\.99s\. The reason is thathost\-bank’s level\-by\-level construction does not suffer from the right\-spine bias of[Section5](https://arxiv.org/html/2607.25373#S5), and it sees\(1\+x\)\(1\+x\)as early as any other depth\-1 representative\.

On the deep right\-spine targets, however,host\-bankloses catastrophically\. Already atx5x^\{5\}\(depth 4\) it spends154154ms, two orders of magnitude slower than the0\.10\.1ms ofdefrel/bank\. From depth 5 onwards, the cost of building the exhaustive bank exceeds the search budget andhost\-banktimes out on every target\. The same pattern shows up on the string targets, where the host bank is competitive withdefrel/bankat depth 2 but degrades to119119s per iteration at depth 3, as the bank build has to enumerate every depth\-3 string composition\.

In any case, the host bank achieves whatever performance it has by abandoning the relational interface: the bank is built outsideminiKanren, and the membership predicate cannot be combined with arbitrary relational goals such as typed enumerators, refinement constraints, or mutual recursion across relations\. By contrast,defrel/bankkeeps the bank inside the relational language, recovering most of the host\-bank speedup where the right\-spine bias does not bite, and remaining composable with the rest ofminiKanren\.

##### Which engine, when\.

The preceding paragraphs suggest simple selection guidance\. Useboundedwhen the target depth is known \(or can be iterated over\) and predictability matters most\. It is the only engine that never times out in our suite\. It also remains the fastest on the shallow string rows and on deep targets whose representatives sit late in the canonical order \(the\(1\+x\)k\(1\+x\)^\{k\}family\)\. Usedefrel/bankas the default depth\-less engine\. It wins by one to two orders of magnitude whenever the target’s representative sits early in the canonical order \(thexkx^\{k\}andxk\+cx^\{k\}\+cfamily\)\. Its failure mode is confined to representatives that sit late in that order\. Usedefrel/bank\-wwhen the behavior space is wide but the target is shallow \(it wins the depth\-3 string row\), or when obtaining the compact representative matters more than raw speed\. Finally, use the host\-language bank when compositionality with other relational goals is not needed and the minimum depth is small\.

##### Limitations of this evaluation\.

We close the section by making the limitations of this evaluation explicit\.

- •The suite covers two domains with one grammar each, 14 targets in total\. Conclusions about which enumeration order wins on which target shape may not transfer to richer grammars\.
- •The deep arithmetic cells are single runs\. Ratios drift across executions, and cells close to the budget may flip to a timeout\. For example,bank\-wsolvesx5\+1x^\{5\}\+1in26\.426\.4s against a3030s budget\.
- •boundedis given the minimum depth for each target, which is its best case\. In practice the right depth is unknown, and the cost of discovering it \(e\.g\. by iterative deepening\) is not measured\.
- •All four engines are our own implementations over the same core\. We do not yet compare against tabledminiKanren, relational\-interpreter synthesis, or bottom\-up SyGuS solvers\.
- •We measure wall\-clock time to the first answer only\. Memory consumption \(the canonical bank persists for the whole run\) is not reported\.

Correspondingly, we plan the following evaluations for an extended version of this paper, each matched to an open question:

- •additional PBE domains \(bit\-vector, list, typed\-component synthesis\), to test whether the enumeration\-order regimes of[Table1](https://arxiv.org/html/2607.25373#S6.T1)persist on richer grammars;
- •a comparison with tabledminiKanrenon relations where both apply, to quantify the cost of semantic versus syntactic deduplication;
- •a comparison with bottom\-up SyGuS solvers on a common subset of targets, to locate the overhead of staying relational;
- •repeated\-trial timing with memory profiling\.

## 7\.Related Work

We organize the related work into four threads, covering bottom\-up PBE synthesis, prior work on synthesis viaminiKanren, tabling in logic programming, and fair search\.

### 7\.1\.Bottom\-Up PBE Synthesis

Bottom\-up enumeration with observational deduplication is the central idea behind a long line of non\-relational PBE synthesizers\(Albarghouthi et al\.,[2013](https://arxiv.org/html/2607.25373#bib.bib2); Alur et al\.,[2017](https://arxiv.org/html/2607.25373#bib.bib3); Barke et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib5); Odena et al\.,[2021](https://arxiv.org/html/2607.25373#bib.bib23)\)\.666We use “relational” here in theminiKanrensense, that is, programs written as multi\-way relations over logic variables\. Wang, Wang, and Dillig\(Wang et al\.,[2018](https://arxiv.org/html/2607.25373#bib.bib30)\)use the same word for the unrelated notion of synthesizing pairs of programs satisfying a relational specification\.These tools maintain a worklist of representative expressions, deduplicated by their behavior on the example inputs, and grow the worklist level by level until a candidate matches the specification\. We adopt the same bottom\-up plus observational\-equivalence skeleton indefrel/bank: the canonical\-variable bank*is*a bottom\-up worklist, except that it is consumed byminiKanren’s unification\-driven search rather than by an explicit enumeration loop, and it composes with arbitrary relational goals such as typed enumerators, refinement constraints, or mutual recursion across relations\. One specific neighbor worth singling out, on thedefrel/bank\-wside rather than thedefrel/bankside, is Barke, Peleg, and Polikarpova’s Probe\(Barke et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib5)\), which layers a just\-in\-time\-learned probabilistic context\-free grammar over a bottom\-up behavior\-pruned bank to bias the enumeration order toward likely solutions\. The closest analog in our paper is the much simpler depth\-decay heuristic ofdefrel/bank\-w\([Section5](https://arxiv.org/html/2607.25373#S5)\); layering a Probe\-style learned ranker on top ofdefrel/bank\-wwould be a natural direction for future work\. A complementary angle on the same goal of shrinking the effective PBE search space is taken by Hocquette and Cropper\(Hocquette and Cropper,[2025](https://arxiv.org/html/2607.25373#bib.bib17)\), who decompose each example into position\-indexed input/output facts and learn relations between those facts via inductive logic programming\. Their decomposition acts on the*representation*side, reshaping how the examples are presented to the synthesizer; ourpruneacts on the*enumeration*side, quotienting candidate answers by observational equivalence\.

### 7\.2\.Synthesis viaminiKanren

The closest prior work on*relational*synthesis usesminiKanrenas a top\-down search engine over relational interpreters\. The idea is to run a relational evaluator “backwards” against the target input/output examples, and the search then returns programs whose evaluation matches the examples\. Byrd, Ballantyne, Rosenblatt, and Might\(Byrd et al\.,[2017](https://arxiv.org/html/2607.25373#bib.bib7)\)demonstrate this recipe on a suite of synthesis problems, and the Barliman prototype\(Byrd and Rosenblatt,[2017](https://arxiv.org/html/2607.25373#bib.bib8)\)packages it into a live program\-completion tool\. Hemann and Friedman\(Hemann and Friedman,[2020](https://arxiv.org/html/2607.25373#bib.bib15)\)extend the canon with further quine\-style benchmarks and “mirrored” relational\-interpreter tasks\. The same recipe has also been applied to several non\-toy languages: Chirkov*et al\.*\(Chirkov et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib10)\)build a relational interpreter for a subset of JavaScript by composing a relational S\-expression parser with a relational evaluator, Kosarev, Lozov, and Boulytchev\(Kosarev et al\.,[2020](https://arxiv.org/html/2607.25373#bib.bib19)\)synthesize pattern\-matching decision trees by running a low\-level switch relation backward against a high\-level pattern\-match relation, and Domoratskiy and Boulytchev\(Domoratskiy and Boulytchev,[2024](https://arxiv.org/html/2607.25373#bib.bib11)\)report the OCanren extensions and optimizations needed to scale a relational type\-inference solver beyond toy STLC examples\. Thepruneanddefrel/bankcombinators of the present paper are in the same spirit of small additions to vanillaminiKanrenthat aim to make this recipe scale\.

Two recent directions are worth contrasting more closely with our work\. First, Rosenblatt, Zhang, Byrd, and Might\(Rosenblatt et al\.,[2019](https://arxiv.org/html/2607.25373#bib.bib24)\)introduce a first\-order defunctionalized representation ofminiKanrengoals and streams that decouples search from semantics, making it easier to swap in alternate search strategies, and Zhang*et al\.*\(Zhang et al\.,[2018](https://arxiv.org/html/2607.25373#bib.bib31)\)pursue one such alternate strategy, training a neural network to score candidate branches in theminiKanrensearch tree and thereby guide the search toward promising sub\-searches on PBE problems\. Our emphasis is different: we focus on memoization of canonical\-variable streams and on pruning those streams by observational equivalence, rather than on the order in which branches of a top\-down search are expanded\. Second, Ballantyne*et al\.*\(Ballantyne et al\.,[2025](https://arxiv.org/html/2607.25373#bib.bib4)\)attack the per\-query overhead of synthesis\-via\-relational\-interpreters from a different angle, lifting MetaOCaml\-style multi\-stage programming intominiKanrenso that the known parts of a partially\-unknown program can be compiled away, leaving only the relational holes to be solved\. Their staging and our memoization are complementary: their technique cuts the per\-step cost of the relational interpreter, whereasdefrel/bankcuts the cost of re\-enumerating the same answer set across recursive call sites of a sub\-relation\.

We view all of these efforts as orthogonal todefrel/bank: relational interpretation describes the synthesis problem declaratively, whiledefrel/bankadds bottom\-up enumeration to the underlying search, and we believe that the several lines compose\. The branch\-selection question of Zhang*et al\.*\(Zhang et al\.,[2018](https://arxiv.org/html/2607.25373#bib.bib31)\)does surface narrowly for our weighted variantdefrel/bank\-w, where we answer it with an admissible\-heuristic ceiling on immature streams rather than with a learned scorer; combining the two answers would be an interesting direction for future work\.

### 7\.3\.Tabling in Logic Programming

Tabling, that is, memoizing the answer set of a relation, has a long history\. The foundational technique is OLD resolution with tabulation\(Tamaki and Sato,[1986](https://arxiv.org/html/2607.25373#bib.bib29)\), and SLG resolution as implemented in XSB\(Chen and Warren,[1996](https://arxiv.org/html/2607.25373#bib.bib9)\)extends it to general logic programs with negation\. TabledminiKanrenis the descendant of these ideas in the relational host\(Byrd,[2009](https://arxiv.org/html/2607.25373#bib.bib6), Part IV\), and it is the closest neighbour todefrel/bank\. Indeed, both systems memoize a relation on its first call and replay the cached answers on subsequent calls, and both must handle the variable\-shifting issue that arises when canonical bindings are substituted into the caller’s namespace\.

That said, there are two differences, and both are best understood by viewingdefrel/bankas a variant of tabling rather than as an unrelated construct\. The first difference is*which equivalence*the cache preserves\. Classical tabling already operates on equivalence classes of answers, namely syntactic identity up to variable renaming\.defrel/bankswaps this fixed syntactic equivalence for a user\-supplied semantic one \(in our PBE setting, behavior on the example inputs\)\. For PBE, the semantic classes are the desired shape, since two terms with the same input/output behavior are interchangeable for the rest of the search\. The price is that the cached stream no longer reproduces the full syntactic answer set\. This matters for multiplicity\-sensitive applications\. In probabilistic logic programming, for instance, the number of syntactically distinct answers may itself be the quantity of interest, and collapsing by behavior would be unsound there\.

The second difference lies in cache indexing\. TabledminiKanrenkeys each cache by the reified call arguments, so that different call shapes maintain separate caches\. Semantic deduplication, if added, would then have to be repeated per cache\. By contrast,defrel/bankfixes the cache key to the most general call\. The single canonical bank is built with all parameters unbound, and caller\-specific structure is recovered by unification at replay time\. In this light,defrel/bankmay fairly be described as tabling with the argument key fixed to the most general call, plus deduplication by a user\-chosen key\. Indeed, one could approximate it in a classical tabling system by always calling the tabled relation with unbound arguments and constraining the results afterwards\. Whatdefrel/bankadds on top of this recipe is that deduplication happens once, inside the shared cache, rather than downstream of every call site\. These trade\-offs add up to a difference in implementation cost as well: tabledminiKanrenextends the central stream dispatchercase\-infwith a new waiting\-stream variant and rewritestake,bind, andmplusto detect saturation, whereasdefrel/banksits as a library on top of an unmodifiedμ\\upmuKanrencore, requiring only a per\-\(run …\)parameter for the cache\. We see the two designs as complementary, and a future extension may thread a tabling mode throughdefrel/memo, keyed on whether the caller wants every answer or every equivalence class\.

### 7\.4\.Fair Search and Search Strategies

Fair conjunction and disjunction ensure that every answer is eventually emitted, by interleaving the streams from each conjunct or disjunct\. The monad\-transformer view is due to Hinze\(Hinze,[2000](https://arxiv.org/html/2607.25373#bib.bib16)\)and Kiselyov, Shan, Friedman, and Sabry\(Kiselyov et al\.,[2005](https://arxiv.org/html/2607.25373#bib.bib18)\), while the algebraic view of Spivey\(Spivey,[2009](https://arxiv.org/html/2607.25373#bib.bib27)\)characterizes depth\-first, breadth\-first, and iterative\-deepening search as instances of a single search algebra\.miniKanren’s standardmplusimplements interleaved disjunction, and the corresponding fair\-conjunction discipline has been studied specifically forminiKanrenby Lozov and Boulytchev\(Lozov and Boulytchev,[2020](https://arxiv.org/html/2607.25373#bib.bib21)\), whose fair\-conjunction combinator converges independently of conjunct order, and by Lu, Ma, and Friedman\(Lu et al\.,[2019](https://arxiv.org/html/2607.25373#bib.bib22)\), who survey fair\-search strategies in the relational setting\. Rozplokhas and Boulytchev have studied the same question from two further angles: in earlier work\(Rozplokhas and Boulytchev,[2018](https://arxiv.org/html/2607.25373#bib.bib25)\), they introduce a dynamic divergence test that detects potentially non\-terminating conjuncts at run time and reorders them to improve refutational completeness; in later work\(Rozplokhas and Boulytchev,[2022](https://arxiv.org/html/2607.25373#bib.bib26)\), they analyze the scheduling complexity of interleaving search, characterizing when fair disciplines yield asymptotic improvements\. The closestminiKanren\-internal predecessor to a weighted\-stream discipline such as ours is Swords and Friedman’srKanren\(Swords and Friedman,[2013](https://arxiv.org/html/2607.25373#bib.bib28)\), which introduces uniform\-cost guided search insideminiKanren\.

As we have discussed in[Section6](https://arxiv.org/html/2607.25373#S6), the depth\-bias ofdefrel/bankon\(1\+x\)k\(1\+x\)^\{k\}is not a fair\-conjunction failure: the bias is in*which cells*the canonical stream emits first, not in*how pairs of cells*are formed\. The lazy\-ceiling discipline ofdefrel/bank\-wlives in the same design space as these fair\-search efforts, but it is closer to a relational analogue of A\* \(a sorted merge by an admissible heuristic on immature streams\) than to interleaving or uniform\-cost search\.

## 8\.Conclusion and Future Work

We have presented two small library combinators,pruneanddefrel/bank, together with a weighted variantdefrel/bank\-w, that suffice to lift bottom\-up enumeration with observational deduplication intominiKanrenwithout changing the host search discipline\. On a preliminary PBE benchmark of arithmetic and string synthesis targets,defrel/bankis 9–99×\\timesfaster than the depth\-bounded baseline on 6 out of 8 deep arithmetic targets, and the two cases it loses, both in the\(1\+x\)k\(1\+x\)^\{k\}family, are precisely characterized as an enumeration\-order issue that fair conjunction cannot resolve\. We plan a more thorough empirical study for an extended version of this paper\.

We see several promising directions for future work\.

First, the depth bias ofdefrel/bankon\(1\+x\)k\(1\+x\)^\{k\}may be addressed by*iterative deepening over the canonical body*, that is, by forcing the canonical bank to enumerate depthKKfully before any depthK\+1K\+1, perhaps by instrumenting the recursive calls with a depth counter\. We expect that such a discipline would fix the\(1\+x\)k\(1\+x\)^\{k\}bias by construction, without paying the breadth\-first cost thatdefrel/bank\-wpays on wide behavior spaces\.

Second, an obvious optimization is*saturation detection*: stop growing the canonical bank once the prune cache stops expanding\. This caps the cost of unhelpful bank construction, and is also a prerequisite for the tabling\-mode semantics that we have sketched in[Section7](https://arxiv.org/html/2607.25373#S7)\.

Third, we may consider*mixed depth\-first and best\-first strategies*, for example, preferring depth\-first within a sub\-tree and best\-first across sub\-trees\. One way to achieve this is to allowscale\-wto be applied selectively, or to combinemplus\-wandmplusat different recursion boundaries\.

Fourth, it remains to be seen how our combinators interact with the relational\-interpreter recipe\(Byrd et al\.,[2017](https://arxiv.org/html/2607.25373#bib.bib7)\)and, by extension, with systems such as Barliman\(Byrd and Rosenblatt,[2017](https://arxiv.org/html/2607.25373#bib.bib8)\), where the examples are test cases for a program executed by a relational interpreter\. The enumerate\-and\-test recipe that we target in this paper keeps the candidate generator separate from the oracle\. This is what letsground\-keyevaluate candidates with a host\-language interpreter\. It is an open question whether a behavioral prune key can be computed efficiently for candidates*inside*a relational interpreter for a realistic language, e\.g\. by running each candidate on the test inputs as part of the key\. We plan to investigate this\.

Finally, the preliminary benchmark of[Section6](https://arxiv.org/html/2607.25373#S6)should be broadened along the lines set out in the limitations paragraph at the end of that section, and the interaction of our combinators with the existingminiKanrenconstraint stores remains to be studied\.

###### Acknowledgements\.

We thank the anonymous miniKanren 2026 reviewers for their helpful comments, and in particular for the question aboutdefrel/bank\-w’s performance that prompted the pairing\-heap merge of[Section5](https://arxiv.org/html/2607.25373#S5)\.

## References

- \(1\)
- Albarghouthi et al\.\(2013\)Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid\. 2013\.Recursive Program Synthesis\. In*Computer Aided Verification — 25th International Conference \(CAV 2013\)**\(Lecture Notes in Computer Science, Vol\. 8044\)*\. Springer, 934–950\.[doi:10\.1007/978\-3\-642\-39799\-8\_67](https://doi.org/10.1007/978-3-642-39799-8_67)
- Alur et al\.\(2017\)Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa\. 2017\.Scaling Enumerative Program Synthesis via Divide and Conquer\. In*Tools and Algorithms for the Construction and Analysis of Systems — 23rd International Conference \(TACAS 2017\)**\(Lecture Notes in Computer Science, Vol\. 10205\)*\. Springer, 319–336\.[doi:10\.1007/978\-3\-662\-54577\-5\_18](https://doi.org/10.1007/978-3-662-54577-5_18)
- Ballantyne et al\.\(2025\)Michael Ballantyne, Rafaello Sanna, Jason Hemann, William E\. Byrd, and Nada Amin\. 2025\.Multi\-Stage Relational Programming\.*Proceedings of the ACM on Programming Languages*9, PLDI, Article 314 \(2025\)\.[doi:10\.1145/3729314](https://doi.org/10.1145/3729314)
- Barke et al\.\(2020\)Shraddha Barke, Hila Peleg, and Nadia Polikarpova\. 2020\.Just\-in\-Time Learning for Bottom\-Up Enumerative Synthesis\.*Proceedings of the ACM on Programming Languages*4, OOPSLA, Article 227 \(2020\), 29 pages\.[doi:10\.1145/3428295](https://doi.org/10.1145/3428295)
- Byrd \(2009\)William E\. Byrd\. 2009\.*Relational Programming in miniKanren: Techniques, Applications, and Implementations*\.Ph\. D\. Dissertation\. Indiana University, Bloomington, Indiana, USA\.
- Byrd et al\.\(2017\)William E\. Byrd, Michael Ballantyne, Greg Rosenblatt, and Matthew Might\. 2017\.A Unified Approach to Solving Seven Programming Problems \(Functional Pearl\)\.*Proceedings of the ACM on Programming Languages*1, ICFP, Article 8 \(2017\), 26 pages\.[doi:10\.1145/3110252](https://doi.org/10.1145/3110252)
- Byrd and Rosenblatt \(2017\)William E\. Byrd and Greg Rosenblatt\. 2017\.Barliman: Trying the Halting Problem Backwards, Blindfolded\.Software repository\.[https://github\.com/webyrd/Barliman](https://github.com/webyrd/Barliman)
- Chen and Warren \(1996\)Weidong Chen and David S\. Warren\. 1996\.Tabled Evaluation with Delaying for General Logic Programs\.*Journal of the ACM*43, 1 \(1996\), 20–74\.[doi:10\.1145/227595\.227597](https://doi.org/10.1145/227595.227597)
- Chirkov et al\.\(2020\)Artem Chirkov, Gregory Rosenblatt, Matthew Might, and Lisa Zhang\. 2020\.A Relational Interpreter for Synthesizing JavaScript\. In*Proceedings of the 2020 miniKanren and Relational Programming Workshop*\.[https://minikanren\.org/workshop/2020/minikanren\-2020\-paper10\.pdf](https://minikanren.org/workshop/2020/minikanren-2020-paper10.pdf)Co\-located with ICFP 2020\.
- Domoratskiy and Boulytchev \(2024\)Eridan Domoratskiy and Dmitry Boulytchev\. 2024\.A Relational Solver for Constraint\-Based Type Inference\. In*Proceedings of the 2024 miniKanren and Relational Programming Workshop*\.[https://arxiv\.org/abs/2408\.17138](https://arxiv.org/abs/2408.17138)Co\-located with ICFP 2024\.
- Gulwani \(2011\)Sumit Gulwani\. 2011\.Automating String Processing in Spreadsheets Using Input\-Output Examples\. In*Proceedings of the 38th ACM SIGPLAN\-SIGACT Symposium on Principles of Programming Languages \(POPL 2011\)*\. ACM, 317–330\.[doi:10\.1145/1926385\.1926423](https://doi.org/10.1145/1926385.1926423)
- Hart et al\.\(1968\)Peter E\. Hart, Nils J\. Nilsson, and Bertram Raphael\. 1968\.A Formal Basis for the Heuristic Determination of Minimum Cost Paths\.*IEEE Transactions on Systems Science and Cybernetics*4, 2 \(1968\), 100–107\.[doi:10\.1109/TSSC\.1968\.300136](https://doi.org/10.1109/TSSC.1968.300136)
- Hemann and Friedman \(2013\)Jason Hemann and Daniel P\. Friedman\. 2013\.μ\\muKanren: A Minimal Functional Core for Relational Programming\. In*Proceedings of the 2013 Workshop on Scheme and Functional Programming \(Scheme ’13\)*\. Alexandria, Virginia, USA\.
- Hemann and Friedman \(2020\)Jason Hemann and Daniel P\. Friedman\. 2020\.Some Novel miniKanren Synthesis Tasks\. In*Proceedings of the 2020 miniKanren and Relational Programming Workshop*\.[https://minikanren\.org/workshop/2020/minikanren\-2020\-paper9\.pdf](https://minikanren.org/workshop/2020/minikanren-2020-paper9.pdf)Co\-located with ICFP 2020\.
- Hinze \(2000\)Ralf Hinze\. 2000\.Deriving Backtracking Monad Transformers\. In*Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming \(ICFP 2000\)*\. ACM, 186–197\.[doi:10\.1145/351240\.351258](https://doi.org/10.1145/351240.351258)
- Hocquette and Cropper \(2025\)Céline Hocquette and Andrew Cropper\. 2025\.Relational Decomposition for Program Synthesis\. In*Proceedings of the 34th International Joint Conference on Artificial Intelligence \(IJCAI 2025\)*\.[https://arxiv\.org/abs/2408\.12212](https://arxiv.org/abs/2408.12212)
- Kiselyov et al\.\(2005\)Oleg Kiselyov, Chung chieh Shan, Daniel P\. Friedman, and Amr Sabry\. 2005\.Backtracking, Interleaving, and Terminating Monad Transformers \(Functional Pearl\)\. In*Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming \(ICFP 2005\)*\. ACM, 192–203\.[doi:10\.1145/1086365\.1086390](https://doi.org/10.1145/1086365.1086390)
- Kosarev et al\.\(2020\)Dmitri Kosarev, Petr Lozov, and Dmitry Boulytchev\. 2020\.Relational Synthesis for Pattern Matching\. In*Programming Languages and Systems — 18th Asian Symposium \(APLAS 2020\)**\(Lecture Notes in Computer Science, Vol\. 12470\)*\. Springer, 293–310\.[doi:10\.1007/978\-3\-030\-64437\-6\_15](https://doi.org/10.1007/978-3-030-64437-6_15)
- Limperg and From \(2023\)Jannis Limperg and Asta Halkjær From\. 2023\.Aesop: White\-Box Best\-First Proof Search for Lean\. In*Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs \(CPP 2023\)*\. ACM, 253–266\.[doi:10\.1145/3573105\.3575671](https://doi.org/10.1145/3573105.3575671)
- Lozov and Boulytchev \(2020\)Petr Lozov and Dmitry Boulytchev\. 2020\.On Fair Relational Conjunction\. In*Proceedings of the 2020 miniKanren and Relational Programming Workshop*\.[https://minikanren\.org/workshop/2020/minikanren\-2020\-paper1\.pdf](https://minikanren.org/workshop/2020/minikanren-2020-paper1.pdf)Co\-located with ICFP 2020\.
- Lu et al\.\(2019\)Weixi Lu, Tianyi Ma, and Daniel P\. Friedman\. 2019\.Towards a miniKanren with Fair Search Strategies\. In*Proceedings of the 2019 miniKanren and Relational Programming Workshop*\.[https://minikanren\.org/workshop/2019/minikanren19\-final1\.pdf](https://minikanren.org/workshop/2019/minikanren19-final1.pdf)Co\-located with ICFP 2019\.
- Odena et al\.\(2021\)Augustus Odena, Kensen Shi, David Bieber, Rishabh Singh, Charles Sutton, and Pengcheng Yin\. 2021\.BUSTLE: Bottom\-Up Program Synthesis Through Learning\-Guided Exploration\. In*9th International Conference on Learning Representations \(ICLR 2021\)*\.
- Rosenblatt et al\.\(2019\)Greg Rosenblatt, Lisa Zhang, William E\. Byrd, and Matthew Might\. 2019\.First\-Order miniKanren Representation: Great for Tooling and Search\. In*Proceedings of the 2019 miniKanren and Relational Programming Workshop*\.[https://minikanren\.org/workshop/2019/minikanren19\-final2\.pdf](https://minikanren.org/workshop/2019/minikanren19-final2.pdf)Co\-located with ICFP 2019\.
- Rozplokhas and Boulytchev \(2018\)Dmitri Rozplokhas and Dmitry Boulytchev\. 2018\.Improving Refutational Completeness of Relational Search via Divergence Test\. In*Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming \(PPDP 2018\)*\. ACM, Article 5, 13 pages\.[doi:10\.1145/3236950\.3236958](https://doi.org/10.1145/3236950.3236958)
- Rozplokhas and Boulytchev \(2022\)Dmitry Rozplokhas and Dmitry Boulytchev\. 2022\.Scheduling Complexity of Interleaving Search\. In*Functional and Logic Programming — 16th International Symposium \(FLOPS 2022\)**\(Lecture Notes in Computer Science, Vol\. 13215\)*\. Springer, 152–170\.[doi:10\.1007/978\-3\-030\-99461\-7\_9](https://doi.org/10.1007/978-3-030-99461-7_9)
- Spivey \(2009\)J\. M\. Spivey\. 2009\.Algebras for Combinatorial Search\.*Journal of Functional Programming*19, 3–4 \(2009\), 469–487\.[doi:10\.1017/S0956796809007321](https://doi.org/10.1017/S0956796809007321)
- Swords and Friedman \(2013\)Cameron Swords and Daniel P\. Friedman\. 2013\.rKanren: Guided Search in miniKanren\. In*Proceedings of the 2013 Workshop on Scheme and Functional Programming \(Scheme ’13\)*\. Alexandria, Virginia, USA\.[https://www\.schemeworkshop\.org/2013/papers/Swords2013\.pdf](https://www.schemeworkshop.org/2013/papers/Swords2013.pdf)
- Tamaki and Sato \(1986\)Hisao Tamaki and Taisuke Sato\. 1986\.OLD Resolution with Tabulation\. In*Third International Conference on Logic Programming \(ICLP 1986\)**\(Lecture Notes in Computer Science, Vol\. 225\)*\. Springer, 84–98\.[doi:10\.1007/3\-540\-16492\-8\_66](https://doi.org/10.1007/3-540-16492-8_66)
- Wang et al\.\(2018\)Yuepeng Wang, Xinyu Wang, and Isil Dillig\. 2018\.Relational Program Synthesis\.*Proceedings of the ACM on Programming Languages*2, OOPSLA, Article 155 \(2018\), 27 pages\.[doi:10\.1145/3276525](https://doi.org/10.1145/3276525)
- Zhang et al\.\(2018\)Lisa Zhang, Gregory Rosenblatt, Ethan Fetaya, Renjie Liao, William E\. Byrd, Matthew Might, Raquel Urtasun, and Richard Zemel\. 2018\.Neural Guided Constraint Logic Programming for Program Synthesis\. In*Advances in Neural Information Processing Systems 31 \(NeurIPS 2018\)*\. 1741–1751\.[https://arxiv\.org/abs/1809\.02840](https://arxiv.org/abs/1809.02840)

## Appendix ASupplementary Material

In this appendix, we provide the full source code of our prototype implementation, together with the setup instructions and the reproduction steps for the numerical results reported in[Table1](https://arxiv.org/html/2607.25373#S6.T1)\. The prototype is implemented in Racket and consists of twelve modules totalling roughly 2000 lines of code, all of which we list in[SectionA\.5](https://arxiv.org/html/2607.25373#A1.SS5)\. The modules keep the layout of the accompanying repository: the library at the root, the benchmark drivers underbench/, and the shared\-table witness underexamples/\.

### A\.1\.Overview

[Table2](https://arxiv.org/html/2607.25373#A1.T2)provides an overview of the modules in the prototype\. For each module, we indicate the section of the main text that introduces or makes use of it, together with a pointer to the corresponding source listing later in this appendix\.

Table 2\.Modules in the appendix\.
### A\.2\.Setup

The prototype is implemented in pure Racket and runs on Racket 9\.x \(CS\) on macOS, Linux, or Windows; the numbers reported in this paper were produced with Racket 9\.1 \(CS\)\. No external packages are required beyond the Racketbasecollection, and the installation instructions for Racket itself may be found at[https://racket\-lang\.org/](https://racket-lang.org/)\.

Once the source tree is unpacked \(or the repository at[https://github\.com/fizruk/prune\-kanren](https://github.com/fizruk/prune-kanren)is cloned\), the modules may be optionally pre\-compiled for faster benchmark startup with

raco make main\.rkt bench/\*\.rkt examples/\*\.rkt

We also provide the package metadata ininfo\.rkt\([SectionA\.5\.7](https://arxiv.org/html/2607.25373#A1.SS5.SSS7)\), which allows the directory to be picked up byraco pkgas a local Racket package, should the user prefer to install it\.

### A\.3\.Reproducing[Table1](https://arxiv.org/html/2607.25373#S6.T1)

The two row groups of[Table1](https://arxiv.org/html/2607.25373#S6.T1)are produced by two benchmark drivers, which we describe in turn\.

##### Deep arithmetic rows\.

To produce the deep arithmetic rows of[Table1](https://arxiv.org/html/2607.25373#S6.T1), the reader may run

racket bench/deep\-bench\.rkt

from the root of the source tree\. The script runs ten arithmetic targets at depths 2 through 6 against each of the four engines \(bounded,bank,bank\-w,host\-bank\), with per\-target wall\-clock timeouts of 30 seconds for depths≤5\\leq 5and 60 seconds for depth 6\. Each cell is the wall\-clock time of a single run, prefixed by a forced garbage collection; the full source is in[SectionA\.5\.10](https://arxiv.org/html/2607.25373#A1.SS5.SSS10)\. We expect the total runtime to be roughly 3 to 6 minutes on a modern laptop, dominated by the rows on which multiple engines reach the timeout\. Because the methodology is single\-run, the exact ratios may drift slightly across executions; for instance, we have observed thex5x^\{5\}row’s bank\-versus\-boundedratio moving between roughly9×9\\timesand11×11\\timesacross two runs on the same hardware\. The qualitative shape of the table, however, is stable\.

##### String PBE rows\.

To produce the string PBE rows of[Table1](https://arxiv.org/html/2607.25373#S6.T1), the reader may run

racket bench/shallow\-bench\.rkt

from the same directory\. This second driver covers both the arithmetic suite at depths 0–3 \(seven targets, mean per iteration over 50–1000 iterations\) and the string PBE suite at depths 2–3 \(four targets, mean per iteration over 10–200 iterations\)\. For each string target, all four engines are timed;bank\-wis additionally wrapped in a 30 second timeout, since it can be slow on wide string\-behavior spaces\. The full source is in[SectionA\.5\.9](https://arxiv.org/html/2607.25373#A1.SS5.SSS9)\. We expect the total runtime to be roughly 20 to 25 minutes, almost all of it spent on the depth\-3 string target withhost\-bank, which rebuilds the exhaustive depth\-3 string bank on every iteration\.

##### Enumeration indices\.

The \(\#nn\) annotations of[Table1](https://arxiv.org/html/2607.25373#S6.T1)are produced by

racket bench/order\-bench\.rkt

which counts, for each engine and target, the candidates emitted up to and including the first match\. Unlike the timings, these indices are deterministic and machine\-independent\. The run takes roughly 15 minutes, dominated by the cells that reach their timeout while counting\.

##### Decay\-factor experiment\.

The numbers in the decay\-factor discussion of[Section6](https://arxiv.org/html/2607.25373#S6)are produced by

racket bench/decay\-bench\.rkt

which enumerates the first 50 representatives of the weighted arithmetic bank for five decay values, compares the prefixes and their weight\-class structure, and times the\(1\+x\)2\(1\+x\)^\{2\}target under each value\. The run takes well under a minute\.

##### Hardware\.

The numbers reported in this paper were measured on an Apple M4 Pro with 24 GB of memory, running macOS 26\.5 and Racket 9\.1 \(CS\)\.

### A\.4\.Verifying the Shared\-Table Anti\-Pattern of[Section3\.4](https://arxiv.org/html/2607.25373#S3.SS4)

To reproduce, in practice, the completeness failure that we discuss in[Section3\.4](https://arxiv.org/html/2607.25373#S3.SS4), the reader may run

racket examples/shared\-table\-witness\.rkt

from the same directory\. This script defines a variant ofprunethat threads a single deduplication table across all nested calls via a Racket parameter, and runs it side by side with the standard per\-call variant on two PBE targets\. On the easy targetx⋅xx\\cdot x, the shared variant hangs: the depth\-less search loops looking for an alternative ground term with behavior\(4,9,16\)\(4,9,16\), finds none, and never returns\. By contrast, the standard per\-callprunevariant solves the same target immediately\. The full source is given in[SectionA\.5\.8](https://arxiv.org/html/2607.25373#A1.SS5.SSS8); the run should be interrupted with Ctrl\-C once the failure mode is visible\.

### A\.5\.Source Code

The remainder of this appendix lists the full source of each module of the prototype in dependency order\. We begin with theμ\\upmuKanrencore \([SectionA\.5\.1](https://arxiv.org/html/2607.25373#A1.SS5.SSS1)\) and the surface wrappers around it \([SectionA\.5\.2](https://arxiv.org/html/2607.25373#A1.SS5.SSS2)\), which together constitute the substrate that we build upon\. We then list the new combinators introduced in this paper, namelypruneand its helpers \([SectionA\.5\.3](https://arxiv.org/html/2607.25373#A1.SS5.SSS3)\) and the memoization combinatorsdefrel/memo,defrel/bank, anddefrel/bank\-w\([SectionA\.5\.4](https://arxiv.org/html/2607.25373#A1.SS5.SSS4)\)\. Next, we provide the non\-relational host\-language bank used as thehost\-bankengine in[Section6](https://arxiv.org/html/2607.25373#S6)\([SectionA\.5\.5](https://arxiv.org/html/2607.25373#A1.SS5.SSS5)\), followed by the package filesmain\.rktandinfo\.rkt\([SectionsA\.5\.6](https://arxiv.org/html/2607.25373#A1.SS5.SSS6)and[A\.5\.7](https://arxiv.org/html/2607.25373#A1.SS5.SSS7)\)\. Finally, we list the witness for the shared\-table anti\-pattern and the four benchmark drivers that produce the numbers reported in this paper \([SectionsA\.5\.8](https://arxiv.org/html/2607.25373#A1.SS5.SSS8),[A\.5\.9](https://arxiv.org/html/2607.25373#A1.SS5.SSS9),[A\.5\.10](https://arxiv.org/html/2607.25373#A1.SS5.SSS10),[A\.5\.11](https://arxiv.org/html/2607.25373#A1.SS5.SSS11)and[A\.5\.12](https://arxiv.org/html/2607.25373#A1.SS5.SSS12)\)\.

#### A\.5\.1\.microkanren\.rkt

\#langracket/base

;;MinimalmicroKanrencore,afterHemann&Friedman\(2013\)\.

;;Nodisequalityconstraints\.

\(providevarvar?var=?

walkunify

empty\-state

==call/freshdisjconj

mzerounitmplusbind

mplus\-ibind\-i

\(struct\-outlazy\)peek\-weight

lift\-wscale\-wmplus\-wbind\-w\)

;;Logicvariablesare1\-elementvectorsholdinganintegerindex,sotheyare

;;distinguishablefromotherterms\(e\.g\.plainintegers\)byunification\.

\(define\(varc\)\(vectorc\)\)

\(define\(var?x\)\(vector?x\)\)

\(define\(var=?x1x2\)\(=\(vector\-refx10\)\(vector\-refx20\)\)\)

;;Asubstitutionisanassociationlistmappingvariablestoterms\.

\(define\(assppl\)

\(cond

\[\(null?l\)\#f\]

\[\(p\(car\(carl\)\)\)\(carl\)\]

\[else\(asspp\(cdrl\)\)\]\)\)

\(define\(walkus\)

\(let\(\[pr\(and\(var?u\)\(assp\(lambda\(v\)\(var=?uv\)\)s\)\)\]\)

\(ifpr\(walk\(cdrpr\)s\)u\)\)\)

\(define\(ext\-sxvs\)\(cons\(consxv\)s\)\)

\(define\(unifyuvs\)

\(let\(\[u\(walkus\)\]\[v\(walkvs\)\]\)

\(cond

\[\(and\(var?u\)\(var?v\)\(var=?uv\)\)s\]

\[\(var?u\)\(ext\-suvs\)\]

\[\(var?v\)\(ext\-svus\)\]

\[\(and\(pair?u\)\(pair?v\)\)

\(let\(\[s\(unify\(caru\)\(carv\)s\)\]\)

\(ands\(unify\(cdru\)\(cdrv\)s\)\)\)\]

\[else\(and\(eqv?uv\)s\)\]\)\)\)

;;Astateis\(conssubstitutionfresh\-var\-counter\)\.

\(defineempty\-state’\(\(\)\.0\)\)

;;Streams:’\(\)ismzero;\(conss/c$\)isamaturepair;aprocedureofno

;;argumentsisanimmaturestreamusedforinverse\-etadelay\.

\(definemzero’\(\)\)

\(define\(units/c\)\(conss/cmzero\)\)

\(define\(mplus$1$2\)

\(cond

\[\(null?$1\)$2\]

\[\(procedure?$1\)\(lambda\(\)\(mplus$2\($1\)\)\)\]

\[else\(cons\(car$1\)\(mplus\(cdr$1\)$2\)\)\]\)\)

\(define\(bind$g\)

\(cond

\[\(null?$\)mzero\]

\[\(procedure?$\)\(lambda\(\)\(bind\($\)g\)\)\]

\[else\(mplus\(g\(car$\)\)\(bind\(cdr$\)g\)\)\]\)\)

;;Goalsarefunctionsfromastatetoastreamofstates\.

\(define\(==uv\)

\(lambda\(s/c\)

\(let\(\[s\(unifyuv\(cars/c\)\)\]\)

\(ifs\(unit\(conss\(cdrs/c\)\)\)mzero\)\)\)\)

\(define\(call/freshf\)

\(lambda\(s/c\)

\(let\(\[c\(cdrs/c\)\]\)

\(\(f\(varc\)\)\(cons\(cars/c\)\(\+c1\)\)\)\)\)\)

\(define\(disjg1g2\)\(lambda\(s/c\)\(mplus\(g1s/c\)\(g2s/c\)\)\)\)

\(define\(conjg1g2\)\(lambda\(s/c\)\(bind\(g1s/c\)g2\)\)\)

;;—Fairinterleavingvariants—————————————\-

;;

;;Standard‘bind‘forconjisdepth\-biased:whenstream$ismaturewith

;;manystates,‘\(mplus\(g\(car$\)\)\(bind\(cdr$\)g\)\)‘recursivelyyields

;;allof\(g\(car$\)\)’smatureheadbeforethenextstatefrom\(cdr$\)\.

;;Forarecursiverelationlike‘\(conj\(exprl\)\(exprr\)\)‘,thismeans

;;thesearchdrillsdownon\(l=first\-bank\-cell,r=…\)beforeever

;;advancingl,producingastronglydepth\-biasedcanonicalenumeration

;;order\(seebench/deep\-bench\.rktforempiricalimpact\)\.

;;

;;‘mplus\-i‘\(interleave\)and‘bind\-i‘arethefairvariants\.After

;;emittingoneelementfrom$1,mplus\-isuspendstheremainderof$1

;;andswitchesto$2,forcingper\-stepalternationregardlessof

;;whethertheunderlyingstreamsaremature\.

;;

;;References:

;;Kiselyov,Shan,Friedman,Sabry\.”Backtracking,Interleaving,and

;;TerminatingMonadTransformers\.”ICFP2005\.–the‘interleave‘

;;combinatoronMonadPlusfromwhichthisisadapted\.

;;Byrd\.”RelationalProgramminginminiKanren:Techniques,

;;Applications,andImplementations\.”PhDthesis,Indiana

;;University,2009\.–discussionofconjunctionfairnessand

;;interleavingalternatives\.

;;

;;Notetheasymmetryvs‘mplus‘:the‘else‘branchwrapsthecdrina

;;thunksotheconsumer’snextpullwillalternateto$2\.Thiscosts

;;onethunkallocationperelementbutproducesafairdiagonal

;;enumerationof\(l,r\)pairs\.

\(define\(mplus\-i$1$2\)

\(cond

\[\(null?$1\)$2\]

\[\(procedure?$1\)\(lambda\(\)\(mplus\-i$2\($1\)\)\)\]

\[else\(cons\(car$1\)\(lambda\(\)\(mplus\-i$2\(cdr$1\)\)\)\)\]\)\)

\(define\(bind\-i$g\)

\(cond

\[\(null?$\)mzero\]

\[\(procedure?$\)\(lambda\(\)\(bind\-i\($\)g\)\)\]

\[else\(mplus\-i\(g\(car$\)\)\(bind\-i\(cdr$\)g\)\)\]\)\)

;;—Weightedstreams\(depth\-decayedbest\-first\)———————\-

;;

;;Aweightedstreamisoneof:

;;’\(\)–empty

;;\(cons\(consweightstate\)rest\)–matureheadwithexplicitweight

;;\(lazyweightthunk\)–immature,withaknownupperbound

;;onweightsanyforcedcellcouldhave

;;

;;Carryingaweightceilingonimmaturestreamsisthecriticaldesign

;;choice:‘mplus\-w‘candeterminewhichsidecouldpossiblyemita

;;higher\-weightcell\*withoutforcing\*eitherside\.Thisavoidsthe

;;classic”peekrequiresforce”trapthat,inarecursivememoized

;;bank,wouldcauseforcingofamemo\-thunkwhileit’sstillbeing

;;computed\(cycle/infiniterecursion\)\.

;;

;;Inspiredbybest\-firstproofsearchinLean4’saesoptactic

;;\(Limperg&From,”Aesop:White\-BoxBest\-FirstProofSearchfor

;;Lean,”CPP2023\),andbyadmissibleheuristicsinA\*\-stylesearch

;;\(Hart,Nilsson,Raphael1968\)–‘lazy\-weight‘playstheroleofan

;;admissibleupperboundonwhatthelazycanyield\.

;;

;;Weightpropagation:

;;\-Zzz\-wwrapsagoalas‘\(lazy1\.0…\)‘–conservativedefault\.

;;\-scale\-wmultipliesthelazy’sceiling\(andeachmaturecell’s

;;weight\)by‘factor‘\.

;;\-bind\-won‘\(lazyw…\)‘produces‘\(lazyw…\)‘–assumesthe

;;appliedgoal’soutputceilingis<=1\.0\(trueforunweighted

;;goals;weightedgoalsareconservativelyover\-estimated\)\.

;;\-mplus\-woftwolaziesreturnsalazywithceiling=maxofthe

;;twoceilings\(anycellemittedcomesfromoneofthem\)\.

;;\-lift\-wofanunweightedprocedurestreamwrapsas‘\(lazy1\.0…\)‘\.

\(structlazy\(weightthunk\)\#:transparent\)

\(define\(peek\-weight$\)

\(cond

\[\(null?$\)\-inf\.0\]

\[\(lazy?$\)\(lazy\-weight$\)\]

\[else\(caar$\)\]\)\)

\(define\(weighted\-cell?c\)

\(and\(pair?c\)\(pair?\(carc\)\)\(number?\(caarc\)\)\)\)

;;lift\-w:promoteanystreamtoweightedform\.

;;\-Alreadyweighted\(maturewith\(weight\.state\)cell,orlazy\)\-\>unchanged\.

;;\-Unweightedprocedure\-\>wrapaslazywithceiling1\.0\.

;;\-Unweightedmaturestream\-\>tageachcellwithweight1\.0\.

\(define\(lift\-w$\)

\(cond

\[\(null?$\)’\(\)\]

\[\(lazy?$\)$\]

\[\(procedure?$\)\(lazy1\.0\(lambda\(\)\(lift\-w\($\)\)\)\)\]

\[\(weighted\-cell?$\)$\]

\[else\(cons\(cons1\.0\(car$\)\)\(lift\-w\(cdr$\)\)\)\]\)\)

\(define\(scale\-wfactor$\)

\(cond

\[\(null?$\)’\(\)\]

\[\(lazy?$\)\(lazy\(\*factor\(lazy\-weight$\)\)

\(lambda\(\)\(scale\-wfactor\(\(lazy\-thunk$\)\)\)\)\)\]

\[else\(cons\(cons\(\*factor\(caar$\)\)\(cdar$\)\)

\(scale\-wfactor\(cdr$\)\)\)\]\)\)

;;mplus\-w:emitcellsindescendingweightorder\.Usespeek\-weightto

;;decidewhichsidewinswithoutforcingtheloser\.Onlyforcesalazy

;;whenitsceilingindicatesitmightstillproduceawinningcell\.

;;

;;Amergeofmanyalternatives\(oneperpendingdisjunctorbind

;;cell\)iskeptinapairingmax\-heapkeyedbypeek\-weight,rather

;;thaninanestofbinarymerges:withabinarynest,emittingthe

;;nextcellcostsO\(\#alternatives\),whichdominatestheruntimeof

;;best\-firstsearch\(eachpullre\-traversesthewholefrontierof

;;suspendedalternatives\)\.Theheapishiddenbehindthepublic

;;streaminterfaceas‘lazy\-merge‘,asubtypeof‘lazy‘that

;;additionallycarriestheheap,sothatnestedmplus\-wcallsmeld

;;heapsinO\(1\)whileeveryotherconsumertreatsthemergeasan

;;ordinaryimmaturestream\.

\(structlazy\-mergelazy\(heap\)\#:transparent\)

;;Pairingmax\-heapof\(non\-null,non\-merge\)streamskeyedby

;;peek\-weight\.Aheapis\#f\(empty\)or\(constop\-streamchildren\),

;;wherechildrenisalistofheaps\.

\(define\(heap\-meldh1h2\)

\(cond

\[\(noth1\)h2\]

\[\(noth2\)h1\]

\[\(\>=\(peek\-weight\(carh1\)\)\(peek\-weight\(carh2\)\)\)

\(cons\(carh1\)\(consh2\(cdrh1\)\)\)\]

\[else\(cons\(carh2\)\(consh1\(cdrh2\)\)\)\]\)\)

\(define\(heap\-meld\-pairshs\)

\(cond

\[\(null?hs\)\#f\]

\[\(null?\(cdrhs\)\)\(carhs\)\]

\[else\(heap\-meld\(heap\-meld\(carhs\)\(cadrhs\)\)

\(heap\-meld\-pairs\(cddrhs\)\)\)\]\)\)

;;heap\-add:insertastream,flatteningnestedmergesbymelding

;;theirheapsdirectly\.

\(define\(heap\-addh$\)

\(cond

\[\(null?$\)h\]

\[\(lazy\-merge?$\)\(heap\-meldh\(lazy\-merge\-heap$\)\)\]

\[else\(heap\-meldh\(cons$’\(\)\)\)\]\)\)

;;heap\-\>stream:exposeaheapasapublicweightedstream\.Ifthe

;;topismature,emititsheadcellandre\-insertitstail\.Ifthe

;;topisimmature,thewholemergeisimmaturewiththetop’s

;;ceiling;forcingitforcesexactlyonestepofthetop\.

\(define\(heap\-\>streamh\)

\(cond

\[\(noth\)’\(\)\]

\[else

\(let\(\[top\(carh\)\]\)

\(cond

\[\(lazy?top\)

\(lazy\-merge\(lazy\-weighttop\)

\(lambda\(\)

\(let\(\[rest\(heap\-meld\-pairs\(cdrh\)\)\]\)

\(heap\-\>stream\(heap\-addrest\(\(lazy\-thunktop\)\)\)\)\)\)

h\)\]

\[else

\(let\(\[rest\(heap\-meld\-pairs\(cdrh\)\)\]\)

\(cons\(cartop\)\(heap\-\>stream\(heap\-addrest\(cdrtop\)\)\)\)\)\]\)\)\]\)\)

\(define\(mplus\-w$1$2\)

\(heap\-\>stream\(heap\-add\(heap\-add\#f$1\)$2\)\)\)

;;bind\-w:foreach\(w,state\)in$,applyg,scalebyw\.Theoutput

;;ceilingisconservatively\(lazy\-weight$\)–assumesg’soutputis

;;boundedby1\.0\.\-wgoalsthatproducesmalleroutputsimplyemit

;;cellswithlowerweight;theystillsortcorrectlybecauseofhow

;;scale\-wdecaypropagates\.

\(define\(bind\-w$g\)

\(cond

\[\(null?$\)’\(\)\]

\[\(lazy?$\)\(lazy\(lazy\-weight$\)

\(lambda\(\)\(bind\-w\(\(lazy\-thunk$\)\)g\)\)\)\]

\[else

\(let\(\[w\(caar$\)\]\[s\(cdar$\)\]\)

\(mplus\-w\(scale\-ww\(lift\-w\(gs\)\)\)

\(bind\-w\(cdr$\)g\)\)\)\]\)\)

#### A\.5\.2\.wrappers\.rkt

\#langracket/base

;;miniKanren\-stylewrappersaroundthemicroKanrencore:variadic

;;conde/fresh,run/run\*,plusthestreamdriverandreifier\.

;;Followssection4ofHemann&Friedman\(2013\)\.

\(require\(for\-syntaxracket/base\)

”microkanren\.rkt”\)

\(provideZzzconj\+disj\+condefresh

conj\-iconj\-i\+conde\-ifresh\-i

Zzz\-wconj\-wconj\-w\+disj\-wdisj\-w\+conde\-wfresh\-w

runrun\*run\-wrun\*\-w

pulltaketake\-allpull\-wtake\-wtake\-all\-w

walk\*

current\-memo\)

;;Memoizationcachefordefrel/memo,populatedper‘run‘invocation\.

;;\#fmeans”nomemosessionactive”–memoizedrelationsfallbackto

;;runningtheirbodynormally\.

\(definecurrent\-memo\(make\-parameter\#f\)\)

;;Inverse\-etadelay:wrapsagoalsothatitsstreamisathunk,which

;;letsdisj\+/conj\+recurinto\(potentiallynonterminating\)goalssafely\.

\(define\-syntaxZzz

\(syntax\-rules\(\)

\[\(\_g\)\(lambda\(s/c\)\(lambda\(\)\(gs/c\)\)\)\]\)\)

\(define\-syntaxconj\+

\(syntax\-rules\(\)

\[\(\_g\)\(Zzzg\)\]

\[\(\_g0g…\)\(conj\(Zzzg0\)\(conj\+g…\)\)\]\)\)

\(define\-syntaxdisj\+

\(syntax\-rules\(\)

\[\(\_g\)\(Zzzg\)\]

\[\(\_g0g…\)\(disj\(Zzzg0\)\(disj\+g…\)\)\]\)\)

\(define\-syntaxconde

\(syntax\-rules\(\)

\[\(\_\(g0g…\)…\)\(disj\+\(conj\+g0g…\)…\)\]\)\)

\(define\-syntaxfresh

\(syntax\-rules\(\)

\[\(\_\(\)g0g…\)\(conj\+g0g…\)\]

\[\(\_\(x0x…\)g0g…\)

\(call/fresh\(lambda\(x0\)\(fresh\(x…\)g0g…\)\)\)\]\)\)

;;—Fairinterleavingvariants\(Kiselyov\-Shan\-Friedman\-Sabry2005\)—

;;

;;conj\-i:likeconjbutusesbind\-iinsteadofbind\.

;;conj\-i\+:variadic,likeconj\+buteachcompositionisinterleaving\.

;;fresh\-i:likefreshbutcombinesitsbodywithconj\-i\+\.

;;conde\-i:likecondebutusesconj\-i\+insideeachclause\.

;;

;;Usethesewhenconj’sdepthbiashurts–typicallywhenthebody

;;hasindependentrecursivesubgoalslike‘\(rell\)\(relr\)‘andyou

;;wantfaircoverageof\(l,r\)pairsalongantidiagonalsratherthan

;;anested\-loopenumeration\.Thecostisoneextrathunkallocation

;;peremittedstate\.

\(define\(conj\-ig1g2\)\(lambda\(s/c\)\(bind\-i\(g1s/c\)g2\)\)\)

\(define\-syntaxconj\-i\+

\(syntax\-rules\(\)

\[\(\_g\)\(Zzzg\)\]

\[\(\_g0g…\)\(conj\-i\(Zzzg0\)\(conj\-i\+g…\)\)\]\)\)

\(define\-syntaxconde\-i

\(syntax\-rules\(\)

\[\(\_\(g0g…\)…\)\(disj\+\(conj\-i\+g0g…\)…\)\]\)\)

\(define\-syntaxfresh\-i

\(syntax\-rules\(\)

\[\(\_\(\)g0g…\)\(conj\-i\+g0g…\)\]

\[\(\_\(x0x…\)g0g…\)

\(call/fresh\(lambda\(x0\)\(fresh\-i\(x…\)g0g…\)\)\)\]\)\)

;;—Weighted\(best\-first\)combinators——————————–

;;

;;Theseoperateonweightedstreams\(seemicrokanren\.rkt\)\.Eachgoal’s

;;outputisauto\-lifted:==andotherunweightedgoalsproduce

;;weight\-1cellswhenconsumedbya\-wcombinator\.Goalsreturnedby

;;defrel/bank\-walreadyproduceweightedstreamsandpassthrough

;;lift\-wunchanged\.

;;Zzz\-wwrapsagoalsoitsapplicationproducesanimmatureweighted

;;streamwitha1\.0weightceiling\.Theceilingisconservative–

;;a\-wgoalwhoseunderlyingcellsarescaleddown\(e\.g\.bydecay\)

;;willreportloweractualcellweightsonceforced,butthelazy’s

;;advertisedceilingstaysat1\.0unlesswehavestaticinfotodo

;;better\.scale\-wcantightentheceilingatrelationboundaries\.

\(define\-syntaxZzz\-w

\(syntax\-rules\(\)

\[\(\_g\)\(lambda\(s/c\)\(lazy1\.0\(lambda\(\)\(lift\-w\(gs/c\)\)\)\)\)\]\)\)

\(define\(conj\-wg1g2\)

\(lambda\(s/c\)\(bind\-w\(lift\-w\(g1s/c\)\)g2\)\)\)

\(define\(disj\-wg1g2\)

\(lambda\(s/c\)\(mplus\-w\(lift\-w\(g1s/c\)\)\(lift\-w\(g2s/c\)\)\)\)\)

\(define\-syntaxconj\-w\+

\(syntax\-rules\(\)

\[\(\_g\)\(Zzz\-wg\)\]

\[\(\_g0g…\)\(conj\-w\(Zzz\-wg0\)\(conj\-w\+g…\)\)\]\)\)

\(define\-syntaxdisj\-w\+

\(syntax\-rules\(\)

\[\(\_g\)\(Zzz\-wg\)\]

\[\(\_g0g…\)\(disj\-w\(Zzz\-wg0\)\(disj\-w\+g…\)\)\]\)\)

\(define\-syntaxconde\-w

\(syntax\-rules\(\)

\[\(\_\(g0g…\)…\)\(disj\-w\+\(conj\-w\+g0g…\)…\)\]\)\)

\(define\-syntaxfresh\-w

\(syntax\-rules\(\)

\[\(\_\(\)g0g…\)\(conj\-w\+g0g…\)\]

\[\(\_\(x0x…\)g0g…\)

\(call/fresh\(lambda\(x0\)\(fresh\-w\(x…\)g0g…\)\)\)\]\)\)

;;Weightedreify:extractstatefromweightedcellbeforereifying\.

\(define\(reify\-1st/wcell\)

\(let\*\(\[s/c\(cdrcell\)\]

\[v\(walk\*\(var0\)\(cars/c\)\)\]\)

\(walk\*v\(reify\-sv’\(\)\)\)\)\)

;;pull/takeforweightedstreams:lazystructs\(notprocedures\)signal

;;immature;forcevialazy\-thunk\.

\(define\(pull\-w$\)

\(cond

\[\(lazy?$\)\(pull\-w\(\(lazy\-thunk$\)\)\)\]

\[else$\]\)\)

\(define\(take\-wn$\)

\(if\(zero?n\)’\(\)

\(let\(\[$\(pull\-w$\)\]\)

\(if\(null?$\)’\(\)

\(cons\(car$\)\(take\-w\(\-n1\)\(cdr$\)\)\)\)\)\)\)

\(define\(take\-all\-w$\)

\(let\(\[$\(pull\-w$\)\]\)

\(if\(null?$\)’\(\)

\(cons\(car$\)\(take\-all\-w\(cdr$\)\)\)\)\)\)

\(define\-syntaxrun\-w

\(syntax\-rules\(\)

\[\(\_n\(q\)g0g…\)

\(parameterize\(\[current\-memo\(make\-hash\)\]\)

\(mapreify\-1st/w\(take\-wn\(\(fresh\-w\(q\)g0g…\)empty\-state\)\)\)\)\]

\[\(\_n\(x0x…\)g0g…\)

\(run\-wn\(q\)\(fresh\-w\(x0x…\)\(==q\(listx0x…\)\)g0g…\)\)\]\)\)

\(define\-syntaxrun\*\-w

\(syntax\-rules\(\)

\[\(\_\(q\)g0g…\)

\(parameterize\(\[current\-memo\(make\-hash\)\]\)

\(mapreify\-1st/w\(take\-all\-w\(\(fresh\-w\(q\)g0g…\)empty\-state\)\)\)\)\]

\[\(\_\(x0x…\)g0g…\)

\(run\*\-w\(q\)\(fresh\-w\(x0x…\)\(==q\(listx0x…\)\)g0g…\)\)\]\)\)

;;—streamdriver—

\(define\(pull$\)\(if\(procedure?$\)\(pull\($\)\)$\)\)

\(define\(take\-all$\)

\(let\(\[$\(pull$\)\]\)

\(if\(null?$\)’\(\)

\(cons\(car$\)\(take\-all\(cdr$\)\)\)\)\)\)

\(define\(taken$\)

\(if\(zero?n\)’\(\)

\(let\(\[$\(pull$\)\]\)

\(if\(null?$\)’\(\)

\(cons\(car$\)\(take\(\-n1\)\(cdr$\)\)\)\)\)\)\)

;;—reification—

\(define\(walk\*vs\)

\(let\(\[v\(walkvs\)\]\)

\(cond

\[\(var?v\)v\]

\[\(pair?v\)\(cons\(walk\*\(carv\)s\)\(walk\*\(cdrv\)s\)\)\]

\[elsev\]\)\)\)

\(define\(reify\-namen\)

\(string\-\>symbol\(string\-append”\_\.”\(number\-\>stringn\)\)\)\)

\(define\(reify\-svs\)

\(let\(\[v\(walkvs\)\]\)

\(cond

\[\(var?v\)\(cons\(consv\(reify\-name\(lengths\)\)\)s\)\]

\[\(pair?v\)\(reify\-s\(cdrv\)\(reify\-s\(carv\)s\)\)\]

\[elses\]\)\)\)

;;Thefirstfreshvariableintroducedfromempty\-statehasindex0;

;;therunmacroarrangesforthatvariabletoholdthequeryvalue\.

\(define\(reify\-1sts/c\)

\(let\(\[v\(walk\*\(var0\)\(cars/c\)\)\]\)

\(walk\*v\(reify\-sv’\(\)\)\)\)\)

;;—run/run\*—

;;

;;Single\-varformreturnsreifiedvaluesdirectly\.

;;Multi\-varformbundlesthequeryvarsintoalistunderahygienicq\.

\(define\-syntaxrun

\(syntax\-rules\(\)

\[\(\_n\(q\)g0g…\)

\(parameterize\(\[current\-memo\(make\-hash\)\]\)

\(mapreify\-1st\(taken\(\(fresh\(q\)g0g…\)empty\-state\)\)\)\)\]

\[\(\_n\(x0x…\)g0g…\)

\(runn\(q\)\(fresh\(x0x…\)\(==q\(listx0x…\)\)g0g…\)\)\]\)\)

\(define\-syntaxrun\*

\(syntax\-rules\(\)

\[\(\_\(q\)g0g…\)

\(parameterize\(\[current\-memo\(make\-hash\)\]\)

\(mapreify\-1st\(take\-all\(\(fresh\(q\)g0g…\)empty\-state\)\)\)\)\]

\[\(\_\(x0x…\)g0g…\)

\(run\*\(q\)\(fresh\(x0x…\)\(==q\(listx0x…\)\)g0g…\)\)\]\)\)

#### A\.5\.3\.prune\.rkt

\#langracket/base

;;Pruningcombinator\.

;;

;;\(prunekeyg\)wrapsagoalgandfiltersitsanswerstreamsothatat

;;mostonestateisemittedperdistinctvalueof\(keys/c\)\.Thekey

;;functionissuppliedpercall,sotheequivalenceusedtopruneis

;;chosenlocally–e\.g\.”behaviorontheinputexamples”forPBE

;;synthesis,or”shapemoduloalpha\-renaming”elsewhere\.

;;

;;Thededuptableislocaltooneprunecallandsharedacrossthe

;;stream’slazythunks\(theclosurecapturesit\),sodedupstate

;;survivestheinverse\-etadelayusedbymplus/bind\.

;;

;;Thissketchusesequal?\-keyedhashing;anefficientversionwould

;;hash\-consthekeyvaluesproducedbytheuser’ssemanticfunction\.

\(require”microkanren\.rkt”

”wrappers\.rkt”\)

\(providepruneskip\-prune

ground?ground\-keywhen\-ground

prune\-w\)

;;Sentinelakeyfunctionmayreturntomean”don’tdedupyet”–

;;typicallybecausetherelevantvariablesarestillfresh\.

\(defineskip\-prune’skip\-prune\)

;;prune:\(state\-\>any\)goal\-\>goal

\(define\(prunekeyg\)

\(lambda\(s/c\)

\(prune\-streamkey\(make\-hash\)\(gs/c\)\)\)\)

\(define\(prune\-streamkeyseen$\)

\(cond

\[\(null?$\)’\(\)\]

\[\(procedure?$\)\(lambda\(\)\(prune\-streamkeyseen\($\)\)\)\]

\[else

\(let\*\(\[s/c\(car$\)\]

\[k\(keys/c\)\]\)

\(cond

\[\(eq?kskip\-prune\)

\(conss/c\(prune\-streamkeyseen\(cdr$\)\)\)\]

\[\(hash\-has\-key?seenk\)

\(prune\-streamkeyseen\(cdr$\)\)\]

\[else

\(hash\-set\!seenk\#t\)

\(conss/c\(prune\-streamkeyseen\(cdr$\)\)\)\]\)\)\]\)\)

;;—key\-buildinghelpers—

;;Atermisgroundifitcontainsnologicvariables\.

\(define\(ground?t\)

\(cond

\[\(var?t\)\#f\]

\[\(pair?t\)\(and\(ground?\(cart\)\)\(ground?\(cdrt\)\)\)\]

\[else\#t\]\)\)

;;ground\-key:variable\(term\-\>any\)\-\>\(state\-\>any\)

;;

;;Liftsahostfunctionontermsintoaprunekeyonstates:walks‘v‘

;;inthecurrentsubstitutionand,iftheresultisground,applies‘f‘

;;toit\.Returns‘skip\-prune‘when‘v‘hasn’tgroundoutyet,sothose

;;statespassthrough‘prune‘unfiltered\.

;;

;;TypicaluseinPBEsynthesis:

;;\(prune\(ground\-keye\(lambda\(t\)\(map\(eval\-ont\)inputs\)\)\)

;;\(expredepth\)\)

\(define\(ground\-keyvf\)

\(lambda\(s/c\)

\(let\(\[t\(walk\*v\(cars/c\)\)\]\)

\(if\(ground?t\)

\(ft\)

skip\-prune\)\)\)\)

;;when\-ground:variable\(term\-\>boolean\)\-\>goal

;;

;;Agoalthatsucceedswhen‘v‘walkstoagroundtermsatisfying

;;‘pred‘,andfailsotherwise\(includingwhen‘v‘isstillnon\-ground\)\.

;;Usefulasthefinal”acceptthiscandidate”stageofasynthesisrun\.

\(define\(when\-groundvpred\)

\(lambda\(s/c\)

\(let\(\[t\(walk\*v\(cars/c\)\)\]\)

\(if\(and\(ground?t\)\(predt\)\)

\(units/c\)

’\(\)\)\)\)\)

;;—prune\-w:pruneforweightedstreams——————————

\(define\(prune\-wkeyg\)

\(lambda\(s/c\)

\(prune\-stream\-wkey\(make\-hash\)\(lift\-w\(gs/c\)\)\)\)\)

\(define\(prune\-stream\-wkeyseen$\)

\(cond

\[\(null?$\)’\(\)\]

\[\(lazy?$\)\(lazy\(lazy\-weight$\)

\(lambda\(\)\(prune\-stream\-wkeyseen\(\(lazy\-thunk$\)\)\)\)\)\]

\[else

\(let\*\(\[cell\(car$\)\]\[s\(cdrcell\)\]\[k\(keys\)\]\)

\(cond

\[\(eq?kskip\-prune\)

\(conscell\(prune\-stream\-wkeyseen\(cdr$\)\)\)\]

\[\(hash\-has\-key?seenk\)

\(prune\-stream\-wkeyseen\(cdr$\)\)\]

\[else

\(hash\-set\!seenk\#t\)

\(conscell\(prune\-stream\-wkeyseen\(cdr$\)\)\)\]\)\)\]\)\)

#### A\.5\.4\.memo\.rkt

\#langracket/base

;;defrel/memo:defineapurerelationwhosecanonicalanswerstreamis

;;computedonceper‘run‘andreplayedagainsteachcaller’sarguments\.

;;

;;Thebodyofamemoizedrelationisrunwithcanonicalinputvars

;;\(var0\),\(var1\),…,\(varN\-1\)\(N=arity\),startingcounterN\.

;;Theresultingstreamofstates\(lazy\)isstoredintheper\-runcache\.

;;Eachsubsequentcallreplaysthiscanonicalstreamagainstthe

;;caller’sargs:

;;\-canonicalinputvarsarerenamedtothecaller’sactualargs;

;;\-canonicalinternalfreshvars\(idx\>=N\)areshiftedbythe

;;caller’scountertoallocatefreshvarsinthecaller’snamespace;

;;\-therenamedbindingsareunifiedintothecaller’ssubstitution\.

;;

;;RecursivecallsinsidethebodyZzz\-suspend,sobythetimetheyfire

;;thecacheentryisinplace\.Thelazythunksofthecanonicalstream

;;arememoized\(‘memo\-thunk‘\)soforcinghappensatmostoncepercell

;;acrossallreplays\.

\(require”microkanren\.rkt”

”wrappers\.rkt”

”prune\.rkt”\)

\(providedefrel/memodefrel/bankdefrel/bank\-wwith\-memo\-session\)

\(define\-syntax\-rule\(with\-memo\-sessionbody…\)

\(parameterize\(\[current\-memo\(make\-hash\)\]\)body…\)\)

;;—thunk\+streammemoization—

\(define\(memo\-thunkf\)

\(let\(\[result\#f\]\[done?\#f\]\)

\(lambda\(\)

\(unlessdone?

\(set\!result\(f\)\)

\(set\!done?\#t\)\)

result\)\)\)

\(define\(memo\-streams\)

\(cond

\[\(null?s\)’\(\)\]

;;Weighted:preservethelazy’sweightceiling,butmemoizethe

;;forcingofitsthunk\.Eachlazygetsitsownmemo\-thunk;multiple

;;replayssharingthesamecanonicalbankallhitthecache\.

\[\(lazy?s\)\(lazy\(lazy\-weights\)

\(memo\-thunk\(lambda\(\)\(memo\-stream\(\(lazy\-thunks\)\)\)\)\)\)\]

\[\(procedure?s\)\(memo\-thunk\(lambda\(\)\(memo\-stream\(s\)\)\)\)\]

\[else\(cons\(cars\)\(memo\-stream\(cdrs\)\)\)\]\)\)

;;—replay—

\(define\(replay\-statecanonical\-statecaller\-stateargs\-vecnum\-args\)

\(definecanonical\-subst\(carcanonical\-state\)\)

\(definecanonical\-counter\(cdrcanonical\-state\)\)

\(definecaller\-subst\(carcaller\-state\)\)

\(definecaller\-counter\(cdrcaller\-state\)\)

\(defineshift\-internal\(\-caller\-counternum\-args\)\)

\(definenew\-counter\(\+caller\-counter\(\-canonical\-counternum\-args\)\)\)

\(define\(renamet\)

\(cond

\[\(var?t\)

\(let\(\[idx\(vector\-reft0\)\]\)

\(cond

\[\(<idxnum\-args\)\(vector\-refargs\-vecidx\)\]

\[else\(var\(\+idxshift\-internal\)\)\]\)\)\]

\[\(pair?t\)\(cons\(rename\(cart\)\)\(rename\(cdrt\)\)\)\]

\[elset\]\)\)

\(letloop\(\[i0\]\[scaller\-subst\]\)

\(cond

\[\(=inum\-args\)\(conssnew\-counter\)\]

\[else

\(let\*\(\[canonical\-value\(walk\*\(vari\)canonical\-subst\)\]

\[renamed\(renamecanonical\-value\)\]

\[caller\-arg\(vector\-refargs\-veci\)\]

\[s\*\(unifycaller\-argrenameds\)\]\)

\(ifs\*\(loop\(\+i1\)s\*\)\#f\)\)\]\)\)\)

\(define\(replay\-streamcanonicalcaller\-stateargs\-vecnum\-args\)

\(cond

\[\(null?canonical\)’\(\)\]

\[\(procedure?canonical\)

;;Collapseachainofimmaturecanonicalthunksintoasingle

;;replay\-thunkforce–whentheconsumerasksforthenextstate,

;;wekeepforcinguntilwegetaconcretecons\(ornull\),instead

;;ofproducinganewreplay\-thunkforeachlayerofcanonical

;;laziness\.Thisiswhat‘pull‘doesontheconsumerside;doing

;;itherecutsthethunk\-forcecountfrom~330kto~3kforthe

;;PBEbenchandbringsdefrel/banktowithin1\.5xofthe

;;depth\-boundedbaseline\.

\(lambda\(\)

\(letloop\(\[c\(canonical\)\]\)

\(cond

\[\(null?c\)’\(\)\]

\[\(procedure?c\)\(loop\(c\)\)\]

\[else

\(let\(\[new\(replay\-state\(carc\)caller\-stateargs\-vecnum\-args\)\]\)

\(cond

\[new\(consnew\(replay\-stream\(cdrc\)caller\-stateargs\-vecnum\-args\)\)\]

\[else\(replay\-stream\(cdrc\)caller\-stateargs\-vecnum\-args\)\]\)\)\]\)\)\)\]

\[else

\(let\(\[new\(replay\-state\(carcanonical\)caller\-stateargs\-vecnum\-args\)\]\)

\(cond

\[new

\(consnew

\(replay\-stream\(cdrcanonical\)caller\-stateargs\-vecnum\-args\)\)\]

\[else

\(replay\-stream\(cdrcanonical\)caller\-stateargs\-vecnum\-args\)\]\)\)\]\)\)

;;—init\+memo\-call—

\(define\(init\-cellcacherel\-tagbody\-fnnum\-args\)

\(definecanonical\-vars\(for/list\(\[i\(in\-rangenum\-args\)\]\)\(vari\)\)\)

\(definecanonical\-state\(cons’\(\)num\-args\)\)

\(defineb\(box\#f\)\)

\(hash\-set\!cacherel\-tagb\)

\(defines\(\(applybody\-fncanonical\-vars\)canonical\-state\)\)

\(set\-box\!b\(memo\-streams\)\)

b\)

\(define\(make\-memo\-relnum\-argsbody\-fn\)

\(definerel\-tag\(box\#f\)\)

\(lambdaactual\-args

\(let\(\[args\-vec\(list\-\>vectoractual\-args\)\]\)

\(lambda\(s/c\)

\(let\(\[cache\(current\-memo\)\]\)

\(cond

\[cache

\(let\(\[b\(or\(hash\-refcacherel\-tag\#f\)

\(init\-cellcacherel\-tagbody\-fnnum\-args\)\)\]\)

\(replay\-stream\(unboxb\)s/cargs\-vecnum\-args\)\)\]

\[else

\(\(applybody\-fnactual\-args\)s/c\)\]\)\)\)\)\)\)

\(define\-syntaxdefrel/memo

\(syntax\-rules\(\)

\[\(\_\(namex…\)body…\)

\(definename

\(make\-memo\-rel\(length’\(x…\)\)

\(lambda\(x…\)\(conj\+body…\)\)\)\)\]\)\)

;;defrel/bank:likedefrel/memobutadditionallyprunesthecanonical

;;streambythesuppliedkey\.Prunerunsonceatcanonical\-stream

;;constructiontime;replaysalreadyseeonlyonerepresentativeper

;;key\.Useshape:

;;

;;\(defrel/bank\(relx…\)\#:prunekey\-exprbody…\)

;;

;;key\-exprisevaluatedinthescopeoftherelationparameters,soit

;;canreferencethem\(e\.g\.\(ground\-keyx\(lambda\(t\)…\)\)\)\.The

;;canonicalrunbindstheparametersto\(var0\),\(var1\),…\.

\(define\(init\-bank\-cellcacherel\-tagbody\-fnkey\-fnnum\-args\)

\(definecanonical\-vars\(for/list\(\[i\(in\-rangenum\-args\)\]\)\(vari\)\)\)

\(definecanonical\-state\(cons’\(\)num\-args\)\)

\(defineb\(box\#f\)\)

\(hash\-set\!cacherel\-tagb\)

\(definekey\(applykey\-fncanonical\-vars\)\)

\(definebody\-goal\(applybody\-fncanonical\-vars\)\)

\(defines\(\(prunekeybody\-goal\)canonical\-state\)\)

\(set\-box\!b\(memo\-streams\)\)

b\)

\(define\(make\-bank\-relnum\-argsbody\-fnkey\-fn\)

\(definerel\-tag\(box\#f\)\)

\(lambdaactual\-args

\(let\(\[args\-vec\(list\-\>vectoractual\-args\)\]\)

\(lambda\(s/c\)

\(let\(\[cache\(current\-memo\)\]\)

\(cond

\[cache

\(let\(\[b\(or\(hash\-refcacherel\-tag\#f\)

\(init\-bank\-cellcacherel\-tagbody\-fnkey\-fnnum\-args\)\)\]\)

\(replay\-stream\(unboxb\)s/cargs\-vecnum\-args\)\)\]

\[else

;;Nomemosession:fallbacktopruningper\-call\.

\(let\(\[k\(applykey\-fnactual\-args\)\]

\[g\(applybody\-fnactual\-args\)\]\)

\(\(prunekg\)s/c\)\)\]\)\)\)\)\)\)

\(define\-syntaxdefrel/bank

\(syntax\-rules\(\)

\[\(\_\(namex…\)\#:prunekey\-exprbody…\)

\(definename

\(make\-bank\-rel\(length’\(x…\)\)

\(lambda\(x…\)\(conj\+body…\)\)

\(lambda\(x…\)key\-expr\)\)\)\]\)\)

;;—defrel/bank\-w:weightedbankwithdepthdecay——————–

;;

;;Sameasdefrel/bankbutusesweightedstreamsandappliesadecay

;;factortoeachcall\.Recursiveusesoftherelationgetweight

;;scaledby‘decay‘\(default0\.5\)\.Withsorted\-mergemplus\-w,this

;;producesdepth\-orderedenumeration:shallowrepresentativesare

;;emittedbeforedeeperones\.

;;

;;\(defrel/bank\-w\(relx…\)\#:prunekey\-expr\#:decaydbody…\)

;;

;;Thebodyshouldusethe\*\-wcombinators\(conde\-w,fresh\-w,conj\-w\+\)

;;soitsinternalschedulingparticipatesintheweightedordering\.

;;Plain==isauto\-liftedtoweight1\.

;;

;;Replay\-stream\-wistheweightedanalogueofreplay\-stream:each

;;canonicalcellcarriesaweightthatgetspassedthroughtothe

;;caller\.Theouter‘\(scale\-wdecay…\)‘wrapperaddsonefactorof

;;decayperinvocation,soadepth\-Kcanonicalcelldeliveredtothe

;;callerhasweightroughlydecay^\(2K\+1\)\.

\(define\(replay\-stream\-wcanonicalcaller\-stateargs\-vecnum\-args\)

\(cond

\[\(null?canonical\)’\(\)\]

\[\(lazy?canonical\)

;;Preservethecanonicallazy’sweightceiling–replaydoesn’t

;;changeweights,onlyrenamesvars\.Crucially,wedoNOTforce

;;thecanonicalthunkhere;thelazyisreturnedas\-is,andthe

;;consumerforcesitonlywhenitsweightindicatesitmightwin\.

\(lazy\(lazy\-weightcanonical\)

\(lambda\(\)

\(replay\-stream\-w\(\(lazy\-thunkcanonical\)\)

caller\-stateargs\-vecnum\-args\)\)\)\]

\[else

\(let\*\(\[cell\(carcanonical\)\]\[w\(carcell\)\]\[cs\(cdrcell\)\]\)

\(let\(\[new\(replay\-statecscaller\-stateargs\-vecnum\-args\)\]\)

\(cond

\[new\(cons\(conswnew\)

\(replay\-stream\-w\(cdrcanonical\)caller\-stateargs\-vecnum\-args\)\)\]

\[else\(replay\-stream\-w\(cdrcanonical\)caller\-stateargs\-vecnum\-args\)\]\)\)\)\]\)\)

\(define\(init\-bank\-cell\-wcacherel\-tagbody\-fnkey\-fnnum\-args\)

\(definecanonical\-vars\(for/list\(\[i\(in\-rangenum\-args\)\]\)\(vari\)\)\)

\(definecanonical\-state\(cons’\(\)num\-args\)\)

\(defineb\(box\#f\)\)

\(hash\-set\!cacherel\-tagb\)

\(definekey\(applykey\-fncanonical\-vars\)\)

\(definebody\-goal\(applybody\-fncanonical\-vars\)\)

\(defines\(\(prune\-wkeybody\-goal\)canonical\-state\)\)

\(set\-box\!b\(memo\-streams\)\)

b\)

\(define\(make\-bank\-rel\-wnum\-argsbody\-fnkey\-fndecay\)

\(definerel\-tag\(box\#f\)\)

\(lambdaactual\-args

\(let\(\[args\-vec\(list\-\>vectoractual\-args\)\]\)

\(lambda\(s/c\)

\(let\(\[cache\(current\-memo\)\]\)

\(cond

\[cache

\(let\(\[b\(or\(hash\-refcacherel\-tag\#f\)

\(init\-bank\-cell\-wcacherel\-tagbody\-fnkey\-fnnum\-args\)\)\]\)

\(scale\-wdecay

\(replay\-stream\-w\(unboxb\)s/cargs\-vecnum\-args\)\)\)\]

\[else

\(scale\-wdecay

\(\(prune\-w\(applykey\-fnactual\-args\)\(applybody\-fnactual\-args\)\)s/c\)\)\]\)\)\)\)\)\)

\(define\-syntaxdefrel/bank\-w

\(syntax\-rules\(\)

\[\(\_\(namex…\)\#:prunekey\-expr\#:decaydecaybody…\)

\(definename

\(make\-bank\-rel\-w\(length’\(x…\)\)

\(lambda\(x…\)\(conj\-w\+body…\)\)

\(lambda\(x…\)key\-expr\)

decay\)\)\]

\[\(\_\(namex…\)\#:prunekey\-exprbody…\)

;;defaultdecay

\(defrel/bank\-w\(namex…\)\#:prunekey\-expr\#:decay0\.5body…\)\]\)\)

#### A\.5\.5\.bench/bank\.rkt

\#langracket/base

;;Bottom\-upobservational\-equivalencebankforPBEsynthesis\.

;;

;;build\-bank/depthgrowsasetofprogramslayerbylayer,keepingone

;;representativeperobservablebehavior\.Composesinhostcode;the

;;producedbankisthenenumeratedrelationallyby‘membero‘\.

;;

;;ThisisthestandardPBEbankconstruction\.Itpreservescompleteness

;;underconj/bind\(unlikeashareddeduptable\)becauseeachentryin

;;thebankisaconcretesyntacticrepthatcanbereplayedanynumber

;;oftimesforanycaller\.

\(require”\.\./microkanren\.rkt”\)

\(providebuild\-bank/depthmembero\)

;;build\-bank/depth:

;;\(listofprog\-\>listofprog\);grammar\-step:composebankentries

;;\(listofprog\);terminals:leafprograms

;;\(prog\-\>any\);behavior:observablekey

;;natural;d:numberofcompositionlayers

;;\-\>\(listofprog\)

\(define\(build\-bank/depthgrammar\-stepterminalsbehaviord\)

\(defineseen\(make\-hash\)\)

\(definebank’\(\)\)

\(define\(tryp\)

\(defineb\(behaviorp\)\)

\(unless\(hash\-has\-key?seenb\)

\(hash\-set\!seenb\#t\)

\(set\!bank\(conspbank\)\)\)\)

\(for\(\[t\(in\-listterminals\)\]\)\(tryt\)\)

\(for\(\[\_\(in\-ranged\)\]\)

\(definesnapshotbank\);freezethebankforthislayer’scompositions

\(for\(\[p\(in\-list\(grammar\-stepsnapshot\)\)\]\)\(tryp\)\)\)

\(reversebank\)\)

;;membero:term\(listofterm\)\-\>goal

;;

;;Agoalthatsucceedswithvunifiedtoeachelementoflsinturn\.

;;Lazy:producesonestateperpull,so‘run1‘stopsatthefirst

;;matchwithoutmaterializingthewholelistofstates\.

\(define\(memberovls\)

\(lambda\(s/c\)

\(letloop\(\[lsls\]\)

\(cond

\[\(null?ls\)’\(\)\]

\[else

\(let\(\[result\(\(==v\(carls\)\)s/c\)\]\)

\(cond

\[\(null?result\)\(loop\(cdrls\)\)\]

\[else\(cons\(carresult\)\(lambda\(\)\(loop\(cdrls\)\)\)\)\]\)\)\]\)\)\)\)

#### A\.5\.6\.main\.rkt

\#langracket/base

;;prune\-kanren:miniKanrenwithbuilt\-inpruningforPBEprogramsynthesis\.

;;Re\-exportsthemicroKanrencore,theminiKanren\-stylesurfaceforms,

;;theprunecombinator,andthememoizedrelationforms\.

\(require”microkanren\.rkt”

”wrappers\.rkt”

”prune\.rkt”

”memo\.rkt”\)

\(provide\(all\-from\-out”microkanren\.rkt”\)

\(all\-from\-out”wrappers\.rkt”\)

\(all\-from\-out”prune\.rkt”\)

\(all\-from\-out”memo\.rkt”\)\)

#### A\.5\.7\.info\.rkt

\#langinfo

\(definecollection”prune\-kanren”\)

\(definepkg\-desc

”AminiKanrenimplementationwithabuilt\-inpruningmechanism,suitableforPBEprogramsynthesis\.”\)

\(defineversion”0\.0”\)

\(definepkg\-authors’\(nikolai\-kudasov\)\)

\(definelicense’MIT\)

\(definedeps’\(”base”\)\)

\(definebuild\-deps’\(”racket\-doc”

”rackunit\-lib”

”scribble\-lib”\)\)

#### A\.5\.8\.examples/shared\-table\-witness\.rkt

\#langracket/base

;;Experimental:shareddeduptableacrossnestedprunesviaaparameter\.

;;Theoutermostprunecallcreatesthetable;recursiveprunecalls

;;inherititviacurrent\-prune\-table\.Testswhethersharingspeedsup

;;thedepth\-lesssearchANDpreservesthesynthesisanswer\.

;;

;;RESULT:sharingbreakscompleteness\.Runningthisfilehangsonthe

;;easytarget\(‘x\*x‘\)beforereachingthehardone\.Thereason:the

;;outerpruneemitstheleaf‘\(==e’x\)‘first,addingbehavior\(234\)

;;tothesharedtable\.Whentherecursivebranchthenruns‘\(exprl\)‘

;;and‘\(exprr\)‘totrytoform‘\(timesxx\)‘,bothchildrenwouldbe

;;‘x‘withbehavior\(234\)–whichisnowblockedbythetable\.

;;\(timesxx\)isunreachable,andthesearchneverfindsanotherground

;;termwithbehavior\(4916\)soitloopsforeverpullingatthe

;;depth\-lessstream\.

;;

;;Moregenerally:simplesharingbreaksanysynthesistargetwhose

;;sub\-expressionsshareabehaviorwithanythingalreadyemitted\.

;;Thisbenchmarkiskeptasawitnesstothatfailure\.ItisNOTmeant

;;toberununattended;thesecondrunwillhang\.

\(require”\.\./main\.rkt”\)

;;—shared\-tableprune—

\(definecurrent\-prune\-table\(make\-parameter\#f\)\)

\(define\(prune/sharedkeyg\)

\(let\(\[table\(or\(current\-prune\-table\)\(make\-hash\)\)\]\)

\(lambda\(s/c\)

\(parameterize\(\[current\-prune\-tabletable\]\)

\(prune\-stream/sharedkeytable\(gs/c\)\)\)\)\)\)

\(define\(prune\-stream/sharedkeyseen$\)

\(cond

\[\(null?$\)’\(\)\]

\[\(procedure?$\)

\(lambda\(\)

\(parameterize\(\[current\-prune\-tableseen\]\)

\(prune\-stream/sharedkeyseen\($\)\)\)\)\]

\[else

\(let\*\(\[s/c\(car$\)\]

\[k\(keys/c\)\]\)

\(cond

\[\(eq?kskip\-prune\)

\(conss/c\(prune\-stream/sharedkeyseen\(cdr$\)\)\)\]

\[\(hash\-has\-key?seenk\)

\(prune\-stream/sharedkeyseen\(cdr$\)\)\]

\[else

\(hash\-set\!seenk\#t\)

\(conss/c\(prune\-stream/sharedkeyseen\(cdr$\)\)\)\]\)\)\]\)\)

;;—problem—

\(defineinputs’\(234\)\)

\(defineeasy\-io’\(\(2\.4\)\(3\.9\)\(4\.16\)\)\)

\(definehard\-io’\(\(2\.10\)\(3\.17\)\(4\.26\)\)\)

\(define\(interpex\)

\(cond

\[\(eq?e’x\)x\]

\[\(number?e\)e\]

\[\(and\(pair?e\)\(eq?\(care\)’plus\)\)

\(\+\(interp\(cadre\)x\)\(interp\(caddre\)x\)\)\]

\[\(and\(pair?e\)\(eq?\(care\)’times\)\)

\(\*\(interp\(cadre\)x\)\(interp\(caddre\)x\)\)\]

\[else\(error’interp”badexpression:~v”e\)\]\)\)

\(define\(behavior\-keye\)

\(ground\-keye\(lambda\(t\)\(map\(lambda\(x\)\(interptx\)\)inputs\)\)\)\)

\(define\(matcheseio\-pairs\)

\(when\-grounde

\(lambda\(t\)

\(andmap\(lambda\(io\)\(equal?\(interpt\(cario\)\)\(cdrio\)\)\)

io\-pairs\)\)\)\)

;;—exprwitheachpruneflavor—

\(define\(expr\-orige\)

\(prune\(behavior\-keye\)

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)

\(conde

\[\(==e‘\(plus,l,r\)\)\]

\[\(==e‘\(times,l,r\)\)\]\)

\(expr\-origl\)\(expr\-origr\)\)\]\)\)\)

\(define\(expr\-sharede\)

\(prune/shared\(behavior\-keye\)

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)

\(conde

\[\(==e‘\(plus,l,r\)\)\]

\[\(==e‘\(times,l,r\)\)\]\)

\(expr\-sharedl\)\(expr\-sharedr\)\)\]\)\)\)

\(define\(time\-itlabelthunk\)

\(collect\-garbage\)

\(definestart\(current\-inexact\-milliseconds\)\)

\(defineresult\(thunk\)\)

\(defineelapsed\(\-\(current\-inexact\-milliseconds\)start\)\)

\(printf”~a:result=~v\(~ams\)~n”

labelresult\(real\-\>decimal\-stringelapsed1\)\)

;;Returnvoid:anon\-voidvalueatmodulelevelwouldprinttwice\.

\(void\)\)

\(module\+main

\(printf”===easytarget:x\*x\(expected:\(timesxx\)\)===~n”\)

\(time\-it”expr\-orig”\(lambda\(\)\(run1\(e\)\(expr\-orige\)\(matcheseeasy\-io\)\)\)\)

\(time\-it”expr\-shared”\(lambda\(\)\(run1\(e\)\(expr\-sharede\)\(matcheseeasy\-io\)\)\)\)

\(printf”~n===hardtarget:\(1\+x\)^2\+1===~n”\)

\(time\-it”expr\-orig”\(lambda\(\)\(run1\(e\)\(expr\-orige\)\(matchesehard\-io\)\)\)\)

\(time\-it”expr\-shared”\(lambda\(\)\(run1\(e\)\(expr\-sharede\)\(matchesehard\-io\)\)\)\)\)

#### A\.5\.9\.bench/shallow\-bench\.rkt

\#langracket/base

;;Synthesisbenchmarksuite:defrel/bankvsdepth\-boundedprune\.

;;

;;Comparesthecleandepth\-lessdefrel/bankstyleagainstthemore

;;verboseexpr\-boundedidiomacrossmultiplePBEtargets,intwo

;;domains:

;;

;;1\.Arithmetic–polynomialsoverasingleintegerinputx\.

;;2\.Stringmanipulation–concatenationgrammaroverasingle

;;stringinput,àlaPolikarpova’s”BigIdeasinProgram

;;Synthesis”examples\(greetingformatters,echopatterns,etc\)\.

;;

;;Foreachtarget,boundedisrunatthesmallestdepththatadmitsa

;;solution\(bestcaseforbounded\)\.defrel/bankhasnodepthknob\.

\(require”\.\./main\.rkt”

”bank\.rkt”\)

;;—per\-targettimeoutviathread\+custodian\(copiedfromdeep\-bench\)—

\(define\(with\-time\-limitmsthunkon\-timeout\)

\(defineresult\-ch\(make\-channel\)\)

\(definecust\(make\-custodian\)\)

\(parameterize\(\[current\-custodiancust\]\)

\(thread

\(lambda\(\)

\(with\-handlers\(\[exn:fail?\(lambda\(e\)\(channel\-putresult\-ch\(cons’errore\)\)\)\]\)

\(channel\-putresult\-ch\(cons’ok\(thunk\)\)\)\)\)\)\)

\(sync

\(handle\-evtresult\-ch

\(lambda\(v\)

\(case\(carv\)

\[\(ok\)\(cdrv\)\]

\[\(error\)\(raise\(cdrv\)\)\]\)\)\)

\(handle\-evt\(alarm\-evt\(\+\(current\-inexact\-milliseconds\)ms\)\)

\(lambda\(\_\)

\(custodian\-shutdown\-allcust\)

\(on\-timeout\)\)\)\)\)

\(define\(timed\-runbudget\-msthunk\)

\(collect\-garbage\)

\(definestart\(current\-inexact\-milliseconds\)\)

\(defineresult

\(with\-time\-limitbudget\-msthunk\(lambda\(\)’TIMEOUT\)\)\)

\(defineelapsed\(\-\(current\-inexact\-milliseconds\)start\)\)

\(valuesresultelapsed\)\)

\(define\(time\-ititersthunk\)

\(collect\-garbage\)

\(definestart\(current\-inexact\-milliseconds\)\)

\(defineresult\#f\)

\(for\(\[i\(in\-rangeiters\)\]\)

\(set\!result\(thunk\)\)\)

\(defineelapsed\(\-\(current\-inexact\-milliseconds\)start\)\)

\(valuesresult\(/elapsediters\)\)\)

\(define\(pad\-rightns\)

\(if\(\>=\(string\-lengths\)n\)

s

\(string\-appends\(make\-string\(\-n\(string\-lengths\)\)\#\\space\)\)\)\)

\(define\(run\-targettargettarget\-banktarget\-bounded\)

\(definename\(cartarget\)\)

\(defineio\-pairs\(cadrtarget\)\)

\(definedepth\(caddrtarget\)\)

\(defineiters\(cadddrtarget\)\)

\(define\-values\(bank\-resultbank\-ms\)\(time\-ititerstarget\-bank\)\)

\(define\-values\(bounded\-resultbounded\-ms\)\(time\-ititerstarget\-bounded\)\)

\(printf”~adepth=~abounded~amsbank~amsratio~ax~n”

\(pad\-right24name\)

depth

\(pad\-right7\(real\-\>decimal\-stringbounded\-ms3\)\)

\(pad\-right7\(real\-\>decimal\-stringbank\-ms3\)\)

\(real\-\>decimal\-string\(/bank\-msbounded\-ms\)2\)\)

\(unless\(and\(pair?bank\-result\)\(pair?bounded\-result\)\)

\(printf”\!\!\!oneofthesearchesreturnednoanswer~n”\)\)

\(printf”boundedfound:~v~n”\(and\(pair?bounded\-result\)\(carbounded\-result\)\)\)

\(printf”bankfound:~v~n”\(and\(pair?bank\-result\)\(carbank\-result\)\)\)\)

;;============================================================

;;Domain1:Arithmetic

;;============================================================

\(definearith\-inputs’\(234\)\)

\(define\(arith\-interpex\)

\(cond

\[\(eq?e’x\)x\]

\[\(number?e\)e\]

\[\(eq?\(care\)’plus\)\(\+\(arith\-interp\(cadre\)x\)\(arith\-interp\(caddre\)x\)\)\]

\[\(eq?\(care\)’times\)\(\*\(arith\-interp\(cadre\)x\)\(arith\-interp\(caddre\)x\)\)\]\)\)

\(define\(arith\-keye\)

\(ground\-keye\(lambda\(t\)\(map\(lambda\(x\)\(arith\-interptx\)\)arith\-inputs\)\)\)\)

\(define\(arith\-matcheseio\-pairs\)

\(when\-grounde\(lambda\(t\)

\(andmap\(lambda\(io\)\(equal?\(arith\-interpt\(cario\)\)\(cdrio\)\)\)io\-pairs\)\)\)\)

\(defrel/bank\(arith\-banke\)

\#:prune\(arith\-keye\)

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)\(conde\[\(==e‘\(plus,l,r\)\)\]\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-bankl\)\(arith\-bankr\)\)\]\)\)

\(define\(arith\-boundededepth\)

\(prune\(arith\-keye\)

\(cond

\[\(zero?depth\)\(conde\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]\)\]

\[else

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)\(conde\[\(==e‘\(plus,l,r\)\)\]\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-boundedl\(\-depth1\)\)\(arith\-boundedr\(\-depth1\)\)\)\]\)\]\)\)\)

;;\(nameio\-pairsminimum\-depthiterations\)

\(definearith\-targets

‘\(\(”identity:x”

\(\(2\.2\)\(3\.3\)\(4\.4\)\)01000\)

\(”square:x\*x”

\(\(2\.4\)\(3\.9\)\(4\.16\)\)1500\)

\(”x^2\+x”

\(\(2\.6\)\(3\.12\)\(4\.20\)\)2200\)

\(”x^2\+2x\+1=\(x\+1\)^2”

\(\(2\.9\)\(3\.16\)\(4\.25\)\)2200\)

\(”\(1\+x\)^2\+1”

\(\(2\.10\)\(3\.17\)\(4\.26\)\)350\)

\(”x^3”

\(\(2\.8\)\(3\.27\)\(4\.64\)\)2100\)

\(”x^3\+1”

\(\(2\.9\)\(3\.28\)\(4\.65\)\)350\)\)\)

\(define\(arith\-bench\)

\(printf”~n============================================================~n”\)

\(printf”Arithmeticsynthesis\(inputs:~v\)~n”arith\-inputs\)

\(printf”Grammar:e::=x\|0\|1\|\(plusee\)\|\(timesee\)~n”\)

\(printf”============================================================~n”\)

\(for\(\[target\(in\-listarith\-targets\)\]\)

\(defineio\-pairs\(cadrtarget\)\)

\(definedepth\(caddrtarget\)\)

\(run\-targettarget

\(lambda\(\)\(run1\(e\)\(arith\-banke\)\(arith\-matcheseio\-pairs\)\)\)

\(lambda\(\)\(run1\(e\)\(arith\-boundededepth\)\(arith\-matcheseio\-pairs\)\)\)\)\)\)

;;============================================================

;;Domain2:Stringmanipulation\(Polikarpova\-style\)

;;============================================================

\(definestr\-inputs’\(”world””Alice””Bob”\)\)

\(define\(str\-interpes\)

\(cond

\[\(eq?e’in\)s\]

\[\(string?e\)e\]

\[\(eq?\(care\)’concat\)

\(string\-append\(str\-interp\(cadre\)s\)\(str\-interp\(caddre\)s\)\)\]\)\)

\(define\(str\-keye\)

\(ground\-keye\(lambda\(t\)\(map\(lambda\(s\)\(str\-interpts\)\)str\-inputs\)\)\)\)

\(define\(str\-matcheseio\-pairs\)

\(when\-grounde\(lambda\(t\)

\(andmap\(lambda\(io\)\(equal?\(str\-interpt\(cario\)\)\(cdrio\)\)\)io\-pairs\)\)\)\)

;;Stringliteralsavailableasterminals\.InarealPBEsystemthese

;;wouldbeminedfromtheI/Oexamples\(Polikarpova’sapproachuses

;;substringsoftheoutputsthataren’tsubstringsoftheinputs\)\.

\(definestr\-literals’\(”””””\!””?””,””Hello,””Hi,””Dear”\)\)

\(defrel/bank\(str\-banke\)

\#:prune\(str\-keye\)

\(conde

\[\(==e’in\)\]

\[\(memberoestr\-literals\)\]

\[\(fresh\(lr\)\(==e‘\(concat,l,r\)\)

\(str\-bankl\)\(str\-bankr\)\)\]\)\)

;;Weightedvariantforbest\-firstenumeration\.Literalsmustbe

;;spelledoutasconde\-wbranchessothateachcontributesauniform

;;ceilingweight;recursiveconcatbranchesgetscale\-w’dbythe

;;defaultdecay\.

\(defrel/bank\-w\(str\-bank\-we\)

\#:prune\(str\-keye\)

\#:decay0\.5

\(conde\-w

\[\(==e’in\)\]

\[\(==e””\)\]\[\(==e””\)\]\[\(==e”\!”\)\]\[\(==e”?”\)\]

\[\(==e”,”\)\]\[\(==e”Hello,”\)\]

\[\(==e”Hi,”\)\]\[\(==e”Dear”\)\]

\[\(fresh\-w\(lr\)\(==e‘\(concat,l,r\)\)

\(str\-bank\-wl\)\(str\-bank\-wr\)\)\]\)\)

\(define\(str\-boundededepth\)

\(prune\(str\-keye\)

\(cond

\[\(zero?depth\)

\(conde\[\(==e’in\)\]\[\(memberoestr\-literals\)\]\)\]

\[else

\(conde

\[\(==e’in\)\]

\[\(memberoestr\-literals\)\]

\[\(fresh\(lr\)\(==e‘\(concat,l,r\)\)

\(str\-boundedl\(\-depth1\)\)\(str\-boundedr\(\-depth1\)\)\)\]\)\]\)\)\)

;;Host\-languagebottom\-upbankforstrings\.

\(definestr\-terminals\(cons’instr\-literals\)\)

\(define\(str\-grammar\-stepbank\)

\(for\*/list\(\[l\(in\-listbank\)\]

\[r\(in\-listbank\)\]\)

\(list’concatlr\)\)\)

\(define\(str\-behaviorp\)\(map\(lambda\(s\)\(str\-interpps\)\)str\-inputs\)\)

\(define\(str\-host\-bank\-resultdepthio\-pairs\)

\(definebank\(build\-bank/depthstr\-grammar\-stepstr\-terminals

str\-behaviordepth\)\)

\(run1\(e\)\(memberoebank\)\(str\-matcheseio\-pairs\)\)\)

\(definestr\-targets

‘\(\(”greeting:’Hello,X\!’”

\(\(”world”\.”Hello,world\!”\)

\(”Alice”\.”Hello,Alice\!”\)

\(”Bob”\.”Hello,Bob\!”\)\)

2100\)

\(”informalgreeting:’Hi,X?’”

\(\(”world”\.”Hi,world?”\)

\(”Alice”\.”Hi,Alice?”\)

\(”Bob”\.”Hi,Bob?”\)\)

2100\)

\(”echo\-with\-comma:’X,X’”

\(\(”world”\.”world,world”\)

\(”Alice”\.”Alice,Alice”\)

\(”Bob”\.”Bob,Bob”\)\)

2200\)

\(”greeting\+shout:’Hello,X\!\!’”

\(\(”world”\.”Hello,world\!\!”\)

\(”Alice”\.”Hello,Alice\!\!”\)

\(”Bob”\.”Hello,Bob\!\!”\)\)

310\)\)\)

\(define\(fmt\-resultv\)

\(cond

\[\(eq?v’TIMEOUT\)”TIMEOUT”\]

\[\(pair?v\)\(format”~v”\(carv\)\)\]

\[\(null?v\)”no\-answer”\]

\[else\(format”~v”v\)\]\)\)

;;Per\-targetbudgetforthebank\-wengineonstringtargets\.bank\-w

;;canbeveryslowonwidebehaviorspaces,sowewrapitina

;;timeoutratherthanrelyingontheiterationcounttoboundit\.

\(definestr\-bank\-w\-budget\-ms30000\)

\(define\(str\-bench\)

\(printf”~n============================================================~n”\)

\(printf”Stringsynthesis\(inputs:~v\)~n”str\-inputs\)

\(printf”Grammar:e::=in\|<literal\>\|\(concatee\)~n”\)

\(printf”Literals:~v~n”str\-literals\)

\(printf”============================================================~n”\)

\(for\(\[target\(in\-liststr\-targets\)\]\)

\(definename\(cartarget\)\)

\(defineio\-pairs\(cadrtarget\)\)

\(definedepth\(caddrtarget\)\)

\(defineiters\(cadddrtarget\)\)

\(printf”~adepth=~a\(iters=~a\)~n”

\(pad\-right30name\)depthiters\)

\(flush\-output\)

\(define\-values\(bounded\-rbounded\-ms\)

\(time\-ititers\(lambda\(\)\(run1\(e\)\(str\-boundededepth\)\(str\-matcheseio\-pairs\)\)\)\)\)

\(printf”bounded:~ams~a~n”

\(pad\-right8\(real\-\>decimal\-stringbounded\-ms3\)\)

\(fmt\-resultbounded\-r\)\)

\(flush\-output\)

\(define\-values\(bank\-rbank\-ms\)

\(time\-ititers\(lambda\(\)\(run1\(e\)\(str\-banke\)\(str\-matcheseio\-pairs\)\)\)\)\)

\(printf”bank:~ams~a~n”

\(pad\-right8\(real\-\>decimal\-stringbank\-ms3\)\)

\(fmt\-resultbank\-r\)\)

\(flush\-output\)

\(define\-values\(bank\-w\-rbank\-w\-ms\)

\(timed\-runstr\-bank\-w\-budget\-ms

\(lambda\(\)\(run\-w1\(e\)\(str\-bank\-we\)\(str\-matcheseio\-pairs\)\)\)\)\)

\(printf”bank\-w:~ams~a~n”

\(pad\-right8\(real\-\>decimal\-stringbank\-w\-ms3\)\)

\(fmt\-resultbank\-w\-r\)\)

\(flush\-output\)

\(define\-values\(host\-rhost\-ms\)

\(time\-ititers\(lambda\(\)\(str\-host\-bank\-resultdepthio\-pairs\)\)\)\)

\(printf”host\-bank:~ams~a~n”

\(pad\-right8\(real\-\>decimal\-stringhost\-ms3\)\)

\(fmt\-resulthost\-r\)\)

\(printf”~n”\)

\(flush\-output\)\)\)

\(module\+main

\(arith\-bench\)

\(str\-bench\)\)

#### A\.5\.10\.bench/deep\-bench\.rkt

\#langracket/base

;;DeeparithmeticPBEbenchmark–targetsatdepth4andbeyond\.

;;

;;Depthconvention:\(opab\)hasdepth1\+max\(depth\(a\),depth\(b\)\);

;;leavesaredepth0\.Right\-associatedx^khasdepthk\-1,and

;;\(1\+x\)^kright\-assochasdepthk\.

;;

;;Eachtargetrunsunderaper\-callwall\-clockbudget\.Ifarun

;;doesn’tfinishintime,it’sreportedas”TIMEOUT”\.Thiskeepsthe

;;benchfiniteevenwhenonestrategyrunsintoahardcase\.

;;

;;Threestrategiesarecomparedpertarget:

;;

;;bounded–depth\-boundedwithprune\(idiomaticminiKanren\)\.User

;;mustknowtherightdepth\.

;;bank–defrel/bank:depth\-firstcanonicalenumerationwith

;;sharedprunecache\.Fastforright\-spinetargets

;;\(x^k\);thecanonicalordermakes\(1\+x\)^kslowbecause

;;itscompactrepresentativesitsverylateinthe

;;enumeration\.

;;bank\-w–defrel/bank\-w:depth\-decayedbest\-firstenumeration

;;\(decay=0\.5\)\.Weightsonimmaturestreams\(the‘lazy‘

;;struct\)preventthememo\-thunkre\-entrythatwould

;;otherwiseoccur\.Findsthemostcompactrepresentative

;;first;paysforitondeeptargetsbecauseitmust

;;emitallshallowercellsfirst\(BFS\-style\)\.

\(require”\.\./main\.rkt”

”bank\.rkt”\)

;;—per\-targettimeoutviathread\+custodian—

\(define\(with\-time\-limitmsthunkon\-timeout\)

\(defineresult\-ch\(make\-channel\)\)

\(definecust\(make\-custodian\)\)

\(definet

\(parameterize\(\[current\-custodiancust\]\)

\(thread

\(lambda\(\)

\(with\-handlers\(\[exn:fail?\(lambda\(e\)\(channel\-putresult\-ch\(cons’errore\)\)\)\]\)

\(channel\-putresult\-ch\(cons’ok\(thunk\)\)\)\)\)\)\)\)

\(sync

\(handle\-evtresult\-ch

\(lambda\(v\)

\(case\(carv\)

\[\(ok\)\(cdrv\)\]

\[\(error\)\(raise\(cdrv\)\)\]\)\)\)

\(handle\-evt\(alarm\-evt\(\+\(current\-inexact\-milliseconds\)ms\)\)

\(lambda\(\_\)

\(custodian\-shutdown\-allcust\)

\(on\-timeout\)\)\)\)\)

\(define\(timed\-runbudget\-msthunk\)

\(collect\-garbage\)

\(definestart\(current\-inexact\-milliseconds\)\)

\(defineresult

\(with\-time\-limitbudget\-ms

thunk

\(lambda\(\)’TIMEOUT\)\)\)

\(defineelapsed\(\-\(current\-inexact\-milliseconds\)start\)\)

\(valuesresultelapsed\)\)

;;—problemsetup—

\(defineinputs’\(234\)\)

\(define\(interpex\)

\(cond

\[\(eq?e’x\)x\]

\[\(number?e\)e\]

\[\(eq?\(care\)’plus\)\(\+\(interp\(cadre\)x\)\(interp\(caddre\)x\)\)\]

\[\(eq?\(care\)’times\)\(\*\(interp\(cadre\)x\)\(interp\(caddre\)x\)\)\]\)\)

\(define\(arith\-keye\)

\(ground\-keye\(lambda\(t\)\(map\(lambda\(x\)\(interptx\)\)inputs\)\)\)\)

\(define\(matcheseio\-pairs\)

\(when\-grounde\(lambda\(t\)

\(andmap\(lambda\(io\)\(equal?\(interpt\(cario\)\)\(cdrio\)\)\)io\-pairs\)\)\)\)

;;Standarddepth\-firstbank–uses‘conj‘andemitscellsin

;;canonicalrecursionorder\.Faston”right\-spine”targetslikex^k;

;;loseson\(1\+x\)^kbecausethenaturalrepresentativeappearslate

;;inthecanonicalenumerationorder\.

\(defrel/bank\(arith\-banke\)

\#:prune\(arith\-keye\)

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)\(conde\[\(==e‘\(plus,l,r\)\)\]\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-bankl\)\(arith\-bankr\)\)\]\)\)

;;Depth\-decayedbest\-firstbank–weightedstreamswithdecay=0\.5

;;perrecursivecall\.Findsthemostcompact\(shallowest\)

;;representativeforeachbehavior\.Slowerondeeptargetsbecause

;;itexploresallshallowercellsfirst\.

\(defrel/bank\-w\(arith\-bank\-we\)

\#:prune\(arith\-keye\)

\#:decay0\.5

\(conde\-w

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\-w\(lr\)\(conde\-w\[\(==e‘\(plus,l,r\)\)\]\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-bank\-wl\)\(arith\-bank\-wr\)\)\]\)\)

\(define\(arith\-boundededepth\)

\(prune\(arith\-keye\)

\(cond

\[\(zero?depth\)\(conde\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]\)\]

\[else

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)\(conde\[\(==e‘\(plus,l,r\)\)\]\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-boundedl\(\-depth1\)\)\(arith\-boundedr\(\-depth1\)\)\)\]\)\]\)\)\)

;;—host\-languagebottom\-upbank—

;;

;;BuildsthededuplicatedbankinRacket\(norelationalcomposition\)

;;andthenexposesitsmembershippredicatetoarelationalqueryvia

;;‘membero‘\.End\-to\-endtimeincludesbankbuild\.

\(definearith\-terminals’\(x01\)\)

\(define\(arith\-grammar\-stepbank\)

\(for\*/list\(\[l\(in\-listbank\)\]

\[r\(in\-listbank\)\]

\[op\(in\-list’\(plustimes\)\)\]\)

\(listoplr\)\)\)

\(define\(arith\-behaviorp\)\(map\(lambda\(x\)\(interppx\)\)inputs\)\)

\(define\(arith\-host\-bank\-resultdepthio\-pairs\)

\(definebank\(build\-bank/deptharith\-grammar\-steparith\-terminals

arith\-behaviordepth\)\)

\(run1\(e\)\(memberoebank\)\(matcheseio\-pairs\)\)\)

;;—targets—

;;\(nameio\-pairsminimum\-depthbudget\-ms\)

\(definetargets

‘\(\(”\(1\+x\)^2\(d=2\)”

\(\(2\.9\)\(3\.16\)\(4\.25\)\)210000\)

\(”\(1\+x\)^3\(d=3\)”

\(\(2\.27\)\(3\.64\)\(4\.125\)\)330000\)

\(”x^5\(d=4\)”

\(\(2\.32\)\(3\.243\)\(4\.1024\)\)410000\)

\(”\(1\+x\)^4\(d=4\)”

\(\(2\.81\)\(3\.256\)\(4\.625\)\)430000\)

\(”x^5\+x\(d=5\)”

\(\(2\.34\)\(3\.246\)\(4\.1028\)\)530000\)

\(”x^5\+1\(d=5\)”

\(\(2\.33\)\(3\.244\)\(4\.1025\)\)530000\)

\(”x^6\(d=5\)”

\(\(2\.64\)\(3\.729\)\(4\.4096\)\)530000\)

\(”\(1\+x\)^5\(d=5\)”

\(\(2\.243\)\(3\.1024\)\(4\.3125\)\)530000\)

\(”x^6\+1\(d=6\)”

\(\(2\.65\)\(3\.730\)\(4\.4097\)\)660000\)

\(”x^7\(d=6\)”

\(\(2\.128\)\(3\.2187\)\(4\.16384\)\)660000\)\)\)

\(define\(pad\-rightns\)

\(if\(\>=\(string\-lengths\)n\)

s

\(string\-appends\(make\-string\(\-n\(string\-lengths\)\)\#\\space\)\)\)\)

\(define\(fmtv\)

\(cond

\[\(eq?v’TIMEOUT\)”TIMEOUT”\]

\[\(pair?v\)\(format”~v”\(carv\)\)\]

\[\(null?v\)”no\-answer”\]

\[else\(format”~v”v\)\]\)\)

\(module\+main

\(printf”DeeparithmeticPBEbenchmark\(inputs:~v\)~n”inputs\)

\(printf”Grammar:e::=x\|0\|1\|\(plusee\)\|\(timesee\)~n”\)

\(printf”============================================================~n”\)

\(flush\-output\)

\(for\(\[target\(in\-listtargets\)\]\)

\(definename\(cartarget\)\)

\(defineio\-pairs\(cadrtarget\)\)

\(definedepth\(caddrtarget\)\)

\(definebudget\(cadddrtarget\)\)

\(printf”~a\(budget=~as\)~n”

\(pad\-right18name\)

\(real\-\>decimal\-string\(/budget1000\)0\)\)

\(flush\-output\)

\(define\-values\(bounded\-rbounded\-ms\)

\(timed\-runbudget

\(lambda\(\)\(run1\(e\)\(arith\-boundededepth\)\(matcheseio\-pairs\)\)\)\)\)

\(printf”bounded\(d=~a\):~ams~a~n”

depth

\(pad\-right9\(real\-\>decimal\-stringbounded\-ms1\)\)

\(fmtbounded\-r\)\)

\(flush\-output\)

\(define\-values\(bank\-rbank\-ms\)

\(timed\-runbudget

\(lambda\(\)\(run1\(e\)\(arith\-banke\)\(matcheseio\-pairs\)\)\)\)\)

\(printf”bank\(DFS\):~ams~a~n”

\(pad\-right9\(real\-\>decimal\-stringbank\-ms1\)\)

\(fmtbank\-r\)\)

\(flush\-output\)

\(define\-values\(bank\-w\-rbank\-w\-ms\)

\(timed\-runbudget

\(lambda\(\)\(run\-w1\(e\)\(arith\-bank\-we\)\(matcheseio\-pairs\)\)\)\)\)

\(printf”bank\-w\(BFS\):~ams~a~n”

\(pad\-right9\(real\-\>decimal\-stringbank\-w\-ms1\)\)

\(fmtbank\-w\-r\)\)

\(flush\-output\)

\(define\-values\(host\-rhost\-ms\)

\(timed\-runbudget

\(lambda\(\)\(arith\-host\-bank\-resultdepthio\-pairs\)\)\)\)

\(printf”host\-bank:~ams~a~n”

\(pad\-right9\(real\-\>decimal\-stringhost\-ms1\)\)

\(fmthost\-r\)\)

\(define\(ratio\-stra\-ra\-msb\-rb\-ms\)

\(cond

\[\(or\(eq?a\-r’TIMEOUT\)\(eq?b\-r’TIMEOUT\)\)”\(timeout\)”\]

\[else

\(definer\(/a\-ms\(max0\.001b\-ms\)\)\)

\(cond\[\(<r1\)\(string\-append\(real\-\>decimal\-string\(/1r\)2\)”xFASTER”\)\]

\[else\(string\-append\(real\-\>decimal\-stringr2\)”xslower”\)\]\)\]\)\)

\(printf”=\>bankvsbounded:~a~n”

\(ratio\-strbank\-rbank\-msbounded\-rbounded\-ms\)\)

\(printf”=\>bank\-wvsbounded:~a~n”

\(ratio\-strbank\-w\-rbank\-w\-msbounded\-rbounded\-ms\)\)

\(printf”=\>host\-bankvsbounded:~a~n”

\(ratio\-strhost\-rhost\-msbounded\-rbounded\-ms\)\)

\(printf”=\>host\-bankvsbank:~a~n”

\(ratio\-strhost\-rhost\-msbank\-rbank\-ms\)\)

\(printf”~n”\)

\(flush\-output\)\)\)

#### A\.5\.11\.bench/order\-bench\.rkt

\#langracket/base

;;First\-answerenumerationindexperengine,pertarget\.

;;

;;Foreach\(engine,target\)pair,countshowmanycandidatesthe

;;engineemitsbefore\(andincluding\)thefirstonewhosebehavior

;;matchesthetarget’sI/Oexamples\.ThismeasuresWHEREthe

;;target’srepresentativesitsineachengine’senumerationorder,

;;independentlyoftheengine’sthroughput\.Theindicesfeedthe

;;indexannotationsinTable1ofthepaper\.

;;

;;Countingiscappedbyaper\-cellwall\-clockbudget\(asin

;;deep\-bench\.rkt\);cellsthatexceeditarereportedasTIMEOUT\.

;;Unlikethetimingbenches,thereportedindicesaredeterministic:

;;theydependonlyontheenumerationorder,notonmachinespeed\.

\(require”\.\./main\.rkt”

”bank\.rkt”\)

;;—per\-celltimeoutviathread\+custodian\(asindeep\-bench\)—

\(define\(with\-time\-limitmsthunkon\-timeout\)

\(defineresult\-ch\(make\-channel\)\)

\(definecust\(make\-custodian\)\)

\(parameterize\(\[current\-custodiancust\]\)

\(thread

\(lambda\(\)

\(with\-handlers\(\[exn:fail?\(lambda\(e\)\(channel\-putresult\-ch\(cons’errore\)\)\)\]\)

\(channel\-putresult\-ch\(cons’ok\(thunk\)\)\)\)\)\)\)

\(sync

\(handle\-evtresult\-ch

\(lambda\(v\)

\(case\(carv\)

\[\(ok\)\(cdrv\)\]

\[\(error\)\(raise\(cdrv\)\)\]\)\)\)

\(handle\-evt\(alarm\-evt\(\+\(current\-inexact\-milliseconds\)ms\)\)

\(lambda\(\_\)

\(custodian\-shutdown\-allcust\)

\(on\-timeout\)\)\)\)\)

;;—indexcounting——————————————————\-

;;first\-match\-index:\(var\-\>goal\)\(term\-\>boolean\)\-\>natural\|’no\-answer

;;

;;Appliesthegoaltoasinglefreshqueryvariableandwalksits

;;answerstream,countingstatesuntilthequerytermwalkstoa

;;groundtermsatisfyingpred\.Returnsthe1\-basedindexofthat

;;state\.Runsinsideamemosession,mirroringwhat‘run‘does\.

\(define\(first\-match\-indexmake\-goalpred\)

\(with\-memo\-session

\(letloop\(\[$\(\(call/freshmake\-goal\)empty\-state\)\]\[i1\]\)

\(let\(\[$\(pull$\)\]\)

\(cond

\[\(null?$\)’no\-answer\]

\[else

\(let\(\[t\(walk\*\(var0\)\(car\(car$\)\)\)\]\)

\(if\(and\(ground?t\)\(predt\)\)

i

\(loop\(cdr$\)\(\+i1\)\)\)\)\]\)\)\)\)\)

;;Weighted\-streamanalogue:cellsare\(weight\.state\)\.

\(define\(first\-match\-index\-wmake\-goalpred\)

\(with\-memo\-session

\(letloop\(\[$\(\(call/freshmake\-goal\)empty\-state\)\]\[i1\]\)

\(let\(\[$\(pull\-w$\)\]\)

\(cond

\[\(null?$\)’no\-answer\]

\[else

\(let\(\[t\(walk\*\(var0\)\(car\(cdr\(car$\)\)\)\)\]\)

\(if\(and\(ground?t\)\(predt\)\)

i

\(loop\(cdr$\)\(\+i1\)\)\)\)\]\)\)\)\)\)

;;Hostbank:1\-basedindexofthefirstmatchingprograminthebank

;;builttothetarget’sminimumdepth\(level\-by\-levelorder\)\.

\(define\(host\-bank\-indexgrammar\-stepterminalsbehaviordepthpred\)

\(definebank\(build\-bank/depthgrammar\-stepterminalsbehaviordepth\)\)

\(letloop\(\[psbank\]\[i1\]\)

\(cond

\[\(null?ps\)’no\-answer\]

\[\(pred\(carps\)\)i\]

\[else\(loop\(cdrps\)\(\+i1\)\)\]\)\)\)

;;—arithmeticdomain\(asindeep\-bench\.rkt\)——————————

\(defineinputs’\(234\)\)

\(define\(interpex\)

\(cond

\[\(eq?e’x\)x\]

\[\(number?e\)e\]

\[\(eq?\(care\)’plus\)\(\+\(interp\(cadre\)x\)\(interp\(caddre\)x\)\)\]

\[\(eq?\(care\)’times\)\(\*\(interp\(cadre\)x\)\(interp\(caddre\)x\)\)\]\)\)

\(define\(arith\-keye\)

\(ground\-keye\(lambda\(t\)\(map\(lambda\(x\)\(interptx\)\)inputs\)\)\)\)

\(define\(arith\-predio\-pairs\)

\(lambda\(t\)

\(andmap\(lambda\(io\)\(equal?\(interpt\(cario\)\)\(cdrio\)\)\)io\-pairs\)\)\)

\(defrel/bank\(arith\-banke\)

\#:prune\(arith\-keye\)

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)\(conde\[\(==e‘\(plus,l,r\)\)\]\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-bankl\)\(arith\-bankr\)\)\]\)\)

\(defrel/bank\-w\(arith\-bank\-we\)

\#:prune\(arith\-keye\)

\#:decay0\.5

\(conde\-w

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\-w\(lr\)\(conde\-w\[\(==e‘\(plus,l,r\)\)\]\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-bank\-wl\)\(arith\-bank\-wr\)\)\]\)\)

\(define\(arith\-boundededepth\)

\(prune\(arith\-keye\)

\(cond

\[\(zero?depth\)\(conde\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]\)\]

\[else

\(conde

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\(lr\)\(conde\[\(==e‘\(plus,l,r\)\)\]\[\(==e‘\(times,l,r\)\)\]\)

\(arith\-boundedl\(\-depth1\)\)\(arith\-boundedr\(\-depth1\)\)\)\]\)\]\)\)\)

\(definearith\-terminals’\(x01\)\)

\(define\(arith\-grammar\-stepbank\)

\(for\*/list\(\[l\(in\-listbank\)\]

\[r\(in\-listbank\)\]

\[op\(in\-list’\(plustimes\)\)\]\)

\(listoplr\)\)\)

\(define\(arith\-behaviorp\)\(map\(lambda\(x\)\(interppx\)\)inputs\)\)

;;\(nameio\-pairsminimum\-depthbudget\-ms\)–sametargetsasdeep\-bench\.rkt\.

\(definearith\-targets

‘\(\(”\(1\+x\)^2\(d=2\)”

\(\(2\.9\)\(3\.16\)\(4\.25\)\)210000\)

\(”\(1\+x\)^3\(d=3\)”

\(\(2\.27\)\(3\.64\)\(4\.125\)\)330000\)

\(”x^5\(d=4\)”

\(\(2\.32\)\(3\.243\)\(4\.1024\)\)410000\)

\(”\(1\+x\)^4\(d=4\)”

\(\(2\.81\)\(3\.256\)\(4\.625\)\)430000\)

\(”x^5\+x\(d=5\)”

\(\(2\.34\)\(3\.246\)\(4\.1028\)\)530000\)

\(”x^5\+1\(d=5\)”

\(\(2\.33\)\(3\.244\)\(4\.1025\)\)530000\)

\(”x^6\(d=5\)”

\(\(2\.64\)\(3\.729\)\(4\.4096\)\)530000\)

\(”\(1\+x\)^5\(d=5\)”

\(\(2\.243\)\(3\.1024\)\(4\.3125\)\)530000\)

\(”x^6\+1\(d=6\)”

\(\(2\.65\)\(3\.730\)\(4\.4097\)\)660000\)

\(”x^7\(d=6\)”

\(\(2\.128\)\(3\.2187\)\(4\.16384\)\)660000\)\)\)

;;—stringdomain\(asinshallow\-bench\.rkt\)——————————\-

\(definestr\-inputs’\(”world””Alice””Bob”\)\)

\(define\(str\-interpes\)

\(cond

\[\(eq?e’in\)s\]

\[\(string?e\)e\]

\[\(eq?\(care\)’concat\)

\(string\-append\(str\-interp\(cadre\)s\)\(str\-interp\(caddre\)s\)\)\]\)\)

\(define\(str\-keye\)

\(ground\-keye\(lambda\(t\)\(map\(lambda\(s\)\(str\-interpts\)\)str\-inputs\)\)\)\)

\(define\(str\-predio\-pairs\)

\(lambda\(t\)

\(andmap\(lambda\(io\)\(equal?\(str\-interpt\(cario\)\)\(cdrio\)\)\)io\-pairs\)\)\)

\(definestr\-literals’\(”””””\!””?””,””Hello,””Hi,””Dear”\)\)

\(defrel/bank\(str\-banke\)

\#:prune\(str\-keye\)

\(conde

\[\(==e’in\)\]

\[\(memberoestr\-literals\)\]

\[\(fresh\(lr\)\(==e‘\(concat,l,r\)\)

\(str\-bankl\)\(str\-bankr\)\)\]\)\)

\(defrel/bank\-w\(str\-bank\-we\)

\#:prune\(str\-keye\)

\#:decay0\.5

\(conde\-w

\[\(==e’in\)\]

\[\(==e””\)\]\[\(==e””\)\]\[\(==e”\!”\)\]\[\(==e”?”\)\]

\[\(==e”,”\)\]\[\(==e”Hello,”\)\]

\[\(==e”Hi,”\)\]\[\(==e”Dear”\)\]

\[\(fresh\-w\(lr\)\(==e‘\(concat,l,r\)\)

\(str\-bank\-wl\)\(str\-bank\-wr\)\)\]\)\)

\(define\(str\-boundededepth\)

\(prune\(str\-keye\)

\(cond

\[\(zero?depth\)

\(conde\[\(==e’in\)\]\[\(memberoestr\-literals\)\]\)\]

\[else

\(conde

\[\(==e’in\)\]

\[\(memberoestr\-literals\)\]

\[\(fresh\(lr\)\(==e‘\(concat,l,r\)\)

\(str\-boundedl\(\-depth1\)\)\(str\-boundedr\(\-depth1\)\)\)\]\)\]\)\)\)

\(definestr\-terminals\(cons’instr\-literals\)\)

\(define\(str\-grammar\-stepbank\)

\(for\*/list\(\[l\(in\-listbank\)\]

\[r\(in\-listbank\)\]\)

\(list’concatlr\)\)\)

\(define\(str\-behaviorp\)\(map\(lambda\(s\)\(str\-interpps\)\)str\-inputs\)\)

\(definestr\-targets

‘\(\(”greeting:’Hello,X\!’”

\(\(”world”\.”Hello,world\!”\)

\(”Alice”\.”Hello,Alice\!”\)

\(”Bob”\.”Hello,Bob\!”\)\)

230000\)

\(”informalgreeting:’Hi,X?’”

\(\(”world”\.”Hi,world?”\)

\(”Alice”\.”Hi,Alice?”\)

\(”Bob”\.”Hi,Bob?”\)\)

230000\)

\(”echo\-with\-comma:’X,X’”

\(\(”world”\.”world,world”\)

\(”Alice”\.”Alice,Alice”\)

\(”Bob”\.”Bob,Bob”\)\)

230000\)

\(”greeting\+shout:’Hello,X\!\!’”

\(\(”world”\.”Hello,world\!\!”\)

\(”Alice”\.”Hello,Alice\!\!”\)

\(”Bob”\.”Hello,Bob\!\!”\)\)

330000\)\)\)

;;—driver—————————————————————–

\(define\(fmtv\)

\(cond\[\(eq?v’TIMEOUT\)”TIMEOUT”\]

\[\(eq?v’no\-answer\)”no\-answer”\]

\[else\(format”\#~a”v\)\]\)\)

\(define\(report\-celllabelbudgetthunk\)

\(definev\(with\-time\-limitbudgetthunk\(lambda\(\)’TIMEOUT\)\)\)

\(printf”~a:~a~n”label\(fmtv\)\)

\(flush\-output\)\)

\(module\+main

\(printf”First\-answerenumerationindexperengine~n”\)

\(printf”==========================================~n”\)

\(printf”~nArithmeticPBE\(inputs:~v\)~n”inputs\)

\(for\(\[target\(in\-listarith\-targets\)\]\)

\(definename\(cartarget\)\)

\(defineio\-pairs\(cadrtarget\)\)

\(definedepth\(caddrtarget\)\)

\(definebudget\(cadddrtarget\)\)

\(definepred\(arith\-predio\-pairs\)\)

\(printf”~a~n”name\)

\(report\-cell”bounded”budget

\(lambda\(\)\(first\-match\-index\(lambda\(q\)\(arith\-boundedqdepth\)\)pred\)\)\)

\(report\-cell”bank”budget

\(lambda\(\)\(first\-match\-index\(lambda\(q\)\(arith\-bankq\)\)pred\)\)\)

\(report\-cell”bank\-w”budget

\(lambda\(\)\(first\-match\-index\-w\(lambda\(q\)\(arith\-bank\-wq\)\)pred\)\)\)

\(report\-cell”host\-bank”budget

\(lambda\(\)\(host\-bank\-indexarith\-grammar\-steparith\-terminals

arith\-behaviordepthpred\)\)\)\)

\(printf”~nStringPBE\(inputs:~v\)~n”str\-inputs\)

\(for\(\[target\(in\-liststr\-targets\)\]\)

\(definename\(cartarget\)\)

\(defineio\-pairs\(cadrtarget\)\)

\(definedepth\(caddrtarget\)\)

\(definebudget\(cadddrtarget\)\)

\(definepred\(str\-predio\-pairs\)\)

\(printf”~a~n”name\)

\(report\-cell”bounded”budget

\(lambda\(\)\(first\-match\-index\(lambda\(q\)\(str\-boundedqdepth\)\)pred\)\)\)

\(report\-cell”bank”budget

\(lambda\(\)\(first\-match\-index\(lambda\(q\)\(str\-bankq\)\)pred\)\)\)

\(report\-cell”bank\-w”budget

\(lambda\(\)\(first\-match\-index\-w\(lambda\(q\)\(str\-bank\-wq\)\)pred\)\)\)

\(report\-cell”host\-bank”budget

\(lambda\(\)\(host\-bank\-indexstr\-grammar\-stepstr\-terminals

str\-behaviordepthpred\)\)\)\)\)

#### A\.5\.12\.bench/decay\-bench\.rkt

\#langracket/base

;;Decay\-factorexperimentfordefrel/bank\-w\.

;;

;;Withauniformdecayfactordappliedateveryrecursivecall,

;;everycanonicalcell’sweightisd^n,wherencountstherecursive

;;callsinthecell’sderivation\.Sinced^nismonotoneinnforany

;;din\(0,1\),thepairwisecomparisonsmadebymplus\-warethesame

;;foreverysuchd,andthesorted\-mergeenumerationorderis

;;invariantunderthechoiceofd\.Thedecayknobthereforeonly

;;becomesmeaningfulwhendifferentproductionscarrydifferent

;;weights\(e\.g\.Probe\-stylelearnedweights\)\.

;;

;;Thisscriptverifiestheclaimempirically:forseveralvaluesof

;;d,it\(1\)enumeratesthefirstKrepresentativesoftheweighted

;;arithmeticbankandchecksthattheprefixescoincide,and

;;\(2\)timesthe\(1\+x\)^2synthesistargetundereachd\.

\(require”\.\./main\.rkt”\)

\(defineinputs’\(234\)\)

\(define\(interpex\)

\(cond

\[\(eq?e’x\)x\]

\[\(number?e\)e\]

\[\(eq?\(care\)’plus\)\(\+\(interp\(cadre\)x\)\(interp\(caddre\)x\)\)\]

\[\(eq?\(care\)’times\)\(\*\(interp\(cadre\)x\)\(interp\(caddre\)x\)\)\]\)\)

\(define\(arith\-keye\)

\(ground\-keye\(lambda\(t\)\(map\(lambda\(x\)\(interptx\)\)inputs\)\)\)\)

\(define\(matcheseio\-pairs\)

\(when\-grounde

\(lambda\(t\)

\(andmap\(lambda\(io\)\(equal?\(interpt\(cario\)\)\(cdrio\)\)\)io\-pairs\)\)\)\)

;;Oneweightedbankperdecayvalue\.Themacroduplicatesthebody

;;sothateachrelationgetsitsowncanonicalcachecell\.

\(define\-syntax\-rule\(define\-arith\-bank\-wnamed\)

\(defrel/bank\-w\(namee\)

\#:prune\(arith\-keye\)

\#:decayd

\(conde\-w

\[\(==e’x\)\]\[\(==e0\)\]\[\(==e1\)\]

\[\(fresh\-w\(lr\)\(conde\-w\[\(==e‘\(plus,l,r\)\)\]\[\(==e‘\(times,l,r\)\)\]\)

\(namel\)\(namer\)\)\]\)\)\)

\(define\-arith\-bank\-wbank\-w/0900\.9\)

\(define\-arith\-bank\-wbank\-w/0750\.75\)

\(define\-arith\-bank\-wbank\-w/0500\.5\)

\(define\-arith\-bank\-wbank\-w/0250\.25\)

\(define\-arith\-bank\-wbank\-w/0100\.1\)

\(definedecay\-banks

‘\(\(0\.9\.,bank\-w/090\)

\(0\.75\.,bank\-w/075\)

\(0\.5\.,bank\-w/050\)

\(0\.25\.,bank\-w/025\)

\(0\.1\.,bank\-w/010\)\)\)

\(defineprefix\-length50\)

\(definetarget\-io’\(\(2\.9\)\(3\.16\)\(4\.25\)\)\);\(1\+x\)^2

\(define\(time\-itthunk\)

\(collect\-garbage\)

\(definestart\(current\-inexact\-milliseconds\)\)

\(defineresult\(thunk\)\)

\(defineelapsed\(\-\(current\-inexact\-milliseconds\)start\)\)

\(valuesresultelapsed\)\)

\(module\+main

\(printf”Decay\-factorexperiment\(inputs:~v\)~n”inputs\)

\(printf”Prefixlength:~a~n~n”prefix\-length\)

;;\(1\)enumeration\-orderprefixes,comparedpairwise

\(defineprefixes

\(for/list\(\[db\(in\-listdecay\-banks\)\]\)

\(definebank\(cdrdb\)\)

\(cons\(cardb\)\(run\-wprefix\-length\(e\)\(banke\)\)\)\)\)

\(define\(first\-diffxsys\)

\(letloop\(\[xsxs\]\[ysys\]\[i0\]\)

\(cond\[\(or\(null?xs\)\(null?ys\)\)\(if\(equal?xsys\)\#fi\)\]

\[\(equal?\(carxs\)\(carys\)\)\(loop\(cdrxs\)\(cdrys\)\(\+i1\)\)\]

\[elsei\]\)\)\)

\(printf”pairwisecomparisonofthe~a\-representativeprefixes:~n”prefix\-length\)

\(for\*\(\[p\(in\-listprefixes\)\]

\[q\(in\-listprefixes\)\]

\#:when\(<\(carp\)\(carq\)\)\)

\(defined\(first\-diff\(cdrp\)\(cdrq\)\)\)

\(printf”decay=~avsdecay=~a:~a~n”

\(carp\)\(carq\)

\(ifd\(format”firstdifferenceatposition~a”\(\+d1\)\)”IDENTICAL”\)\)\)

;;Samesetofrepresentatives,onlypermuted?

\(printf”prefixesassets\(sorted\):~n”\)

\(define\(prefix\-setp\)\(sort\(map\(lambda\(t\)\(format”~v”t\)\)\(cdrp\)\)string<?\)\)

\(defineref\-set\(prefix\-set\(carprefixes\)\)\)

\(for\(\[p\(in\-list\(cdrprefixes\)\)\]\)

\(printf”decay=~a:~asetofrepresentativesasdecay=~a~n”

\(carp\)

\(if\(equal?\(prefix\-setp\)ref\-set\)”SAME””DIFFERENT”\)

\(car\(carprefixes\)\)\)\)

;;\(1b\)weight\-classstructure:foreachdecay,extracttheraw

;;weightofeachemittedcellandrecoveritsexponentn\(the

;;numberofdecayapplications\)asround\(logw/logd\)\.Ifthe

;;classorderisinvariant,theexponentsequencescoincideacross

;;decaysevenwherethewithin\-classtermorderdiffers\.

\(defineexponent\-seqs

\(for/list\(\[db\(in\-listdecay\-banks\)\]\)

\(defined\(cardb\)\)

\(definebank\(cdrdb\)\)

\(definecells

\(with\-memo\-session

\(take\-wprefix\-length\(\(call/fresh\(lambda\(q\)\(bankq\)\)\)empty\-state\)\)\)\)

\(consd\(map\(lambda\(cell\)

\(inexact\-\>exact\(round\(/\(log\(carcell\)\)\(logd\)\)\)\)\)

cells\)\)\)\)

\(defineref\-exps\(cdr\(carexponent\-seqs\)\)\)

\(printf”weight\-exponentsequences\(classstructure\):~n”\)

\(printf”decay=~a:~a~n”\(car\(carexponent\-seqs\)\)ref\-exps\)

\(for\(\[es\(in\-list\(cdrexponent\-seqs\)\)\]\)

\(printf”decay=~a:~a~n”

\(cares\)

\(if\(equal?\(cdres\)ref\-exps\)”IDENTICAL”\(cdres\)\)\)\)

;;\(2\)timingonthe\(1\+x\)^2target

\(printf”~nTimingontarget\(1\+x\)^2:~n”\)

\(for\(\[db\(in\-listdecay\-banks\)\]\)

\(definebank\(cdrdb\)\)

\(define\-values\(resultelapsed\)

\(time\-it\(lambda\(\)\(run\-w1\(e\)\(banke\)\(matchesetarget\-io\)\)\)\)\)

\(printf”decay=~a:~ams~v~n”

\(cardb\)\(real\-\>decimal\-stringelapsed1\)result\)\)\)