Skip to content

Add best-first search with the cost orders and algebras it searches by - #112

Merged
FelixLaarmann merged 1 commit into
developfrom
feature/cost-orders
Sep 2, 2026
Merged

Add best-first search with the cost orders and algebras it searches by#112
FelixLaarmann merged 1 commit into
developfrom
feature/cost-orders

Conversation

@FelixLaarmann

Copy link
Copy Markdown
Member

Problem:

The search rules of the package are uninformed. depth_first and breadth_first read the order of
their stream off the shape of the derivation tree, and nothing lets a caller order a search by a
cost on the search nodes instead. Random search is already an informed search, but its frontier is
a heap over reals written out inside sampling.py, with no general form behind it and nothing that
states what a cost function must satisfy for the search to remain sound and complete.

Changes:

  • A new module cosy.search.costs, with sixteen of its names re-exported from the package. It
    carries three layers, separable on purpose.
  • The cost order a cost function maps into. Partial by default, since a search node may carry
    incomparable costs, and strengthened to a positively ordered commutative monoid wherever costs
    are summed. Reals for an order without addition, NonNegativeReals and ComponentwiseTuples
    for the domains that sum.
  • The best-first frontier, whose pop returns a node that no node of the frontier lies strictly
    below. LinearScanFrontier in general, HeapFrontier where the order is total, and
    best_first_frontier picks between them so that no caller has to remember which domains admit a
    heap.
  • The additive cost algebras, which read a search node as the partial inhabitant it denotes and
    split its cost into the cost so far and the estimate of what its holes still add.
  • best_first is the search rule the three build up to, run under uniform_cost, greedy or
    a_star. It takes no clause order, because the pop selects by cost alone, and it fixes the
    computation rule to the one the two uninformed rules use.
  • Soundness holds on every space. Completeness needs every cost-bounded set to be finite, and cost
    order needs a cost function that never falls along a branch. Both are properties of the cost
    function rather than of the search, so uniform_cost supplies them and greedy does not.
    assert_uniform_cost_complete decides the first of the two for a given symbol family.
  • The cost domains reject a value that leaves their carrier, at the argument and at the result of
    an addition. A monoid is closed under its operation, so an overflowing sum is reported where it
    arises rather than by the next operation to receive it.
  • The module docstring of sampling.py now names the two frontier classes it described in the
    abstract. Its own heap is the total-order fast path written out in place.

The search rules of the package are uninformed. depth_first and breadth_first read the order of
their stream off the shape of the derivation tree, and nothing lets a caller order a search by a
cost on the search nodes instead. Random search is already informed, but its frontier is a heapq
over reals written out inside sampling.py, with no general form behind it and nothing that states
what a cost function has to be for the search to stay sound and complete.

A new module cosy.search.costs, with sixteen of its names re-exported from the package. It carries
three layers, separable on purpose. The cost order a cost function maps into, partial by default
and strengthened to a positively ordered commutative monoid wherever costs are summed. The
best-first frontier over it, whose pop returns a node that no node of the frontier lies strictly
below, as a linear scan in general and as a binary heap where the order is total. And the additive
cost algebras, which read a search node as the partial inhabitant it denotes and split its cost
into the cost so far and the estimate of what its holes still add.

best_first is the search rule the three build up to, run under uniform_cost, greedy or a_star. It
takes no clause order, because the pop selects by cost alone, and it fixes the computation rule to
the one the two uninformed rules use.

The order stays partial throughout, and that is where the subtle mistakes live. Best-first search
pops a minimal node and not a least one, several incomparable minima may exist at once, and the
cost-bounded sets that carry completeness collect the nodes whose cost is not strictly above the
bound, which over a partial order is weaker than "at most the bound". Soundness holds on every
space. Completeness needs every cost-bounded set to be finite, and cost order needs a cost function
that never falls along a branch. Both are properties of the cost function rather than of the search,
so uniform_cost supplies them and greedy does not.

The two cost domains reject a value that leaves their carrier, at the argument and at the result of
an addition. A monoid is closed under its operation, so an overflowing sum is reported where it
arises rather than by the next operation to receive it.

The module docstring of sampling.py now names the two frontier classes it described in the abstract.
Its own heap is the total-order fast path written out in place.

@tudo-seal-workflows tudo-seal-workflows Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Benchmark CoSy

Details
Benchmark suite Current: 9cc2bfd Previous: be71b5d Ratio
benchmarks/test_benchmark_maximal_elements.py::test_benchmark_maximal_elements 10.549892760483873 iter/sec (stddev: 0.00016046166696687814) 9.608281351562356 iter/sec (stddev: 0.010017085420616013) 0.91
benchmarks/test_benchmark_maze.py::test_benchmark_maze 4.469599573329848 iter/sec (stddev: 0.010452029992877749) 3.9235166334572096 iter/sec (stddev: 0.018797551923491352) 0.88
benchmarks/test_benchmark_maze_contains.py::test_benchmark_maze_contains 4.248682767922877 iter/sec (stddev: 0.015905390729716647) 3.5391214334611916 iter/sec (stddev: 0.025877608823890046) 0.83
benchmarks/test_benchmark_maze_loopfree.py::test_benchmark_maze_loopfree 4.506064942615535 iter/sec (stddev: 0.011333250950426203) 3.8477221717914887 iter/sec (stddev: 0.02072136799063595) 0.85

This comment was automatically generated by workflow using github-action-benchmark.

@codecov-commenter

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 99.79360% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 92.53%. Comparing base (12a587e) to head (9cc2bfd).
✅ All tests successful. No failed tests found.

Files with missing lines Patch % Lines
tests/test_costs.py 99.69% 0 Missing and 2 partials ⚠️
Additional details and impacted files
@@             Coverage Diff             @@
##           develop     #112      +/-   ##
===========================================
+ Coverage    91.70%   92.53%   +0.83%     
===========================================
  Files           76       78       +2     
  Lines         8398     9367     +969     
  Branches       868      959      +91     
===========================================
+ Hits          7701     8668     +967     
  Misses         623      623              
- Partials        74       76       +2     
Flag Coverage Δ
macos-latest-3.10 92.50% <99.79%> (+0.84%) ⬆️
macos-latest-3.11 92.52% <99.79%> (+0.83%) ⬆️
macos-latest-3.12 92.52% <99.79%> (+0.83%) ⬆️
macos-latest-3.13 92.52% <99.79%> (+0.83%) ⬆️
ubuntu-latest-3.10 92.50% <99.79%> (+0.84%) ⬆️
ubuntu-latest-3.11 92.52% <99.79%> (+0.83%) ⬆️
ubuntu-latest-3.12 92.52% <99.79%> (+0.83%) ⬆️
ubuntu-latest-3.13 92.52% <99.79%> (+0.83%) ⬆️
windows-latest-3.10 92.50% <99.79%> (+0.84%) ⬆️
windows-latest-3.11 92.52% <99.79%> (+0.83%) ⬆️
windows-latest-3.12 92.52% <99.79%> (+0.83%) ⬆️
windows-latest-3.13 92.52% <99.79%> (+0.83%) ⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@FelixLaarmann
FelixLaarmann merged commit 8671ad4 into develop Sep 2, 2026
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants