Count the inhabitants a search node reaches, from the tree and from the program - #106
Merged
Conversation
…he program A search that is meant to draw from a chosen distribution cannot pick clauses uniformly. The uniform choice ignores how many inhabitants lie below each child, so it concentrates the sample on the terms the grammar reaches quickly and never reaches the long ones, whatever distribution was intended. Weighting the choice needs a count per child, and the package had no way to produce one. cosy.search.counting supplies that count in two constructions, which arrive at the same numbers and differ in what they cost and what they assume. - branch_counts materializes the retained derivation tree and counts its success branches per cost value. It needs no hypothesis about the program and it costs the number of inhabitants, since the counts have to be complete before anything can be drawn. The recursion is iterative and carries the size of each partial inhabitant along, so a node whose partial inhabitant already exceeds the bound is cut without being measured again. The bound on term size is what makes the retained tree finite, on a recursive space as well, because every expansion fixes at least one function symbol that every completion below it shares. - size_table computes the same numbers from the program: one row N_A(s) per non-terminal and size, filled by increasing s, at a cost in the size of the program and the bound alone. Every clause writes at least its terminal, so row s depends only on rows below it and one pass by increasing size suffices. The fill walks the sizes a non-terminal actually occupies rather than every size below the total, and it stops at the largest term the program has rather than at the bound, which is exact on an acyclic program and saturates at the bound on a recursive one. A clause of three holes or more is convolved through suffix rows, so the memory stays in the size of the program rather than in the number of distinct hole tuples. The table is offered with its condition and never without it. It is indexed by the non-terminal, so it cannot see a predicate that reads a hole: such a predicate makes the residual at that hole a proper subset of the hole's language, and the table then counts terms the space does not contain. decomposable_or_raise decides this and names the offending clauses and their argument positions rather than returning numbers that are quietly too large. The condition is necessarily conservative, because a predicate is an opaque callable and which variables it reads is recorded nowhere, so a clause counts as offending as soon as it carries a predicate and a named non-terminal argument. A predicate over the literals of its clause alone is not reported, and the fill drops the clauses it rejects, exactly as the engine does. assert_unambiguous_within decides the hypothesis under which the branch counts at the root are the number of inhabitants rather than the number of derivations. It costs a full traversal, so it is a validation tool and no counting path runs it. The tests check both constructions against exhaustive enumeration rather than against each other. The oracle builds every term over a signature up to the bound and asks contains_tree which of them the space contains, so it shares no machinery with the recursion it validates; it lives in tests/_generate_and_check.py, next to the reference spaces it enumerates. The reference spaces grow by the shapes the counts have to be right on: a space with a closed form, an ambiguous one that derives one term twice, a space whose clauses write two symbols each, and one space per shape of predicate that decides whether the table applies. The space whose clauses write two symbols is named two_symbol_clause_space rather than after its literals, since literal_space already names the space with a constant argument beside a non-terminal one. Three things the table form got wrong, found while testing it and fixed here rather than carried in. - A hole whose sort the program never derives raised a KeyError instead of counting as empty. The synthesis does not prune, so a clause whose argument type turned out uninhabited survives and names a sort that never becomes a head. The tree form already reads such a hole as empty, and the fill carries the same guard one step further on, but the pass that decides where to stop filling ran before it and subscripted the reach of a sort it had never seen. - A stored tail row stopped at the largest term any *sort* has, which is short of what the tail itself reaches whenever the clause that splits into it derives nothing: that clause is what would carry the tail's reach up to its head. The table then answered two different numbers for one convolution, depending on whether the tuple happened to be a stored tail, and a caller filling holes from the left asks for exactly the stored ones. The stopping point is now the reach of the rows that are kept, sorts and tails alike. - A filled table is shared between readers and its rows refuse assignment, but the mapping holding them did not, so one reader could rebind a whole row under its sort and leave the convolution cache answering from the numbers that were there before. Both mappings are read-only views now. A suffix is only ever a tail and never the head of a split, so the occupancy list that was kept for each one was written every round and never read. It is gone. Two reference spaces are here because a mutation run showed the suite could not tell the fill from a broken one without them. `ternary_space` has a clause of three holes, which is the only shape whose convolution needs a row for the tail of the clause: with every space having at most two holes, that whole path ran under the suite without a single test reaching it. `mixed_arity_space` writes into one size from two clauses at once, which is what says that a size is recorded as occupied once per row rather than once per clause. Both are checked against closed forms, the ternary Catalan numbers and a count this file computes by hand.
![tudo-seal-workflows[bot]](https://avatars.githubusercontent.com/in/2312552?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Benchmark CoSy
Details
| Benchmark suite | Current: 531b379 | Previous: be71b5d | Ratio |
|---|---|---|---|
benchmarks/test_benchmark_maximal_elements.py::test_benchmark_maximal_elements |
9.88421579211616 iter/sec (stddev: 0.0005093223282924836) |
9.608281351562356 iter/sec (stddev: 0.010017085420616013) |
0.97 |
benchmarks/test_benchmark_maze.py::test_benchmark_maze |
4.192933768470181 iter/sec (stddev: 0.017375647640240622) |
3.9235166334572096 iter/sec (stddev: 0.018797551923491352) |
0.94 |
benchmarks/test_benchmark_maze_contains.py::test_benchmark_maze_contains |
3.8954035895526973 iter/sec (stddev: 0.014869210471046624) |
3.5391214334611916 iter/sec (stddev: 0.025877608823890046) |
0.91 |
benchmarks/test_benchmark_maze_loopfree.py::test_benchmark_maze_loopfree |
4.180229054062536 iter/sec (stddev: 0.012761972443776212) |
3.8477221717914887 iter/sec (stddev: 0.02072136799063595) |
0.92 |
This comment was automatically generated by workflow using github-action-benchmark.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #106 +/- ##
===========================================
+ Coverage 84.25% 86.02% +1.77%
===========================================
Files 56 60 +4
Lines 5056 5933 +877
Branches 616 718 +102
===========================================
+ Hits 4260 5104 +844
- Misses 699 729 +30
- Partials 97 100 +3
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
mrhaandi
approved these changes
Aug 27, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem:
Random search is best-first search under a randomizing cost function, and two things are asked of
it: every prefix of its stream is a sample from a chosen distribution, and it draws without
replacement. A search that picks clauses uniformly delivers neither. The uniform choice ignores
how many inhabitants lie below each child, so it concentrates the sample on the terms the grammar
reaches quickly and never reaches the long ones, whatever distribution was intended. Weighting the
choice needs a count per child and per cost value, and nothing in the package produces one.
Changes:
A new module
cosy.search.counting, with ten of its names re-exported from the package. It isadditive: nothing but the package
__init__imports it and no behavior changes.branch_countsmaterializes the retained derivation tree of a query and counts its successbranches per cost value. It assumes nothing about the program and takes any computable cost
function. The recursion is iterative and carries the size of each partial inhabitant along, so a
node that already exceeds the bound is cut without being measured again. The bound on term size is
what makes the tree finite, on a recursive space as well, because every expansion fixes at least
one function symbol that every completion below it shares.
size_tablecomputes the same numbers from the program instead: one rowN_A(s)per non-terminaland size, filled by increasing
s. Every clause writes at least its terminal, so rowsdependsonly on rows below it and one pass suffices. The fill walks the sizes a non-terminal actually
occupies rather than every size below the total, and it stops at the largest term the program has
rather than at the bound. A clause of three holes or more is convolved through a row for its tail,
so the memory stays in the size of the program rather than in the number of distinct hole tuples.
This is what makes a generous bound affordable: on the list space the tree form reaches a bound of
12 in 46 s holding 531 440 nodes, while the table answers a bound of 400 in 0.2 ms and agrees with
the closed form
3^(s-1)throughout.decomposable_or_raisedecides the condition under which the second construction is valid. Atable indexed by the non-terminal cannot see a predicate that reads a hole, since such a predicate
makes the residual at that hole a proper subset of the hole's language and the table then counts
terms the space does not contain. The check names the offending clauses and their argument
positions rather than returning numbers that are quietly too large, and there is no fallback: a
caller who hits it uses the tree form, which needs no hypothesis. It is necessarily conservative,
because a predicate is an opaque callable and which variables it reads is recorded nowhere, so a
clause counts as offending as soon as it carries a predicate and a named non-terminal argument. A
predicate over the literals of its clause alone is not reported, and the fill drops the clauses it
rejects exactly as
Goal.from_rhs_ruleandGoal.updatedo.assert_unambiguous_withindecides the second condition, the one under which the counts at theroot are the number of inhabitants rather than the number of derivations. It costs a full
traversal of the retained tree, so it is a validation tool and no counting path runs it.
branch_multiplicitiesreports the witnesses it names.A hole whose sort the program never derives counts as empty rather than raising.
construct_solution_spacedoes not prune, so a clause whose argument type turned out uninhabitedsurvives and names a sort that never becomes a head, and both constructions read such a hole the
same way. A filled table is shared between readers, so its rows and the mappings holding them are
read-only: rebinding a row would leave the convolution cache answering from the numbers that were
there before.
The reference spaces in
tests/search_fixtures.pygrow by the shapes the counts have to be righton, and the membership oracle they are checked against moves to
tests/_generate_and_check.py,beside them. It builds every term over a signature up to the bound and asks
contains_treewhichof them the space contains, so it shares no machinery with the recursion it validates. The space
whose clauses write two symbols each is named
two_symbol_clause_spacerather than after itsliterals, since
literal_spacealready names the space with a constant argument beside anon-terminal one.