From a44defccbb439899f38c575591f8d81ee6432e0b Mon Sep 17 00:00:00 2001 From: Jack Date: Thu, 6 Feb 2020 20:30:36 -0500 Subject: [PATCH 1/8] Initial draft of engine book --- book/src/SUMMARY.md | 2 + book/src/engine.md | 16 ++++++- book/src/engine/logic.md | 62 +++++++++++++++++++++++++++ book/src/engine/major_concepts.md | 69 +++++++++++++++++++++++++++++++ 4 files changed, 147 insertions(+), 2 deletions(-) create mode 100644 book/src/engine/logic.md create mode 100644 book/src/engine/major_concepts.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 226bd7443a8..581a969c48a 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -14,4 +14,6 @@ - [Lowering Rust IR to logic](./clauses.md) - [Unification and type equality](./clauses/type_equality.md) - [How does the engine work](./engine.md) + - [Major concepts](./engine/major_concepts.md) + - [Logic](./engine/logic.md) - [Glossary and terminology](./glossary.md) diff --git a/book/src/engine.md b/book/src/engine.md index ed5e427b282..2145c3de911 100644 --- a/book/src/engine.md +++ b/book/src/engine.md @@ -1,3 +1,15 @@ -# How does the engine work +# Chalk engine -*TBD:* Explain how chalk-engine +The `chalk-engine` crate is the core PROLOG-like solver for logical predicates. Importantly, it is very general and not specific to Rust, Rust types, or Rust logic. + +## Implemented PROLOG concepts + +The engine implements the following PROLOG logic concepts. Some of these have been published on previously, and some a `Chalk`-specific. This isn't necesarily an exhaustive list: +- Basic logic +- Negation +- Floundering +- Coinductive solving + +## Note + +Throughout most of this chapter, the specifics in regards to `Canonicalization` and `UCanonicalization` are avoided. These are important concepts to understand, but don't particulary help to understand how `chalk-engine` *works*. In a few places, it may be highlighted if it *is* important. diff --git a/book/src/engine/logic.md b/book/src/engine/logic.md new file mode 100644 index 00000000000..739b389ec87 --- /dev/null +++ b/book/src/engine/logic.md @@ -0,0 +1,62 @@ +# Logic + +## Overview + +`chalk-engine` solves a `Goal` using a depth-first search. When asked to solve a particular `Goal` it hasn't seen before, it will first ask the [`Context`] to generate a set of program clauses, that get turned into `Strand`s, that could solve that goal. Otherwise, if asked to solve a `Goal` it has seen before, it will select the existing table. + +Once a table is selected, it will pick a `Strand` and a subgoal of that `Strand`, try to solve that `Goal`, repeating the process. + +When an `Answer` is found for a `Goal`, it is merged into the parent `Strand`, or returned if it was the root `Goal`. It will then go on to pick the next subgoal of the `Strand` and continue on. + +If at any point the solving stops being "successful" (i.e. we definitely found something to be unsolvable), the solving is restarted at the root `Goal`. + +## The stack + +In order to detect cycles (talked more about later), as well as keep track of the selected `Strand` for each table, `chalk-engine` stores a [`Stack`] on the `Forest`. Whenever a new goal is selected, a `StackEntry` is pushed onto the `Stack`, as well as the the "time" (which also gets incremented) that it was pushed. This "time" can be compared later to check if all the `Strands` of a `Table` have been checked in a single solve. + +As either `Answer`s are found for the selected `Table`, entries on the stack are `pop`ed. If something is found to be unsolvable, the complete stack is unwound. + +## Table creation + +As mentioned before, whenever a new `Goal` is encounted, a new `Table` is created to store current and future answers. First, the `Goal` is converted into an [`HhGoal`]. If it can be simplified, then a `Strand` with one or more subgoals will be generated and can be followed as above. Otherwise, if it is a `DomainGoal` (see above), then [`program_clauses`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html#tymethod.program_clauses) is called and each clause is converted into a `Strand` and can be followed. + +## `root_answer` and `ensure_root_answer` + +The `root_answer` function is the entry point to solve a `Goal`. Up until now, the idea of `Answer` versus `CompleteAnswer` have been ignored. However, in reality `Answer`s to `Goal`s may actually have delayed subgoals (see `ExClause` and `Coinduction and refinement strands`), whereas `CompleteAnswer`s may not. `root_answer` essentially just wraps `ensure_root_answer` and converts the `Goal`'s `Answer` to a `CompleteAnswer`. + +The `ensure_root_answer` function contains to core skeleton of the logic around `Strand` and subgoal selection. The majority of the logic, however, is split out into separate functions that branch out from `ensure_root_answer`. + +## Subgoal selection + +Once a given `Strand` for a table has been selected, a subgoal has to be selected. If there are no subgoals left, then there is nothing to do. Otherwise, if there are subgoals left, then a subgoal will attempt to be selected (from [`next_subgoal_index`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#tymethod.next_subgoal_index)). If the table for that subgoal had previously floundered (see next section), then we mark that subgoal as floundered and try the next subgoal. If all subgoals are marked as floundered, then this entire `Strand` is marked as floundered. If a subgoal is successfully selected, there is nothing left to do. + +## Floundering + +There a couple cases where we "give up" - here called floundering - on trying to solve a goal. The most easy to understand case is if the types for a `Goal` or `Answer` are too large. (Side note, we *could* actually handle this - by generalizing - but turns out to be quite buggy and probably unnecessary). Another case where we flounder is if we try to solve a `Goal` where we try to **enumerate** non-enumerable types (like auto traits). In general, floundering just means that we *can't* know any more answers about a `Goal`, for some reason. However, if there are other `Strands` that don't flounder, there may still b other `Answer`s available. + +## Answers + +After an answer has been found for a subgoal, it must be *applied* to the parent `Strand`. Specifcally, it must be able to unify with any existing `Answers`. If the `Answer`s are incompatible, the `Strand` is dropped since it can't lead anywhere. + +## Cycles + +If while pursuing a `Goal`, the engine encounters the same `Table` twice, then a cycle has occured. If the cycle is not coinductive (see next), then there is nothing that can be gained from taking this route. We mark how far up the stack is in the cycle, and try the next `Strand`. If all `Strand`s for a table encounter a cycle, then we know that the current selected `Goal` has no more answers. + +## Coinduction and refinement strands + +Coinduction basically means that two statements can rely on each other being true, unless either is proven false. + +For example with the following program: +``` +#[coinductive] +trait C1 { } +forall { A: C1 if B: C1 } +``` +Then the goal `exists { T: C1 }` holds for all `T` and `U`. If the `C1` trait was not coinductive, this would be a simple cycle. + +To implement coinduction in the engine, delayed subgoals were introduced. Essentially, if a cycle is found, and the `Goal` is coinductive, then this is "delayed" until the stack unwinds back to the top `Goal` and all other non-coinductive cycles have been proven. Then, `Goal` has been proven itself. In some cases, it is the *root* `Goal` that has delayed coinductive subgoals (see above example). In this case, we create another "Refinement Strand" where the only subgoals are the delayed coinductive subgoals. If this new `Strand` can be proven, then any `Answer`s from that are valid answers for the root `Goal`. However, since there are currently delayed coinductive subgoals, there are no answers available yet. + + +[`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html +[`HhGoal`]: https://rust-lang.github.io/chalk/chalk_engine/hh/enum.HhGoal.html +[`Stack`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.Stack.html diff --git a/book/src/engine/major_concepts.md b/book/src/engine/major_concepts.md new file mode 100644 index 00000000000..601fc1f17f8 --- /dev/null +++ b/book/src/engine/major_concepts.md @@ -0,0 +1,69 @@ +# Major concepts + +This section goes over a few different concepts that are crucial to understanding how `chalk-engine` works, without going over the exact solving logic. + +## `Context`, `ContextOps`, and `InferenceTable` + +### `Context` + +The [`Context`] trait is the primary bridge between Chalk internal logic and external types. In addition actually *defining* the types (via associated types), it also contains associated functions to convert or extract information from those types. Overall, this allows the types to be basically opaque to the engine internals. Functions in trait are agnostic to specific program or environment details, since they lack a `&self` argument. + +To give an example, there is an associated `Goal` type. However, Chalk doesn't know how to solve this. Instead, it has to be converted an [`HhGoal`] via the `Context::into_hh_goal` function. This will be coverted more in the `Goals` section. + +### `ContextOps` + +The [`ContextOps`] trait contains functions that may specifically require information a specific program or environment. For example, the `program_clauses` function gives potential ways to prove a `Goal`, but obviously it requires knowing the program (for example, what types, traits, and impls there are). Functions in this trait all take a `&self` argument. + +### `InferenceTable` + +The [`InferenceTable`] is a super trait to the `UnificationOps`, `TruncateOps`, and `ResolventOps`. Each of these contains functions that track the state of specific parts of the program. Importantly, these operations can dynamically change the state of the logic itself. + +## Goals + +A "goal" in Chalk can be thought of as "something we want to prove". The engine itself understands [`HhGoal`]s. Goals of are consist of the most basic logic, such as introducing Binders (`Forall` or `Exists`) or combining goals (`All`). On the other `Context::Goal` represents an opaque goal generated externally. As such, it may contain any extra information or may be interned. When solving a logic predicate, Chalk will lazily convert `Context::Goal`s into `HHGoal`s. + +There are three types of completely opaque `HhGoal`s that Chalk can solve: `Unify`, `DomainGoal`, and `CannotProve`. Unlike the other types of goals, these three cannot be simiplified any further. `Unify` is the goal of unifying any two types. `DomainGoal` is any goal that can solve by applying a `ProgramClause`. To solve this, more `Goal`s may generated. Finally, `CannotProve` is a special goal that *cannot* be proven true or false. + +## Answers and Solutions + +For every `Goal`, there are zero or more `Answer`s. Each `Answer` contains values for the inference variables in the goal. + +For example, given the following program: +``` +trait Clone {} +struct A {} +struct B {} +impl Clone for A {} +impl Clone for B {} +``` +With the following goal: `exists { T: Clone }` +The following solutions would be given: +``` +T = A +T = B +``` +In other words, either `A` or `B` can substituted for `T` and the goal will hold true. Moreover, either answer could be used when further solving other goals that depend on this goal. + +However, oftentimes, this is not what external crates want when solving for a goal. Instead, the may want a *unique* solution to this goal. Indeed, when we solve for a given root `Goal`, we return a since [`Solution`]. It is up to the implementation of `Context` to decide how a `Solution` is made, given a possibly infinite set of answers. One of example of this is the [`AntiUnifier`](https://rust-lang.github.io/chalk/chalk_solve/solve/slg/aggregate/struct.AntiUnifier.html) from `chalk-solve`, which finds a minimal generalization of answers which don't unify. (For the example above, it would return only `Ambiguous`, since `A` and `B` can't unify.) + +## ExClauses and Strands + +An [`ExClause`] is described in literature as `A :- D | G` or `A holds given that G holds with D delayed goals`. In `chalk-engine`, an `ExClause` stores the current state of proving a goal, including existing substitutions already found, subgoals yet to be proven, or delayed subgoals. A [`Strand`] wraps both an `ExClause` and an [`InferenceTable`] together. + +## Tables and Forests + +A `Strand` represents a *single* direction to find an `Answer` - for example, an implementation of a trait with a set of where clauses. However, in a program, there may be *multiple* possible implementations that match a goal - e.g. multiple impls with different where clauses. Every [`Table`] has a goal, and stores existing `Answers`, as well as all `Strand`s that may result in more answers. + +A [`Forest`] holds all the `Table`s that program generates, and is what most of the logic is implemented on. It also stores the current state of solving (the stack). + + + +[`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html +[`ContextOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html +[`InferenceTable`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.InferenceTable.html +[`HhGoal`]: https://rust-lang.github.io/chalk/chalk_engine/hh/enum.HhGoal.html +[`Solution`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Solution +[`ExClause`]: https://rust-lang.github.io/chalk/chalk_engine/struct.ExClause.html +[`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html +[`Table`]: https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html +[`Forest`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html From e51b002dae277a37652e6343c9079c8c73aad238 Mon Sep 17 00:00:00 2001 From: Jack Date: Thu, 6 Feb 2020 20:44:42 -0500 Subject: [PATCH 2/8] Columns --- book/src/engine.md | 14 ++++- book/src/engine/logic.md | 95 +++++++++++++++++++++++++------ book/src/engine/major_concepts.md | 77 ++++++++++++++++++++----- 3 files changed, 152 insertions(+), 34 deletions(-) diff --git a/book/src/engine.md b/book/src/engine.md index 2145c3de911..c2613417989 100644 --- a/book/src/engine.md +++ b/book/src/engine.md @@ -1,10 +1,14 @@ # Chalk engine -The `chalk-engine` crate is the core PROLOG-like solver for logical predicates. Importantly, it is very general and not specific to Rust, Rust types, or Rust logic. +The `chalk-engine` crate is the core PROLOG-like solver for logical +predicates. Importantly, it is very general and not specific to Rust, +Rust types, or Rust logic. ## Implemented PROLOG concepts -The engine implements the following PROLOG logic concepts. Some of these have been published on previously, and some a `Chalk`-specific. This isn't necesarily an exhaustive list: +The engine implements the following PROLOG logic concepts. Some of these +have been published on previously, and some are `Chalk`-specific. This isn't +necesarily an exhaustive list: - Basic logic - Negation - Floundering @@ -12,4 +16,8 @@ The engine implements the following PROLOG logic concepts. Some of these have be ## Note -Throughout most of this chapter, the specifics in regards to `Canonicalization` and `UCanonicalization` are avoided. These are important concepts to understand, but don't particulary help to understand how `chalk-engine` *works*. In a few places, it may be highlighted if it *is* important. +Throughout most of this chapter, the specifics in regards to +`Canonicalization` and `UCanonicalization` are avoided. These are important +concepts to understand, but don't particulary help to understand how +`chalk-engine` *works*. In a few places, it may be highlighted if it *is* +important. diff --git a/book/src/engine/logic.md b/book/src/engine/logic.md index 739b389ec87..bed0d2a56bc 100644 --- a/book/src/engine/logic.md +++ b/book/src/engine/logic.md @@ -2,49 +2,100 @@ ## Overview -`chalk-engine` solves a `Goal` using a depth-first search. When asked to solve a particular `Goal` it hasn't seen before, it will first ask the [`Context`] to generate a set of program clauses, that get turned into `Strand`s, that could solve that goal. Otherwise, if asked to solve a `Goal` it has seen before, it will select the existing table. +`chalk-engine` solves a `Goal` using a depth-first search. When asked to solve a +particular `Goal` it hasn't seen before, it will first ask the [`Context`] to +generate a set of program clauses, that get turned into `Strand`s, that could +solve that goal. Otherwise, if asked to solve a `Goal` it has seen before, it +will select the existing table. -Once a table is selected, it will pick a `Strand` and a subgoal of that `Strand`, try to solve that `Goal`, repeating the process. +Once a table is selected, it will pick a `Strand` and a subgoal of that +`Strand`, try to solve that `Goal`, repeating the process. -When an `Answer` is found for a `Goal`, it is merged into the parent `Strand`, or returned if it was the root `Goal`. It will then go on to pick the next subgoal of the `Strand` and continue on. +When an `Answer` is found for a `Goal`, it is merged into the parent `Strand`, +or returned if it was the root `Goal`. It will then go on to pick the next +subgoal of the `Strand` and continue on. -If at any point the solving stops being "successful" (i.e. we definitely found something to be unsolvable), the solving is restarted at the root `Goal`. +If at any point the solving stops being "successful" (i.e. we definitely found +something to be unsolvable), the solving is restarted at the root `Goal`. ## The stack -In order to detect cycles (talked more about later), as well as keep track of the selected `Strand` for each table, `chalk-engine` stores a [`Stack`] on the `Forest`. Whenever a new goal is selected, a `StackEntry` is pushed onto the `Stack`, as well as the the "time" (which also gets incremented) that it was pushed. This "time" can be compared later to check if all the `Strands` of a `Table` have been checked in a single solve. +In order to detect cycles (talked more about later), as well as keep track of +the selected `Strand` for each table, `chalk-engine` stores a [`Stack`] on the +`Forest`. Whenever a new goal is selected, a `StackEntry` is pushed onto the +`Stack`, as well as the the "time" (which also gets incremented) that it was +pushed. This "time" can be compared later to check if all the `Strands` of a +`Table` have been checked in a single solve. -As either `Answer`s are found for the selected `Table`, entries on the stack are `pop`ed. If something is found to be unsolvable, the complete stack is unwound. +As either `Answer`s are found for the selected `Table`, entries on the stack are +`pop`ed. If something is found to be unsolvable, the complete stack is unwound. ## Table creation -As mentioned before, whenever a new `Goal` is encounted, a new `Table` is created to store current and future answers. First, the `Goal` is converted into an [`HhGoal`]. If it can be simplified, then a `Strand` with one or more subgoals will be generated and can be followed as above. Otherwise, if it is a `DomainGoal` (see above), then [`program_clauses`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html#tymethod.program_clauses) is called and each clause is converted into a `Strand` and can be followed. +As mentioned before, whenever a new `Goal` is encounted, a new `Table` is +created to store current and future answers. First, the `Goal` is converted into +an [`HhGoal`]. If it can be simplified, then a `Strand` with one or more +subgoals will be generated and can be followed as above. Otherwise, if it is a +`DomainGoal` (see above), then +[`program_clauses`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html#tymethod.program_clauses) +is called and each clause is converted into a `Strand` and can be followed. ## `root_answer` and `ensure_root_answer` -The `root_answer` function is the entry point to solve a `Goal`. Up until now, the idea of `Answer` versus `CompleteAnswer` have been ignored. However, in reality `Answer`s to `Goal`s may actually have delayed subgoals (see `ExClause` and `Coinduction and refinement strands`), whereas `CompleteAnswer`s may not. `root_answer` essentially just wraps `ensure_root_answer` and converts the `Goal`'s `Answer` to a `CompleteAnswer`. +The `root_answer` function is the entry point to solve a `Goal`. Up until now, +the idea of `Answer` versus `CompleteAnswer` have been ignored. However, in +reality `Answer`s to `Goal`s may actually have delayed subgoals (see `ExClause` +and `Coinduction and refinement strands`), whereas `CompleteAnswer`s may not. +`root_answer` essentially just wraps `ensure_root_answer` and converts the +`Goal`'s `Answer` to a `CompleteAnswer`. -The `ensure_root_answer` function contains to core skeleton of the logic around `Strand` and subgoal selection. The majority of the logic, however, is split out into separate functions that branch out from `ensure_root_answer`. +The `ensure_root_answer` function contains to core skeleton of the logic around +`Strand` and subgoal selection. The majority of the logic, however, is split out +into separate functions that branch out from `ensure_root_answer`. ## Subgoal selection -Once a given `Strand` for a table has been selected, a subgoal has to be selected. If there are no subgoals left, then there is nothing to do. Otherwise, if there are subgoals left, then a subgoal will attempt to be selected (from [`next_subgoal_index`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#tymethod.next_subgoal_index)). If the table for that subgoal had previously floundered (see next section), then we mark that subgoal as floundered and try the next subgoal. If all subgoals are marked as floundered, then this entire `Strand` is marked as floundered. If a subgoal is successfully selected, there is nothing left to do. +Once a given `Strand` for a table has been selected, a subgoal has to be +selected. If there are no subgoals left, then there is nothing to do. Otherwise, +if there are subgoals left, then a subgoal will attempt to be selected (from +[`next_subgoal_index`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#tymethod.next_subgoal_index)). +If the table for that subgoal had previously floundered (see next section), then +we mark that subgoal as floundered and try the next subgoal. If all subgoals are +marked as floundered, then this entire `Strand` is marked as floundered. If a +subgoal is successfully selected, there is nothing left to do. ## Floundering -There a couple cases where we "give up" - here called floundering - on trying to solve a goal. The most easy to understand case is if the types for a `Goal` or `Answer` are too large. (Side note, we *could* actually handle this - by generalizing - but turns out to be quite buggy and probably unnecessary). Another case where we flounder is if we try to solve a `Goal` where we try to **enumerate** non-enumerable types (like auto traits). In general, floundering just means that we *can't* know any more answers about a `Goal`, for some reason. However, if there are other `Strands` that don't flounder, there may still b other `Answer`s available. +There a couple cases where we "give up" - here called floundering - on trying to +solve a goal. The most easy to understand case is if the types for a `Goal` or +`Answer` are too large. (Side note, we *could* actually handle this - by +generalizing - but turns out to be quite buggy and probably unnecessary). +Another case where we flounder is if we try to solve a `Goal` where we try to +**enumerate** non-enumerable types (like auto traits). In general, floundering +just means that we *can't* know any more answers about a `Goal`, for some +reason. However, if there are other `Strands` that don't flounder, there may +still be other `Answer`s available. ## Answers -After an answer has been found for a subgoal, it must be *applied* to the parent `Strand`. Specifcally, it must be able to unify with any existing `Answers`. If the `Answer`s are incompatible, the `Strand` is dropped since it can't lead anywhere. +After an answer has been found for a subgoal, it must be *applied* to the parent +`Strand`. Specifcally, it must be able to unify with any existing `Answers`. If +the `Answer`s are incompatible, the `Strand` is dropped since it can't lead +anywhere. ## Cycles -If while pursuing a `Goal`, the engine encounters the same `Table` twice, then a cycle has occured. If the cycle is not coinductive (see next), then there is nothing that can be gained from taking this route. We mark how far up the stack is in the cycle, and try the next `Strand`. If all `Strand`s for a table encounter a cycle, then we know that the current selected `Goal` has no more answers. +If while pursuing a `Goal`, the engine encounters the same `Table` twice, then a +cycle has occured. If the cycle is not coinductive (see next), then there is +nothing that can be gained from taking this route. We mark how far up the stack +is in the cycle, and try the next `Strand`. If all `Strand`s for a table +encounter a cycle, then we know that the current selected `Goal` has no more +answers. ## Coinduction and refinement strands -Coinduction basically means that two statements can rely on each other being true, unless either is proven false. +Coinduction basically means that two statements can rely on each other being +true, unless either is proven false. For example with the following program: ``` @@ -52,9 +103,19 @@ For example with the following program: trait C1 { } forall { A: C1 if B: C1 } ``` -Then the goal `exists { T: C1 }` holds for all `T` and `U`. If the `C1` trait was not coinductive, this would be a simple cycle. - -To implement coinduction in the engine, delayed subgoals were introduced. Essentially, if a cycle is found, and the `Goal` is coinductive, then this is "delayed" until the stack unwinds back to the top `Goal` and all other non-coinductive cycles have been proven. Then, `Goal` has been proven itself. In some cases, it is the *root* `Goal` that has delayed coinductive subgoals (see above example). In this case, we create another "Refinement Strand" where the only subgoals are the delayed coinductive subgoals. If this new `Strand` can be proven, then any `Answer`s from that are valid answers for the root `Goal`. However, since there are currently delayed coinductive subgoals, there are no answers available yet. +Then the goal `exists { T: C1 }` holds for all `T` and `U`. If the `C1` +trait was not coinductive, this would be a simple cycle. + +To implement coinduction in the engine, delayed subgoals were introduced. +Essentially, if a cycle is found, and the `Goal` is coinductive, then this is +"delayed" until the stack unwinds back to the top `Goal` and all other +non-coinductive cycles have been proven. Then, `Goal` has been proven itself. In +some cases, it is the *root* `Goal` that has delayed coinductive subgoals (see +above example). In this case, we create another "Refinement Strand" where the +only subgoals are the delayed coinductive subgoals. If this new `Strand` can be +proven, then any `Answer`s from that are valid answers for the root `Goal`. +However, since there are currently delayed coinductive subgoals, there are no +answers available yet. [`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html diff --git a/book/src/engine/major_concepts.md b/book/src/engine/major_concepts.md index 601fc1f17f8..f0b2eed0de7 100644 --- a/book/src/engine/major_concepts.md +++ b/book/src/engine/major_concepts.md @@ -1,32 +1,60 @@ # Major concepts -This section goes over a few different concepts that are crucial to understanding how `chalk-engine` works, without going over the exact solving logic. +This section goes over a few different concepts that are crucial to +understanding how `chalk-engine` works, without going over the exact solving +logic. ## `Context`, `ContextOps`, and `InferenceTable` ### `Context` -The [`Context`] trait is the primary bridge between Chalk internal logic and external types. In addition actually *defining* the types (via associated types), it also contains associated functions to convert or extract information from those types. Overall, this allows the types to be basically opaque to the engine internals. Functions in trait are agnostic to specific program or environment details, since they lack a `&self` argument. +The [`Context`] trait is the primary bridge between Chalk internal logic and +external types. In addition actually *defining* the types (via associated +types), it also contains associated functions to convert or extract +information from those types. Overall, this allows the types to be basically +opaque to the engine internals. Functions in trait are agnostic to specific +program or environment details, since they lack a `&self` argument. -To give an example, there is an associated `Goal` type. However, Chalk doesn't know how to solve this. Instead, it has to be converted an [`HhGoal`] via the `Context::into_hh_goal` function. This will be coverted more in the `Goals` section. +To give an example, there is an associated `Goal` type. However, Chalk doesn't +know how to solve this. Instead, it has to be converted an [`HhGoal`] via the +`Context::into_hh_goal` function. This will be coverted more in the `Goals` +section. ### `ContextOps` -The [`ContextOps`] trait contains functions that may specifically require information a specific program or environment. For example, the `program_clauses` function gives potential ways to prove a `Goal`, but obviously it requires knowing the program (for example, what types, traits, and impls there are). Functions in this trait all take a `&self` argument. +The [`ContextOps`] trait contains functions that may specifically require +information a specific program or environment. For example, the +`program_clauses` function gives potential ways to prove a `Goal`, but obviously + it requires knowing the program (for example, what types, traits, and impls + there are). Functions in this trait all take a `&self` argument. ### `InferenceTable` -The [`InferenceTable`] is a super trait to the `UnificationOps`, `TruncateOps`, and `ResolventOps`. Each of these contains functions that track the state of specific parts of the program. Importantly, these operations can dynamically change the state of the logic itself. +The [`InferenceTable`] is a super trait to the `UnificationOps`, `TruncateOps`, +and `ResolventOps`. Each of these contains functions that track the state of +specific parts of the program. Importantly, these operations can dynamically +change the state of the logic itself. ## Goals -A "goal" in Chalk can be thought of as "something we want to prove". The engine itself understands [`HhGoal`]s. Goals of are consist of the most basic logic, such as introducing Binders (`Forall` or `Exists`) or combining goals (`All`). On the other `Context::Goal` represents an opaque goal generated externally. As such, it may contain any extra information or may be interned. When solving a logic predicate, Chalk will lazily convert `Context::Goal`s into `HHGoal`s. +A "goal" in Chalk can be thought of as "something we want to prove". The engine +itself understands [`HhGoal`]s. Goals of are consist of the most basic logic, +such as introducing Binders (`Forall` or `Exists`) or combining goals (`All`). +On the other `Context::Goal` represents an opaque goal generated externally. +As such, it may contain any extra information or may be interned. When solving a +logic predicate, Chalk will lazily convert `Context::Goal`s into `HHGoal`s. -There are three types of completely opaque `HhGoal`s that Chalk can solve: `Unify`, `DomainGoal`, and `CannotProve`. Unlike the other types of goals, these three cannot be simiplified any further. `Unify` is the goal of unifying any two types. `DomainGoal` is any goal that can solve by applying a `ProgramClause`. To solve this, more `Goal`s may generated. Finally, `CannotProve` is a special goal that *cannot* be proven true or false. +There are three types of completely opaque `HhGoal`s that Chalk can solve: +`Unify`, `DomainGoal`, and `CannotProve`. Unlike the other types of goals, +these three cannot be simiplified any further. `Unify` is the goal of unifying +any two types. `DomainGoal` is any goal that can solve by applying a +`ProgramClause`. To solve this, more `Goal`s may generated. Finally, +`CannotProve` is a special goal that *cannot* be proven true or false. ## Answers and Solutions -For every `Goal`, there are zero or more `Answer`s. Each `Answer` contains values for the inference variables in the goal. +For every `Goal`, there are zero or more `Answer`s. Each `Answer` contains +values for the inference variables in the goal. For example, given the following program: ``` @@ -42,19 +70,40 @@ The following solutions would be given: T = A T = B ``` -In other words, either `A` or `B` can substituted for `T` and the goal will hold true. Moreover, either answer could be used when further solving other goals that depend on this goal. - -However, oftentimes, this is not what external crates want when solving for a goal. Instead, the may want a *unique* solution to this goal. Indeed, when we solve for a given root `Goal`, we return a since [`Solution`]. It is up to the implementation of `Context` to decide how a `Solution` is made, given a possibly infinite set of answers. One of example of this is the [`AntiUnifier`](https://rust-lang.github.io/chalk/chalk_solve/solve/slg/aggregate/struct.AntiUnifier.html) from `chalk-solve`, which finds a minimal generalization of answers which don't unify. (For the example above, it would return only `Ambiguous`, since `A` and `B` can't unify.) +In other words, either `A` or `B` can substituted for `T` and the goal will +hold true. Moreover, either answer could be used when further solving other +goals that depend on this goal. + +However, oftentimes, this is not what external crates want when solving for a +goal. Instead, the may want a *unique* solution to this goal. Indeed, when we +solve for a given root `Goal`, we return a since [`Solution`]. It is up to the +implementation of `Context` to decide how a `Solution` is made, given a possibly +infinite set of answers. One of example of this is the +[`AntiUnifier`](https://rust-lang.github.io/chalk/chalk_solve/solve/slg/aggregate/struct.AntiUnifier.html) +from `chalk-solve`, which finds a minimal generalization of answers which don't +unify. (For the example above, it would return only `Ambiguous`, since `A` and +`B` can't unify.) ## ExClauses and Strands -An [`ExClause`] is described in literature as `A :- D | G` or `A holds given that G holds with D delayed goals`. In `chalk-engine`, an `ExClause` stores the current state of proving a goal, including existing substitutions already found, subgoals yet to be proven, or delayed subgoals. A [`Strand`] wraps both an `ExClause` and an [`InferenceTable`] together. +An [`ExClause`] is described in literature as `A :- D | G` or +`A holds given that G holds with D delayed goals`. In `chalk-engine`, an +`ExClause` stores the current state of proving a goal, including existing +substitutions already found, subgoals yet to be proven, or delayed subgoals. A +[`Strand`] wraps both an `ExClause` and an [`InferenceTable`] together. ## Tables and Forests -A `Strand` represents a *single* direction to find an `Answer` - for example, an implementation of a trait with a set of where clauses. However, in a program, there may be *multiple* possible implementations that match a goal - e.g. multiple impls with different where clauses. Every [`Table`] has a goal, and stores existing `Answers`, as well as all `Strand`s that may result in more answers. +A `Strand` represents a *single* direction to find an `Answer` - for example, an +implementation of a trait with a set of where clauses. However, in a program, +there may be *multiple* possible implementations that match a goal - e.g. +multiple impls with different where clauses. Every [`Table`] has a goal, and +stores existing `Answers`, as well as all `Strand`s that may result in more +answers. -A [`Forest`] holds all the `Table`s that program generates, and is what most of the logic is implemented on. It also stores the current state of solving (the stack). +A [`Forest`] holds all the `Table`s that program generates, and is what most of +the logic is implemented on. It also stores the current state of solving (the +stack). From 61f6a395971fe17ae2b888555c901d52b6f3ed67 Mon Sep 17 00:00:00 2001 From: Jack Date: Thu, 6 Feb 2020 21:07:59 -0500 Subject: [PATCH 3/8] Mark code blocks as notrust --- book/src/engine/logic.md | 2 +- book/src/engine/major_concepts.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/book/src/engine/logic.md b/book/src/engine/logic.md index bed0d2a56bc..710f44a6b97 100644 --- a/book/src/engine/logic.md +++ b/book/src/engine/logic.md @@ -98,7 +98,7 @@ Coinduction basically means that two statements can rely on each other being true, unless either is proven false. For example with the following program: -``` +```notrust #[coinductive] trait C1 { } forall { A: C1 if B: C1 } diff --git a/book/src/engine/major_concepts.md b/book/src/engine/major_concepts.md index f0b2eed0de7..636dab6cfe6 100644 --- a/book/src/engine/major_concepts.md +++ b/book/src/engine/major_concepts.md @@ -57,7 +57,7 @@ For every `Goal`, there are zero or more `Answer`s. Each `Answer` contains values for the inference variables in the goal. For example, given the following program: -``` +```notrust trait Clone {} struct A {} struct B {} @@ -66,7 +66,7 @@ impl Clone for B {} ``` With the following goal: `exists { T: Clone }` The following solutions would be given: -``` +```notrust T = A T = B ``` From f4597b554d48783d538bf650426f8d29528d25a7 Mon Sep 17 00:00:00 2001 From: Jack Date: Fri, 7 Feb 2020 09:44:55 -0500 Subject: [PATCH 4/8] Typo --- book/src/engine/logic.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/engine/logic.md b/book/src/engine/logic.md index 710f44a6b97..3dfd2508242 100644 --- a/book/src/engine/logic.md +++ b/book/src/engine/logic.md @@ -79,7 +79,7 @@ still be other `Answer`s available. ## Answers After an answer has been found for a subgoal, it must be *applied* to the parent -`Strand`. Specifcally, it must be able to unify with any existing `Answers`. If +`Strand`. Specifically, it must be able to unify with any existing `Answers`. If the `Answer`s are incompatible, the `Strand` is dropped since it can't lead anywhere. From 77a3c18403d4c6c677a39e7357e7c78be501df20 Mon Sep 17 00:00:00 2001 From: Jack Date: Fri, 7 Feb 2020 17:12:18 -0500 Subject: [PATCH 5/8] More typos --- book/src/engine/logic.md | 2 +- book/src/engine/major_concepts.md | 11 ++++++----- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/book/src/engine/logic.md b/book/src/engine/logic.md index 3dfd2508242..325f89f4fd4 100644 --- a/book/src/engine/logic.md +++ b/book/src/engine/logic.md @@ -49,7 +49,7 @@ and `Coinduction and refinement strands`), whereas `CompleteAnswer`s may not. `root_answer` essentially just wraps `ensure_root_answer` and converts the `Goal`'s `Answer` to a `CompleteAnswer`. -The `ensure_root_answer` function contains to core skeleton of the logic around +The `ensure_root_answer` function contains the core skeleton of the logic around `Strand` and subgoal selection. The majority of the logic, however, is split out into separate functions that branch out from `ensure_root_answer`. diff --git a/book/src/engine/major_concepts.md b/book/src/engine/major_concepts.md index 636dab6cfe6..865d234457e 100644 --- a/book/src/engine/major_concepts.md +++ b/book/src/engine/major_concepts.md @@ -12,7 +12,7 @@ The [`Context`] trait is the primary bridge between Chalk internal logic and external types. In addition actually *defining* the types (via associated types), it also contains associated functions to convert or extract information from those types. Overall, this allows the types to be basically -opaque to the engine internals. Functions in trait are agnostic to specific +opaque to the engine internals. Functions in the trait are agnostic to specific program or environment details, since they lack a `&self` argument. To give an example, there is an associated `Goal` type. However, Chalk doesn't @@ -38,11 +38,12 @@ change the state of the logic itself. ## Goals A "goal" in Chalk can be thought of as "something we want to prove". The engine -itself understands [`HhGoal`]s. Goals of are consist of the most basic logic, +itself understands [`HhGoal`]s. `HHGoal`s consist of the most basic logic, such as introducing Binders (`Forall` or `Exists`) or combining goals (`All`). -On the other `Context::Goal` represents an opaque goal generated externally. -As such, it may contain any extra information or may be interned. When solving a -logic predicate, Chalk will lazily convert `Context::Goal`s into `HHGoal`s. +On the other hand, `Context::Goal` represents an opaque goal generated +externally. As such, it may contain any extra information or may be interned. +When solving a logic predicate, Chalk will lazily convert `Context::Goal`s +into `HHGoal`s. There are three types of completely opaque `HhGoal`s that Chalk can solve: `Unify`, `DomainGoal`, and `CannotProve`. Unlike the other types of goals, From 52d2498d082e228fc80513a0d6712ceb65dd2f36 Mon Sep 17 00:00:00 2001 From: Jack Date: Wed, 26 Feb 2020 17:28:33 -0500 Subject: [PATCH 6/8] More links --- book/src/engine/logic.md | 28 +++++++++++++++++----------- book/src/engine/major_concepts.md | 24 +++++++++++++++--------- 2 files changed, 32 insertions(+), 20 deletions(-) diff --git a/book/src/engine/logic.md b/book/src/engine/logic.md index 325f89f4fd4..9c25cbdd0a8 100644 --- a/book/src/engine/logic.md +++ b/book/src/engine/logic.md @@ -4,7 +4,7 @@ `chalk-engine` solves a `Goal` using a depth-first search. When asked to solve a particular `Goal` it hasn't seen before, it will first ask the [`Context`] to -generate a set of program clauses, that get turned into `Strand`s, that could +generate a set of program clauses, that get turned into [`Strand`]s, that could solve that goal. Otherwise, if asked to solve a `Goal` it has seen before, it will select the existing table. @@ -21,19 +21,19 @@ something to be unsolvable), the solving is restarted at the root `Goal`. ## The stack In order to detect cycles (talked more about later), as well as keep track of -the selected `Strand` for each table, `chalk-engine` stores a [`Stack`] on the -`Forest`. Whenever a new goal is selected, a `StackEntry` is pushed onto the +the selected [`Strand`] for each table, `chalk-engine` stores a [`Stack`] on the +`Forest`. Whenever a new goal is selected, a [`StackEntry`] is pushed onto the `Stack`, as well as the the "time" (which also gets incremented) that it was pushed. This "time" can be compared later to check if all the `Strands` of a -`Table` have been checked in a single solve. +[`Table`] have been checked in a single solve. As either `Answer`s are found for the selected `Table`, entries on the stack are `pop`ed. If something is found to be unsolvable, the complete stack is unwound. ## Table creation -As mentioned before, whenever a new `Goal` is encounted, a new `Table` is -created to store current and future answers. First, the `Goal` is converted into +As mentioned before, whenever a new `Goal` is encounted, a new [`Table`] is +created to store current and future answers. First, the [`Goal`] is converted into an [`HhGoal`]. If it can be simplified, then a `Strand` with one or more subgoals will be generated and can be followed as above. Otherwise, if it is a `DomainGoal` (see above), then @@ -42,14 +42,14 @@ is called and each clause is converted into a `Strand` and can be followed. ## `root_answer` and `ensure_root_answer` -The `root_answer` function is the entry point to solve a `Goal`. Up until now, +The [`root_answer`](https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.root_answer) function is the entry point to solve a `Goal`. Up until now, the idea of `Answer` versus `CompleteAnswer` have been ignored. However, in reality `Answer`s to `Goal`s may actually have delayed subgoals (see `ExClause` -and `Coinduction and refinement strands`), whereas `CompleteAnswer`s may not. -`root_answer` essentially just wraps `ensure_root_answer` and converts the -`Goal`'s `Answer` to a `CompleteAnswer`. +and `Coinduction and refinement strands`), whereas [`CompleteAnswer`]s may not. +`root_answer` essentially just wraps [`ensure_root_answer`](https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer) and converts the +`Goal`'s [`Answer`] to a [`CompleteAnswer`]. -The `ensure_root_answer` function contains the core skeleton of the logic around +The [`ensure_root_answer`](https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer) function contains the core skeleton of the logic around `Strand` and subgoal selection. The majority of the logic, however, is split out into separate functions that branch out from `ensure_root_answer`. @@ -118,6 +118,12 @@ However, since there are currently delayed coinductive subgoals, there are no answers available yet. +[`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html [`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html [`HhGoal`]: https://rust-lang.github.io/chalk/chalk_engine/hh/enum.HhGoal.html [`Stack`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.Stack.html +[`StackEntry`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.StackEntry.html +[`Table`]: https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html +[`Goal`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Goal +[`Answer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.Answer.html +[`CompleteAnswer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.CompleteAnswer.html diff --git a/book/src/engine/major_concepts.md b/book/src/engine/major_concepts.md index 865d234457e..6c8a3cd0aeb 100644 --- a/book/src/engine/major_concepts.md +++ b/book/src/engine/major_concepts.md @@ -15,7 +15,7 @@ information from those types. Overall, this allows the types to be basically opaque to the engine internals. Functions in the trait are agnostic to specific program or environment details, since they lack a `&self` argument. -To give an example, there is an associated `Goal` type. However, Chalk doesn't +To give an example, there is an associated [`Goal`] type. However, Chalk doesn't know how to solve this. Instead, it has to be converted an [`HhGoal`] via the `Context::into_hh_goal` function. This will be coverted more in the `Goals` section. @@ -30,8 +30,8 @@ information a specific program or environment. For example, the ### `InferenceTable` -The [`InferenceTable`] is a super trait to the `UnificationOps`, `TruncateOps`, -and `ResolventOps`. Each of these contains functions that track the state of +The [`InferenceTable`] is a super trait to the [`UnificationOps`], [`TruncateOps`], +and [`ResolventOps`]. Each of these contains functions that track the state of specific parts of the program. Importantly, these operations can dynamically change the state of the logic itself. @@ -49,12 +49,12 @@ There are three types of completely opaque `HhGoal`s that Chalk can solve: `Unify`, `DomainGoal`, and `CannotProve`. Unlike the other types of goals, these three cannot be simiplified any further. `Unify` is the goal of unifying any two types. `DomainGoal` is any goal that can solve by applying a -`ProgramClause`. To solve this, more `Goal`s may generated. Finally, +[`ProgramClause`]. To solve this, more `Goal`s may generated. Finally, `CannotProve` is a special goal that *cannot* be proven true or false. ## Answers and Solutions -For every `Goal`, there are zero or more `Answer`s. Each `Answer` contains +For every `Goal`, there are zero or more `Answer`s. Each [`Answer`] contains values for the inference variables in the goal. For example, given the following program: @@ -77,8 +77,8 @@ goals that depend on this goal. However, oftentimes, this is not what external crates want when solving for a goal. Instead, the may want a *unique* solution to this goal. Indeed, when we -solve for a given root `Goal`, we return a since [`Solution`]. It is up to the -implementation of `Context` to decide how a `Solution` is made, given a possibly +solve for a given root [`Goal`], we return a since [`Solution`]. It is up to the +implementation of [`Context`] to decide how a `Solution` is made, given a possibly infinite set of answers. One of example of this is the [`AntiUnifier`](https://rust-lang.github.io/chalk/chalk_solve/solve/slg/aggregate/struct.AntiUnifier.html) from `chalk-solve`, which finds a minimal generalization of answers which don't @@ -91,11 +91,11 @@ An [`ExClause`] is described in literature as `A :- D | G` or `A holds given that G holds with D delayed goals`. In `chalk-engine`, an `ExClause` stores the current state of proving a goal, including existing substitutions already found, subgoals yet to be proven, or delayed subgoals. A -[`Strand`] wraps both an `ExClause` and an [`InferenceTable`] together. +[`Strand`] wraps both an [`ExClause`] and an [`InferenceTable`] together. ## Tables and Forests -A `Strand` represents a *single* direction to find an `Answer` - for example, an +A [`Strand`] represents a *single* direction to find an [`Answer`] - for example, an implementation of a trait with a set of where clauses. However, in a program, there may be *multiple* possible implementations that match a goal - e.g. multiple impls with different where clauses. Every [`Table`] has a goal, and @@ -117,3 +117,9 @@ stack). [`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html [`Table`]: https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html [`Forest`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html +[`Goal`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Goal +[`UnificationOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.UnificationOps.html +[`TruncateOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.TruncateOps.html +[`ResolventOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.ResolventOps.html +[`ProgramClause`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.ProgramClause +[`Answer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.Answer.html \ No newline at end of file From 1fd2672f5299bb898abd6ff547fa6709051c2456 Mon Sep 17 00:00:00 2001 From: Jack Date: Wed, 26 Feb 2020 17:41:58 -0500 Subject: [PATCH 7/8] Other review comments and add coinduction doc as subchapter --- book/src/SUMMARY.md | 1 + book/src/engine/logic.md | 7 +- book/src/engine/logic/coinduction.md | 294 +++++++++++++++++++++++++++ 3 files changed, 300 insertions(+), 2 deletions(-) create mode 100644 book/src/engine/logic/coinduction.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 581a969c48a..0aacd5cea5a 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -16,4 +16,5 @@ - [How does the engine work](./engine.md) - [Major concepts](./engine/major_concepts.md) - [Logic](./engine/logic.md) + - [Coinduction](./engine/logic/coinduction.md) - [Glossary and terminology](./glossary.md) diff --git a/book/src/engine/logic.md b/book/src/engine/logic.md index 9c25cbdd0a8..9c9d8044338 100644 --- a/book/src/engine/logic.md +++ b/book/src/engine/logic.md @@ -2,7 +2,7 @@ ## Overview -`chalk-engine` solves a `Goal` using a depth-first search. When asked to solve a +`chalk-engine` solves a `Goal` using a hybrid search strategy with elements of depth- and breadth-first search. When asked to solve a particular `Goal` it hasn't seen before, it will first ask the [`Context`] to generate a set of program clauses, that get turned into [`Strand`]s, that could solve that goal. Otherwise, if asked to solve a `Goal` it has seen before, it @@ -45,7 +45,7 @@ is called and each clause is converted into a `Strand` and can be followed. The [`root_answer`](https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.root_answer) function is the entry point to solve a `Goal`. Up until now, the idea of `Answer` versus `CompleteAnswer` have been ignored. However, in reality `Answer`s to `Goal`s may actually have delayed subgoals (see `ExClause` -and `Coinduction and refinement strands`), whereas [`CompleteAnswer`]s may not. +and [Coinduction and refinement strands]), whereas [`CompleteAnswer`]s may not. `root_answer` essentially just wraps [`ensure_root_answer`](https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer) and converts the `Goal`'s [`Answer`] to a [`CompleteAnswer`]. @@ -93,6 +93,7 @@ encounter a cycle, then we know that the current selected `Goal` has no more answers. ## Coinduction and refinement strands +[Coinduction and refinement strands]: #coinduction-and-refinement-strands Coinduction basically means that two statements can rely on each other being true, unless either is proven false. @@ -117,6 +118,8 @@ proven, then any `Answer`s from that are valid answers for the root `Goal`. However, since there are currently delayed coinductive subgoals, there are no answers available yet. +For much more in-depth + [`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html [`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html diff --git a/book/src/engine/logic/coinduction.md b/book/src/engine/logic/coinduction.md new file mode 100644 index 00000000000..441ca7d809c --- /dev/null +++ b/book/src/engine/logic/coinduction.md @@ -0,0 +1,294 @@ +# Coinduction + +This sub-chapter was originally prepared for wg-traits design meeting on 2019-11-08 (see the [Hackmd](https://hackmd.io/OJRi5OM6Twunw8ZmuLxfRA) doc). It briefly covers some tricky (and previously incorrectly handled) cases of coinduction, as well as two proposed solutions. The resulting and current solution ended up being something *pretty* close to Niko's solution. However, this is basically a copy-paste from the original document, and so shouldn't necessarily be taken as 100% truth as far as implementation. + +## The problem + +See [chalk#248] for details. The short version is that we fail to handle a case like this correctly, where `Ci` are all co-inductive goals: + +[chalk#248]: https://github.com/rust-lang/chalk/issues/248 + +``` +C1 :- C2, C3. +C2 :- C1. +``` + +What happens is that we + +* start to prove C1 +* start to prove C2 +* see a recursive attempt to prove C1, assume it is succesful +* consider C2 proved **and cache this** +* start to prove C3, fail +* consider C1 **unproven** + +Now we incorrectly have a result that `C2` is true -- but that result was made on the assumption that `C1` was true, and it was not. + +## Some other tricky cases to consider + +### Unification failures + +One thing to consider is that even when we have "coinduction obligations" to prove, we have to remember their substitutions too: + +``` +C1(X) :- C2(Y), X = 22. +C2(X) :- C3(X), X = 44. +C3(X) :- C1(X), C2(X). +``` + +None of these predicates should be provable, because `C1(X)` and `C2(X)` don't hold for the same `X`. + +If we're not careful, we might: + +* start to prove C1 +* start to prove C2 +* start to prove C3, see the recursive calls to C1 and C2 + * maybe we wait to consider it proven until C1 and C2 complete + +In this case, it's not enough that C1 and C2 are provable at all, they have to be provable for the same X. + +### Non-trivial self-cycles + +``` +C1(A) :- C1(B), B = 22, C2(A). +C2(44). +``` + +This case is not provable, even though the only cycle is `C1(X) :- C1(Y)` -- but it turns out that `X` must not be 22. The catch is that while this might *appear* to be a trivial self-cycle, it is not! + +Actually I have to think about the best way to handle this case, as my proposed solution doesn't quite cut it. It wouldn't be *wrong* but it seems not ideal. -- Niko + +### Delayed trivial cycles + +``` +C1(A, B) :- C2(A, B), A = 22, B = 22. +C2(A, B) :- C1(B, A). +``` + +This should be provable, but the cycle from C2 to C1 is not immediately visible as a trivial cycle, at least if subgoals are solved in order. + + +### Delayed trivial cycles, variant 2 + +``` +C1(A, B) :- C2(A, B), A = 22. +C2(A, B) :- C1(B, A). +``` + +As above, here the only complete answer is `C1(22, 22)`. This is because the `C1`, `C2` cycle effectively guarantees equality. + +### Delayed trivial cycles, variant 3 + +``` +C1(A, B) :- C1(B, A). +``` + +This is true for all `A, B` + +### Other cases? + +## Approach in existing PR + +### High-level idea + +* When we encounter a co-inductive subgoal, we delay them in the current `Strand` +* When all subgoals have been tested, and there are remaining delayed co-inductive subgoals, this is propogated up, marking the current `Strand` as co-inductive +* When the co-inductive `Strand`s reach the root table, we only then pursue an answer + +### Failing tests + +* Tests were added for the tricky cases above: + * [First](https://github.com/rust-lang/chalk/pull/272/commits/7be2d42c6ea36dd4416774d6872c43e3988f05bd#diff-721709466568566f24fc2e8634c40dcbR140) + * [Second](https://github.com/rust-lang/chalk/pull/272/commits/7be2d42c6ea36dd4416774d6872c43e3988f05bd#diff-721709466568566f24fc2e8634c40dcbR171) +* Both *are* provable to have no solutions, but are returned as ambiguous + +## Niko's proposed solution + +### High-level idea + +* We only consider a co-induction subgoal proven for *trivial* recursion -- i.e., self-recursion where you have `C1 :- C1`. +* For non-trivial recursion, we propagate the co-inductive subgoal to the parent. This continues until it becomes trivial. + +### Implementation steps + +**Extend `Answer` in two ways.** + +Currently `Answer` has a "constrained substitution" that includes values for the table's substitution + region constraints: + +```rust +struct Answer { + constrained_subst: Canonical, + is_ambiguous: bool +} + +struct ConstrainedSubst { + substitution: Substitution, + region_constraints: Vec, +} +``` + +we would first extend `ConstrainedSubst` to include as yet unproven co-inductive subgoals (this might actually be better done as a new type): + +```rust +struct ConstrainedSubst { + substitution: Substitution, + delayed_subgoals: Vec, + region_constraints: Vec, +} +``` + +then we would extend `Answer` slightly as well so it can be "ok" or ambiguous, as today, but also an *error* case + +```rust +enum AnswerMode { + OK, + Ambiguous, + Error, +} + +struct Answer { + constrained_subst: Canonical, + mode: AnswerMode +} +``` + +We won't need this error case till later, so let's ignore it for now. (And in a way, we never need it.) + +**Deferring coinductive subgoals** + +When we encounter a co-inductive subgoal, we check if it is **trivial cycle** or not. A trivial cycle is a case like `C1 :- C1`. We can simply consider such cycles to be true (but note the distinction between a *trivial* cycle and a *self-cycle* -- see the "non-trivial self-cycle" example above). + +For non-trivial cycles, we will want to store the cycle to be validated later. To accommodate that, we extend `ExClause` to include a `delayed_subgoals` list as well. We can write this the same way SLG does, so `Goal :- DelayedSubgoals | Subgoals` + +In our example, proving `C2 :- C1` would result in adding `C1` to the list of delayed subgoals. + +When we reach the end of the list of subgoals, we can create an answer that contains the delayed subgoals. We don't have to add all the goals -- we can check for those that are trivial self-cycles again and remove them (in some cases, something which was not trivial to start may have become trivial through later unifications, see Delayed Trivial Self-Cycle case). Note that we *do* have to add all non-trivial cycles, including non-trivial self-cycles -- see the walkthrough of Non-trivial self-cycle variant 3. + +So the answer to `C2` would be + +``` +substitution: [] // no variables +delayed_subgoals: ["C1"] +region_constraints: [] +``` + +We can denote this as `C2 :- C1 |`, to use SLG notation. + +**Incorporating an answer with deferred subgoals.** + +When a table gets back an answer that has deferred sub-goals, they get added to the current list of subgoals. + +So e.g. in our case, we had a `ExClause` like: + +``` +C1 :- | C2, C3 +``` + +and we get the answer `C2 :- C1 |`, so we would convert it to + +``` +C1 :- | C3, C1 +``` + +i.e., we have added `C1` to the list of goals to prove. When we go to prove `C3`, of course, we will fail -- but it had succeeded, we would go on to prove `C1` but encounter a trivial cycle and hence succeed. + +**Extending root answer** + +So we failed to prove C1, but we do have a (conditional) answer to C2 -- `C2 :- C1 |`, even though `C2` is unprovable. What happens if `ensure_root_answer` is invoked on `C2`? + +What we have here is a *conditional* answer. We know that `C1` must have ultimately resolved itself somehow (although it might not yet be proven). What we can do is create a strand in C2 to evaluate C1 again -- if this strand succeeds, it can actually overwrite the `C2 :- C1 |` answer in place with `C2 :-` (i.e., an unconditional answer). This is just a refinement of what we had. If the strand fails, though, we'll want to remember the error. + +I think when we get a new answer, we want it to *overwrite* the old answer in place, rather than create a new answer. This is valid because it's not a new answer, it's just a more refined form of the old answer (although note that it might have different substitutions and other details, see the "delayed trivial cycle" case). + +In particular, it could be that the table already has a "complete" set of answers -- i.e., somebody invoked `ensure_answer(N)` and got back `None`. We don't want to be adding new answers which would change the result of that call. It *is* a bit strange that we are changing the result of `ensure_answer(i)` for the current `i`, but then the result is the same answer, just a bit more elaborated. + +The idea then would be to create a strand *associated with this answer somehow* (it doesn't, I don't think, live in the normal strand table; we probably have a separate "refinment strand" table). This strand has as its subgoals the delayed subgoals. It pursues them. This either results in an answer (which replaces the existing answer) or an error (in which case the existing answer is marked as *error*). This may require extending strand with an optional answer index that it should overwrite, or perhaps we thread it down as an argument to `pursue_strand` (optional because, in the normal mode, we are just appending a new answer). + +(Question: What distinguishes root answer? Nothing -- we could actually do this process for any answer, so long as the delayed subgoals are not to tables actively on the stack. This just happens to be trivially true for root answers. The key part though is that the answer must be registered in the table first before the refinement strand is created, see Delayed Self-Cycle Variant 3.) + +This is complex, so let's walk through an example or two. + +**The original problem.** When we finish solving `C1`, we leave `C2` with a single answer `C2 :- C1 |`. If someone invokes `ensure_root_answer(C2, 0)`, we would see the delayed literal and create a refinement strand for the answer: `C2 :- | C1`. We would pursue `C1` and get back the successful answer. So the refinement strand would terminate and we can overwrite with the answer `C2 :- |`. + +**Delayed trivial self-cycle.** Similar to above, but the answer is `C2(?A, ?B) :- C1(?B, ?A) |`. In other words, in the canonical answer, we have a (identity) substitution of `[^0, ^1]` and a delayed goal of `C1(^1, ^0)`. The strand we create will find only one answer to `C1`, `C1(22, 22)`, so we wind up with an answer `C2(22, 22)`. + +**Handling error answers** + +We introduced the idea of an "error answer"...how do we handle that? It's fairly simple. If a strand encounters an error answer, it simply fails. Done. The *outer* search however needs to treat an error answer as basically a no-op -- so e.g. the answer iterator should simply increment the error counter and move to the next answer. + +### Walk through: delayed trivial self cycle, variant 2 + +``` +C1(A, B) :- C2(A, B), A = 22. +C2(A, B) :- C1(B, A). +``` + +* `ensure_root_answer(C1(?A, ?B))` is invoked + * We start solving `C1(?A, ?B)` with the ex-clause `C1(?A, ?B) :- | C2(?A, ?B), ?A = 22` + * That starts solving `C2(?A, ?B)` + * This gets an answer `C2(?A, ?B) :- C1(?B, ?A) |` + * When answer is incorporated, we get `C1(?A, ?B) :- | C1(?B, ?A), ?A = 22` + * `C1(?B, ?A)` is a non-trivial cycle, and so we get + * `C1(?A, ?B) :- C1(?B, ?A) | ?A = 22` + * Unification completes, leaving us with + * `C1(22, ?B) :- C1(?B, 22) |` + * This is a complete answer + * ensure root answer attempts to refine this answer, creating a strand for `C1(22, ?B) :- | C1(?B, 22)` + * This creates a table for `C1(?B, 22)` with ex-clause `C1(?B, 22) :- | C2(?B, 22), ?B = 22` + * We start solving `C2(?B, 22)`, which has ex-clause `C2(?B, 22) :- C1(22, ?B)` + * This creates a table for `C1(22, ?B)`, with ex-clause `C1(22, ?B) :- C2(22, ?B), 22 = 22` + * This starts solving `C2(22, ?B)`, which is a fresh table with ex-clause `C2(22, ?B) :- C1(?B, 22)` + * This is a co-inductive cycle + * So our answer is `C2(22, ?B) :- C1(?B, 22) |` + * Incorporating this answer yields `C1(22, ?B) :- 22 = 22, C1(?B, 22)` + * The unification constraint succeeds, leaving `C1(22, ?B) :- C1(?B, 22)` + * Co-inductive cycle detected, so answer is + * `C1(22, ?B) :- C1(?B, 22) |` + * This answer is incorporated into `C2`, yielding the ex-clause + * `C2(?B, 22) :- C1(?B, 22)` + * Pursuing that sub-goal gives a co-inductive cycle, so our final answer is + * `C2(?B, 22) :- C1(?B, 22) |` + * This answer is incorporated, yielding ex-clause `C1(?B, 22) :- | ?B = 22, C1(?B, 22)` + * Unification yields `C1(22, 22) :- C1(22, 22)` + * Trivial self-cycle detected, so final answer is + * `C1(22, 22)` + * the answer for `C1(?A, ?B)` is thus updated to `C1(22, 22)` + +### Walk through: delayed trivial self cycle, variant 3 + +``` +C1(A, B) :- C1(B, A). +``` + +This example is interesting because it shows that we have to incorporate non-trivial self cycles into an answer so they can recursively build on one another. + +* we get an initial answer of + * `C1(?A, ?B) :- C1(?B, ?A) |` +* if we attempt to refine this, we will get a strand `C1(?X, ?Y) :- C1(?Y, ?X)` + * pursuing the first subgoal `C1(?Y, ?X)` leads us to our own table, but at answer 0 + * (the very answer we are refining) + * the answer is `C1(?Y, ?X) :- C1(?X, ?Y) |` + * this strand incorporates its own answer, yielding + * `C1(?X, ?Y) :- C1(?X, ?Y)` + * next subgoal is a trivial self-cycle, discard, yielding + * `C1(?X, ?Y) :-` +* result: true + + + +### Walk through: non-trivial self cycle + +Let's walk through one more case, the non-trivial self cycle. + +``` +C1(A) :- C1(B), B = 22, C2(A). +C2(44). +``` + +What happens here is that we get an initial answer from `C1` that looks like: + +``` +C1(44) :- C1(22) | +``` + +Ensure root answer will thus try to refine by trying to solve `C1(22)`. Interestingly, this is going to go to a distinct table, because the canonical form is not the same, but that table will just fail. \ No newline at end of file From de87a52fd192675e25500e56b3d4cd51553ab588 Mon Sep 17 00:00:00 2001 From: Jack Date: Wed, 26 Feb 2020 18:06:42 -0500 Subject: [PATCH 8/8] Don't run code blocks in coinduction.md --- book/src/engine/logic/coinduction.md | 32 ++++++++++++++-------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/book/src/engine/logic/coinduction.md b/book/src/engine/logic/coinduction.md index 441ca7d809c..12d94b290e4 100644 --- a/book/src/engine/logic/coinduction.md +++ b/book/src/engine/logic/coinduction.md @@ -8,7 +8,7 @@ See [chalk#248] for details. The short version is that we fail to handle a case [chalk#248]: https://github.com/rust-lang/chalk/issues/248 -``` +```notrust C1 :- C2, C3. C2 :- C1. ``` @@ -30,7 +30,7 @@ Now we incorrectly have a result that `C2` is true -- but that result was made o One thing to consider is that even when we have "coinduction obligations" to prove, we have to remember their substitutions too: -``` +```notrust C1(X) :- C2(Y), X = 22. C2(X) :- C3(X), X = 44. C3(X) :- C1(X), C2(X). @@ -49,7 +49,7 @@ In this case, it's not enough that C1 and C2 are provable at all, they have to b ### Non-trivial self-cycles -``` +```notrust C1(A) :- C1(B), B = 22, C2(A). C2(44). ``` @@ -60,7 +60,7 @@ Actually I have to think about the best way to handle this case, as my proposed ### Delayed trivial cycles -``` +```notrust C1(A, B) :- C2(A, B), A = 22, B = 22. C2(A, B) :- C1(B, A). ``` @@ -70,7 +70,7 @@ This should be provable, but the cycle from C2 to C1 is not immediately visible ### Delayed trivial cycles, variant 2 -``` +```notrust C1(A, B) :- C2(A, B), A = 22. C2(A, B) :- C1(B, A). ``` @@ -79,7 +79,7 @@ As above, here the only complete answer is `C1(22, 22)`. This is because the `C1 ### Delayed trivial cycles, variant 3 -``` +```notrust C1(A, B) :- C1(B, A). ``` @@ -115,7 +115,7 @@ This is true for all `A, B` Currently `Answer` has a "constrained substitution" that includes values for the table's substitution + region constraints: -```rust +```notrust struct Answer { constrained_subst: Canonical, is_ambiguous: bool @@ -129,7 +129,7 @@ struct ConstrainedSubst { we would first extend `ConstrainedSubst` to include as yet unproven co-inductive subgoals (this might actually be better done as a new type): -```rust +```rust,ignore struct ConstrainedSubst { substitution: Substitution, delayed_subgoals: Vec, @@ -139,7 +139,7 @@ struct ConstrainedSubst { then we would extend `Answer` slightly as well so it can be "ok" or ambiguous, as today, but also an *error* case -```rust +```rust,ignore enum AnswerMode { OK, Ambiguous, @@ -166,7 +166,7 @@ When we reach the end of the list of subgoals, we can create an answer that cont So the answer to `C2` would be -``` +```notrust substitution: [] // no variables delayed_subgoals: ["C1"] region_constraints: [] @@ -180,13 +180,13 @@ When a table gets back an answer that has deferred sub-goals, they get added to So e.g. in our case, we had a `ExClause` like: -``` +```notrust C1 :- | C2, C3 ``` and we get the answer `C2 :- C1 |`, so we would convert it to -``` +```notrust C1 :- | C3, C1 ``` @@ -218,7 +218,7 @@ We introduced the idea of an "error answer"...how do we handle that? It's fairly ### Walk through: delayed trivial self cycle, variant 2 -``` +```notrust C1(A, B) :- C2(A, B), A = 22. C2(A, B) :- C1(B, A). ``` @@ -256,7 +256,7 @@ C2(A, B) :- C1(B, A). ### Walk through: delayed trivial self cycle, variant 3 -``` +```notrust C1(A, B) :- C1(B, A). ``` @@ -280,14 +280,14 @@ This example is interesting because it shows that we have to incorporate non-tri Let's walk through one more case, the non-trivial self cycle. -``` +```notrust C1(A) :- C1(B), B = 22, C2(A). C2(44). ``` What happens here is that we get an initial answer from `C1` that looks like: -``` +```notrust C1(44) :- C1(22) | ```