Check predicates of rules without a named non-terminal argument - #96
Merged
Conversation
The predicates of a rule are stored under the tuple of positions of its named
non-terminal arguments, and the goal cascade evaluates them once all of those
positions are grounded. A rule without a named non-terminal argument has no such
tuple. Storing its predicates under the empty tuple is no alternative either,
because the cascade indexes its keys with `ps[0][:-1]`. Nothing was stored, so
nothing was checked: `from_rhs_rule` decided a ground rule directly, but only at
the root of a derivation, and `update` had no such case at all.
Two rule shapes were therefore applied unchecked by the resolution:
* a rule whose non-terminal arguments are all unnamed -- the shape a component
whose suffix is an arrow type produces -- at every position, and
* a ground rule at every position below the root.
`enumerate_trees` and `contains_tree` evaluate the predicates of such a rule on
its literal substitution and reject the resulting terms. The resolution was thus
the only one of the three procedures that answered differently, and it derived
terms that `contains_tree` denied were in the solution space.
Decide these predicates where the rule is applied, on the literal substitution
of the rule. That is the whole substitution they can see: as the docstring of
`resolution` states, the predicates of a rule are applied to the substitution
given by its constant arguments and its named non-terminal arguments, and an
unnamed argument carries no name a predicate could read. A rule without a named
non-terminal argument is decidable as soon as it is formed.
The substitution the ground-rule check at the root used to run on,
`dict(grounded.values()) | rhs.literal_substitution`, is the same dict as
`rhs.literal_substitution` alone: at that point `grounded` holds exactly the
constant arguments of the rule, so the union lets the literal substitution win
every key it contributes. Had it not, a predicate would receive a `Tree` for a
constant name, where `enumerate_trees` and `contains_tree` pass the raw value.
Rules whose predicates read a derived subterm are untouched. Such a predicate
reads the name of a named non-terminal argument, and a rule that has one keeps
taking the existing storage path.
One consequence is worth spelling out. A recursive repository whose only base
rule is forbidden by its predicate has no term at all, and the depth-first
search now says so by not terminating, where before it answered with a term the
repository forbids. That is what a semi-decidable search does on a query without
an answer; `max_depth` bounds it, and `enumerate_trees` terminates on the same
repository because it works bottom-up. `prune` does not help here: it derives
productivity from the shape of a rule alone, so a rule its predicate forbids
still counts as a base case.
The new tests cover both shapes at the root and below it, with one and with two
predicates per rule, built by hand and once through a specification whose suffix
is an arrow type.
![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: b10de34 | Previous: be71b5d | Ratio |
|---|---|---|---|
benchmarks/test_benchmark_maximal_elements.py::test_benchmark_maximal_elements |
9.30736814895611 iter/sec (stddev: 0.002276356541883544) |
9.608281351562356 iter/sec (stddev: 0.010017085420616013) |
1.03 |
benchmarks/test_benchmark_maze.py::test_benchmark_maze |
3.925493739416904 iter/sec (stddev: 0.020397060989096376) |
3.9235166334572096 iter/sec (stddev: 0.018797551923491352) |
1.00 |
benchmarks/test_benchmark_maze_contains.py::test_benchmark_maze_contains |
3.7656390037995258 iter/sec (stddev: 0.012796793585081111) |
3.5391214334611916 iter/sec (stddev: 0.025877608823890046) |
0.94 |
benchmarks/test_benchmark_maze_loopfree.py::test_benchmark_maze_loopfree |
3.9440951552460803 iter/sec (stddev: 0.011750655478563006) |
3.8477221717914887 iter/sec (stddev: 0.02072136799063595) |
0.98 |
This comment was automatically generated by workflow using github-action-benchmark.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #96 +/- ##
===========================================
+ Coverage 73.02% 74.38% +1.35%
===========================================
Files 39 40 +1
Lines 2944 3080 +136
Branches 494 502 +8
===========================================
+ Hits 2150 2291 +141
+ Misses 686 683 -3
+ Partials 108 106 -2
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 20, 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:
The resolution derives terms that
contains_treedenies are in the solution space. Three linesof rules are enough to show it on
develop:The predicate says the digit must be positive.
enumerate_treesobeys it and returns nothing;contains_treeobeys it and answersFalsefor the only term the resolution produced. Theresolution is the odd one out.
breadth_first_resolutionanswers likedepth_first_resolution,and
sample_treedraws from the same stream, so it returns a term its own repository forbids.Two rule shapes are affected, and both are reachable from the public front end.
A rule whose non-terminal arguments are all unnamed. The synthesizer names the arguments a
component declares with
argument(...); the arguments it derives from an arrow inside the suffixstay unnamed. A component with a constraint and an arrow suffix therefore produces exactly this
shape:
A ground rule below the root: This one needs no arrow at all. It is the repository from the
repo above. At the root the resolution decided such a rule. One combinator on top of it was
enough to bypass the check.
Cause:
Goalstores the predicates of a rule under the tuple of positions of the rule's namednon-terminal arguments, and evaluates them once every one of those positions is grounded:
If
namedis empty there is no key. Storing the predicates under the empty tuple is noalternative either: the cascade that fires the stored predicates indexes its keys with
ps[0][:-1], which an empty tuple cannot answer. So nothing was stored, and nothing was fired.That left one special case as the entire check:
from_rhs_ruledecided a rule directly when itproduced no subgoals at all. It applies only to a ground rule, and only at the root of a
derivation, because it lives in
from_rhs_ruleandupdatehas no counterpart. A rule withunnamed holes never reached it, and neither did a ground rule anywhere below the root.
enumerate_treesandcontains_treehave no such gap. Both build the substitution for a rulefrom its named non-terminal arguments plus its literal substitution -- if there are no named
arguments, that is the literal substitution -- and both apply the predicates to it.
What changes:
Decide these predicates where the rule is applied, in both places, on
rhs.literal_substitution:That is the whole substitution such a predicate can see, and the file says so itself. From the
docstring of
resolution:A rule without a named non-terminal argument therefore has a substitution consisting of its
constant arguments alone, which is exactly
literal_substitution. Its predicates are decidable assoon as the rule is formed, and both
enumerate_treesandcontains_treealready decide themthat way.
The change also drops the substitution the old root check ran on,
dict(grounded.values()) | rhs.literal_substitution. That is the same dict asrhs.literal_substitutionalone: at that pointgroundedhas been filled fromConstantArgumentsonly, so it has the same key set as
literal_substitution, and the union lets the literalsubstitution win every key. Checked over 1885 systematically generated rule shapes (0-3 arguments,
duplicate constant names included): no difference, same key order, and no
Treein either result.The order matters and is now fixed by construction: written the other way round, a predicate would
receive
Tree(value, ())for a constant name, whereasenumerate_trees(specific_substitution ... | rule.literal_substitution) andcontains_tree(child.rootfor aConstantArgument) handit the raw value. The existing tests rely on that: the predicate in
tests/test_overlapping_substitution_inference.pycomparesvs["n"]against42, which aTreewould never equal.
from_rhs_rulenow also documents when it returnsNone, in the wording its siblingupdatealready uses.