Merge pull request #488 from nikomatsakis/recursive-solver-document

document recursive solver

Author: nikomatsakis

book/src/SUMMARY.md

@@ -26,6 +26,11 @@
     - [Logic](./engine/logic.md)
         - [Coinduction](./engine/logic/coinduction.md)
     - [SLG Solver](./engine/slg.md)
+- [Chalk recursive solver](./recursive.md)
+    - [The stack](./recursive/stack.md)
+    - [Inductive cycles](./recursive/inductive_cycles.md)
+    - [The search graph and caching](./recursive/search_graph.md)
+    - [Coinduction](./recursive/coinduction.md)
 
 ---
 

book/src/recursive.md

@@ -0,0 +1,97 @@
+# Chalk recursive solver
+
+The recursive solver, as its name suggests, is a logic solver that works
+"recursively". In particular, its basic structure is a function like:
+
+```rust,ignore
+fn(Goal) -> Solution
+```
+
+where the Goal is some [canonical goal](./canonical_queries.md) and
+the Solution is a result like:
+
+* Provable(S): meaning the goal is provable and it is provably exactly (and
+  only) for the substitution S. S is a set of values for the inference variables
+  that appear in the goal. So if we had a goal like `Vec<?X>: Foo`, and we
+  returned `Provable(?X = u32)`, it would mean that only `Vec<u32>: Foo` and not
+  any other sort of vector (e.g., `Vec<u64>: Foo` does not hold).
+* Ambiguous(S): meaning that we can't prove whether or not the goal is true.
+  This can sometimes come with a substitution S, which offers suggested values
+  for the inference variables that might make it provable.
+* Error: the goal cannot be proven.
+
+## Recursion: pros and cons
+
+The recursive solver is so-called because, in the process of solving one goal,
+it will "recurse" to solve another. Consider an example like this:
+
+```rust,ignore
+trait A { }
+impl<T: A> A for Vec<T> { }
+impl A for u32 { }
+impl A for i32 { }
+```
+
+which results in program clauses like:
+
+```notrust
+forall<T> { Implemented(Vec<T>: A) :- Implemented(T: MyTrait) }
+Implemented(u32: A)
+Implemented(i32: A)
+```
+
+First, suppose that we have a goal like `Implemented(Vec<u64>: A)`. This would
+proceed like so:
+
+* `Solve(Implemented(Vec<u64>: A))`
+    * `Solve(Implemented(u64: A))`
+        * returns `Error`
+    * returns `Error`
+
+In other words, the recursive solver would start by applying the first rule,
+which would cause us recursively try to solve `Implemented(u64: A)`. This would
+yield an Error result, because there are no applicable rules, and that error
+would propagate back up, causing the entire attempt at proving things to fail.
+
+Next, consider `Implemented(Vec<u32>: A)`. This would proceed like so:
+
+* `Solve(Implemented(Vec<u32>: A))`
+    * `Solve(Implemented(u32: A))`
+        * returns `Provable` with no substitution (no variables)
+    * returns `Provable`
+
+Finally, consider `Implemented(Vec<?X>: A)`. This is more interesting because it
+has a variable:
+
+* `Solve(Implemented(Vec<?X>: A))`
+    * `Solve(Implemented(?X: A))`
+        * finds two viable solutions, returns `Ambiguous`
+    * returns `Ambiguous`
+
+## Recursion and completeness
+
+One side-effect of the recursive solver's structure is that it
+cannot solve find solutions in some cases where a traditional
+Prolog solver would be successful. Consider this example:
+
+```rust
+trait A { }
+trait B { }
+
+impl<T: A + B> A for Vec<T> { }
+
+impl A for u32 { }
+impl B for u32 { }
+
+impl A for i32 { }
+```
+
+In the recursive solver, with a goal of `Implemented(Vec<?X>: A)`, we
+recursively try to prove `Implemented(?X: A)` and get ambiguity, and we get
+stuck there.
+
+The [SLG solver] in contrast starts by exploring `?X = u32` and finds
+that it works, and then later tries to explore `?X = i32` and finds that it
+fails (because `i32: B` is not true).
+
+[SLG solver]: ./engine.md

book/src/recursive/coinduction.md

@@ -0,0 +1,3 @@
+# Coinduction
+
+TBD

book/src/recursive/inductive_cycles.md

