# 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:

```
fn(Goal) -> Solution
```

where the Goal is some canonical goal 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:

```
trait A { }
impl<T: A> A for Vec<T> { }
impl A for u32 { }
impl A for i32 { }
```

which results in program clauses like:

```
forall<T> { Implemented(Vec<T>: A) :- Implemented(T: A) }
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
- 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
- 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`

- finds two viable solutions, returns
- 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:

`#![allow(unused)] fn main() { trait A { } trait B { } impl<T: A + B> A for Vec<T> { } impl A for u32 { } impl B for u32 { } impl A for i32 { } impl B for i8 { } }`

In the recursive solver, with a goal of `Implemented(Vec<?X>: A)`

, we
recursively try to prove `Implemented(?X: A)`

and `Implemented(?X: B)`

, which
are both ambiguous, 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).