Coinduction handler for the recursive solver #690
Conversation
|
@nikomatsakis FYI PR #683 that you wanted to have a look at was closed in favour of this PR. |
There was a problem hiding this comment.
Sorry @firefighterduck for not reviewing earlier. I'm posting some random comments that had accrued, but don't feel the need to respond to them -- I want to give this another pass today. I have this "feeling" like there's a simplification possible, but I'm having a hard time articulating precisely what I mean so I need to block out some time for that.
book/src/recursive/coinduction.md
Outdated
| This search for a disproof is done by the standard recursive solving process described in the sub-chapters before. | ||
|
|
||
| Albeit this approach would allow for the handling of mixed inductive/co-inductive cycles, these are actually handled as errors to prevent propagation of the assumed provability outside of the coinductive cycle. |
There was a problem hiding this comment.
| Albeit this approach would allow for the handling of mixed inductive/co-inductive cycles, these are actually handled as errors to prevent propagation of the assumed provability outside of the coinductive cycle. | |
| Although this approach would allow for the handling of mixed inductive/co-inductive cycles, these are actually handled as errors to prevent propagation of the assumed provability outside of the coinductive cycle. |
Albeit is an odd word to use here -- I think maybe yo mean "Allow"? In general I had a hard time figuring out just what this paragraph means though.
chalk-recursive/src/lib.rs
Outdated
| pub(crate) struct Minimums { | ||
| pub(crate) positive: DepthFirstNumber, | ||
| pub(crate) coinductive_cycle_starts: FxHashSet<DepthFirstNumber>, |
There was a problem hiding this comment.
do we really need a set of starts
There was a problem hiding this comment.
Some kind of over-approximation by an upper and a lower bound DFN would probably work here as well. If then a cycle start depends on another cycle start, all results inside the inner cycle could simply be dropped, as tracking the precise dependencies would be rather cumbersome.
There was a problem hiding this comment.
I was able to exchange the set for two bounds. The upper bound represents the current innermost cycle whereas the lower bound represents whether there exists an intercycle dependency.
firefighterduck
force-pushed
the
recursive-coinduction-handler
branch
from
3a097cc to
3df6b42
Compare
| pub(crate) struct CoinductionHandler<I: Interner> { | ||
| /// Heap of start DFNs for nested cycles. | ||
| /// The innermost cycle start is the first element in the heap. | ||
| cycle_start_dfns: BinaryHeap<DepthFirstNumber>, |
There was a problem hiding this comment.
This heap could also be vector that then needs to be sorted after every insertion. Otherwise, the order in which goals are evaluated would matter for intercycle dependencies.
|
I'm going to close this PR for now in favor of the other approach. |
This PR is meant to address the issue of false positives in coinductive cycles as described in #399 . It also fixes the two coinduction tests related to that issue (i.e.
coinductive_unsound1andcoinductive_multicycle4). As such it is an improved version of #683 .The PR adds a dedicated handler mechanisms for delaying insertion of results into the cache if they occur inside a coinductive cycle. This is done by tracking dependencies of result to coinductive assumptions (via the
Minimums) and storing those "premature" results in a temporary cache. The exact mechanism is also described in the corresponding book chapter. In general, it follows the idea from #399 to start with a positive result instead of the negative one but delays its effects on other goals until it is know whether this assumption was correct.