@@ -0,0 +1,148 @@
+# Inductive cycles
+
+Recursive solving without cycles is easy. Solving with cycles is rather more
+complicated. Before we get into the details of the implementation,
+let's talk a bit about what behavior we actually *expect* in the face
+of possible cycles.
+
+## Inductive cycles
+
+By default, Rust trait solving is **inductive**. What that means is that, roughly
+speaking, you have to prove something is true without any cycles (i.e., you
+can't say "it's true because it's true"!).
+
+For our purpose, a "cycle" means that, in the course of proving some canonical
+goal G, we had to prove that same goal G again.
+
+Consider this Rust program:
+
+```rust
+trait A { }
+impl<T: A> A for Vec<T> { }
+impl A for u32 { }
+```
+
+Whether or not we hit a cycle will depend on the goal we are trying
+to solve. If for example we are trying to prove `Implemented(Vec<u32>: A)`,
+then we don't hit any cycle:
+
+* `Implemented(Vec<u32>: A) :- Implemented(u32: A)` // from the first impl
+    * `Implemented(u32: A)` // from the second impl
+
+But what if we are trying to prove `Implemented(?X: A)`? This is a bit
+more interesting. Because we don't know what `?X` is, both impls are
+actually potentially applicable, so we wind up with two ways to
+prove our goal. We will try them out one after the other.
+
+One possible execution might be:
+
+* Prove `Implemented(?X: A)`
+    * we find the program clause `forall<T> { Implemented(Vec<T>: A) :- Implemented(T: A) }` from the first impl
+        * we create the variable `?Y` to represent `T` and unify `?X = Vec<?Y>`.
+        * after unification, we have the subgoal `Implemented(?Y: A)`
+            * when we go to recursively prove this impl, however, we find that it is already on the stack
+            * this is because the [canonical form] of `Implemented(?X: A)` and `Implemented(?Y: A)` is the same
+
+[canonical form]: ../canonical_queries.md
+
+## What happens if we treat inductive cycles as errors?
+
+So, what do we do when we hit an inductive cycle? Given that we told you that an
+inductive proof cannot contain cycles, you might imagine that we can just treat
+such a cycle as an error. But this won't give us the correct result.
+
+Consider our previous example. If we just treat that cycle as an error, then we
+will conclude that the impl for `Vec<T>` doesn't apply to `?X: A`, and we'll
+proceed to try the impl for `u32`. This will let us reason that `?X: A` is
+provable if `?X = u32`. This is, in fact, correct: `?X = u32` *is* a possible
+answer. The problem is, it's not the only one!
+
+In fact, `Implemented(?X: A)` has an **infinite** number of answers. It is true
+for `?X = u32`. It is true for `?X = Vec<u32>`. It is also true for
+`Vec<Vec<u32>>` and `Vec<Vec<Vec<u32>>>` and so on.
+
+Given this, the correct result for our query is actually "ambiguous" -- in
+particular, there is no unique substitution that we can give that would make the
+query provable.
+
+## How we solve cycles: loop and try again
+
+The way we actually handle cycles is by iterating until we reach a fixed point
+(or ambiguity). We start out by assuming that all cycles are errors and we try
+to find some solution S. If we succeed, then we can do a loop and iterate again
+-- this time, for each cycle, we assume the result is S. This may yield some new
+solution, S1. The key point here is that we now have **two possible solutions**
+to the same goal, S and S1. This implies two possibilities:
+
+* If S == S1, then in fact there is a unique solution, so we can return `Provable(S)`.
+* If S != S1, then we know there are two solutions, which means that there is
+  not one unique solution, and hence the correct result is **ambiguous**,
+  and in fact we can just stop and return right now.
+
+This technique is very similar to the traditional Prolog technique of handling
+cycles, which is called **tabling**. The difference between our approach and
+tabling is that we are always looking for a unique solution, whereas Prolog
+(like the [SLG solver]) tries to enumerate all solutions (i.e., in Prolog,
+solving a goal is not a function but an iterator that yields solutions, and
+hence it would yield up S first, and then S1, and then any further answers we
+might get).
+
+[SLG solver]: ../engine.md
+
+Intuitively, what is happening here is that we're building bigger and bigger
+"proof trees" (i.e., trees of impl applications). In the first iteration, where
+we assumed that all recursive calls were errors, we would find exactly one
+solution, `u32: A` -- this is the root tree. In the next iteration, we can use
+this result to build a tree for `Vec<u32>: A` and so forth.
+
+## Inductive cycles with no base case
+
+It is interesting to look at what happens without the base case. Consider this
+program:
+
+```rust
+trait B { }
+impl<T: B> B for Vec<T> { }
+```
+
+In this case, there is no base case -- this means that in fact there are no
+solutions at all to the query `?X: B`. The reason is that the only type that
+could match would be a type of infinite size like `Vec<Vec<Vec<...>>>: B`, where
+the chain of `Vec` never terminates.
+
+In our solver, this will work out just fine. We will wind up recursing
+and encountering a cycle. This will be treated as an error in the first
+iteration -- and then, at the end, we'll still have an error. This means
+that we've reached a fixed point, and we can stop.
+
+
+## Inductive cycles: when do we ever terminate
+
+You might be wondering whether there are any examples of inductive cycles that
+actually terminate successfully and without ambiguity. In fact, there are very
+few, but you can construct an example like this:
+
+```rust
+trait C { }
+impl<T: C + D> C for Vec<T> { }
+impl C for u32 { }
+
+trait D { }
+```
+
+In this case, the only valid result of `Implemented(?X: C)` is `?X = u32`. It can't
+be `Vec<u32>` because `Implemented(u32: D)` is not true.
+
+How does this work out with the recursive solver? In the first iteration,
+we wind up with `?X = u32`, but we do encounter a cycle:
+
+* proving `Implemented(?X: C)` has two possibilities...
+    * `?X = Vec<?Y>` and `Implemented(?Y: C)`, which is a cycle (error, at least in this iteration)
+    * `?X = u32`, succeeds
+
+So then we try the next iteration:
+
+* proving `Implemented(?X: C)` has two possibilities...
+    * `?X = Vec<?Y>` and `Implemented(?Y: C)`, which is a cycle, so we use our previous result of `?Y = u32`
+        * we then have to prove `Implemented(u32: D)`, which fails
+    * `?X = u32`, succeeds