余帰納法

トレイトソルバーは、ゴールを証明するときに余帰納法を使うことがあります。余帰納法はかなり繊細なので、独立した章として扱います。

余帰納法と帰納法

帰納法では、有限の証明木に到達するまで再帰的に証明を適用します。次の木になる Vec<Vec<Vec<u32>>>: Debug の例を考えてみましょう。

Vec<Vec<Vec<u32>>>: Debug
- Vec<Vec<u32>>: Debug
  - Vec<u32>: Debug
    - u32: Debug

この木は有限です。しかし、成り立ってほしいすべてのゴールが有限の証明木を持つわけではありません。次の例を考えてみましょう。

#![allow(unused)]
fn main() {
struct List<T> {
    value: T,
    next: Option<Box<List<T>>>,
}
}

List<T>: Send が成り立つには、そのすべてのフィールドも再帰的に Send を実装していなければなりません。これは次の証明木になります。

List<T>: Send
- T: Send
- Option<Box<List<T>>>: Send
  - Box<List<T>>: Send
    - List<T>: Send
      - T: Send
      - Option<Box<List<T>>>: Send
        
        Box<List<T>>: Send
        
        …

この木は無限に大きくなりますが、まさにこれこそが余帰納法の扱う対象です。

ゴールを帰納的に証明するには、そのゴールに対して有限の証明木を提示する必要があります。ゴールを余帰納的に証明する場合、提示される証明木は無限であってもかまいません。

なぜ余帰納法は正しいのか

あるトレイトゴールが成り立つかどうかを確認するとき、私たちは「この境界を満たす impl は存在するか」を問うています。ネストしたゴールの無限の連鎖がある場合でも、使用されるべき一意の impl は依然として存在します。

余帰納法を実装する方法

私たちの実装では、無限の木を構築しようとして余帰納法を確認することはできません。それには無限のリソースが必要になるためです。それでも、この観点から余帰納法を考えることには意味があります。

無限の木を確認することはできないため、代わりに、無限の証明木になると分かっているパターンを探します。現在検出しているパターンは（正準）サイクルです。T: Send が T: Send に依存しているなら、それが永遠に続くだけであることはかなり明らかです。

サイクルを扱う場合、キャッシュには注意が必要です。リージョンと推論変数の正準化により、サイクルに遭遇したからといって、無限の証明木が得られるとは限らないためです。次の例を見てみましょう。

#![allow(unused)]
fn main() {
trait Foo {}
struct Wrapper<T>(T);

impl<T> Foo for Wrapper<Wrapper<T>>
where
    Wrapper<T>: Foo
{} 
}

Wrapper<?0>: Foo を証明すると、impl<T> Foo for Wrapper<Wrapper<T>> という impl が使われ、これによって ?0 は Wrapper<?1> に制約され、その後 Wrapper<?1>: Foo が要求されます。正準化により、これはサイクルとして検出されます。

解決の考え方は、サイクルを検出するたびに暫定結果を返し、そのゴールの暫定結果が最終結果と等しくなるまでゴールを繰り返し再試行することです。最初は制約なしの Yes を結果として使用し、再実行が必要になるたびに前回の反復の結果へ更新します。

TODO: ここを詳述する。余帰納的サイクルについては chalk と同じアプローチを使用しています。なお、帰納的サイクルの扱いは現在、単に Overflow を返すという点で異なります。 chalk book の関連する章を参照してください。

今後の作業

現在は、自動トレイト、Sized、および WF ゴールのみを余帰納的と見なしています。将来的には、ほぼすべてのゴールを余帰納的にするつもりです。まず、より多くの余帰納的証明を許可することがなぜ望ましいのかを詳しく説明します。

再帰的データ型はすでに余帰納法に依存している…

…ただし、トレイトソルバー内ではそれを避ける傾向があります。

#![allow(unused)]
fn main() {
enum List<T> {
    Nil,
    Succ(T, Box<List<T>>),
}

impl<T: Clone> Clone for List<T> {
    fn clone(&self) -> Self {
        match self {
            List::Nil => List::Nil,
            List::Succ(head, tail) => List::Succ(head.clone(), tail.clone()),
        }
    }
}
}

この impl では tail.clone() を使用しています。このためには Box<List<T>>: Clone を証明する必要があり、それには List<T>: Clone が必要ですが、それは現在確認している impl に依存しています。その要件を impl の where 句に追加すると、これは perfect derive で行うことですが、そのサイクルがトレイトソルバーに移動し、エラーが発生します。

再帰的データ型

射影を含む再帰型について推論するためにも余帰納法が必要です。たとえば、次のコードは有効であるべきにもかかわらず、現在はコンパイルに失敗します。

#![allow(unused)]
fn main() {
use std::borrow::Cow;
pub struct Foo<'a>(Cow<'a, [Foo<'a>]>);
}

この問題は少なくとも 2015 年から知られています。詳しく知りたい場合は #23714 を参照してください。

明示的に確認される暗黙の境界

impl を確認するとき、impl ヘッダー内の型は整形式であると仮定します。これは、その impl をインスタンス化して使うときに、それが実際にそうであることを証明しなければならないことを意味します。 #100051 は、これが成り立っていないことを示しています。これを修正するには、impl ヘッダー内の型に対して WF 述語を追加する必要があります。すべてのトレイトに対する余帰納法がなければ、これは core さえ壊してしまいます。

#![allow(unused)]
fn main() {
trait FromResidual<R> {}
trait Try: FromResidual<<Self as Try>::Residual> {
    type Residual;
}

struct Ready<T>(T);
impl<T> Try for Ready<T> {
    type Residual = Ready<()>;
}
impl<T> FromResidual<<Ready<T> as Try>::Residual> for Ready<T> {}
}

FromResidual の impl が整形式であることを確認すると、次のサイクルが発生します。

impl は、<Ready<T> as Try>::Residual と Ready<T> が整形式である場合に整形式です。

wf(<Ready<T> as Try>::Residual) は次を要求します
Ready<T>: Try。これはスーパートレイトにより次を要求します
Ready<T>: FromResidual<Ready<T> as Try>::Residual>、impl に対する暗黙の境界のため
wf(<Ready<T> as Try>::Residual) :tada: サイクル

余帰納法をより多くのゴールへ拡張する際の問題

余帰納法を拡張する際には、留意すべき追加の問題がいくつかあります。ここでの問題は、現在のソルバーには関係ありません。

暗黙のスーパートレイト境界

現在のトレイトシステムは、trait Trait: SuperTrait のようなスーパートレイトを、1) Trait を実装するすべての型について SuperTrait が成り立つことを要求し、2) Trait が成り立つなら SuperTrait も成り立つと仮定する、という形で扱っています。

を証明している間に 2) に依存するのは健全ではありません。これは余帰納的サイクルの場合にのみ観測できます。サイクルがなければ、2) に依存するたびに、使用された Trait の impl について、2) に依存せずに 1) も証明しているはずだからです。

#![allow(unused)]
fn main() {
trait Trait: SuperTrait {}

impl<T: Trait> Trait for T {}

// 余帰納法について現在の構成を維持すると
// これのコンパイルが許可されてしまいます。うーん :<
fn sup<T: SuperTrait>() {}
fn requires_trait<T: Trait>() { sup::<T>() }
fn generic<T>() { requires_trait::<T>() }
}

これは余帰納法に本質的なものというよりも、余帰納法によって不健全になる既存の性質です。

考えられる解決策

これを解決する最も簡単な方法は、2) を完全に削除し、常にトレイトソルバーの外側で T: Trait を T: Trait と T: SuperTrait に elaboration することです。これにより 1) も削除できるようになりますが、トレイト上の通常の where 境界は依然として証明する必要があるため、それは追加の作業にすぎません。

をチェックするときに 2) の循環的な使用を無効化する方法は想像できるかもしれませんが、少なくとも私（@lcnr）の考えでは、どれも合理的とは言えないほど複雑すぎます。

`normalizes_to` ゴールと進捗

normalizes_to ゴールは、<T as Trait>::Assoc が何らかの U に正規化されるという要件を表します。これは事実上、まず <T as Trait>::Assoc を正規化し、次にその結果の型を U と等置することで実現されます。各射影はちょうど 1 つの型に正規化されるべきなので、これはマッピングであるべきです。単に無限の証明木を許可すると、次のような振る舞いになります。

#![allow(unused)]
fn main() {
trait Trait {
    type Assoc;
}

impl Trait for () {
    type Assoc = <() as Trait>::Assoc;
}
}

ここで normalizes_to(<() as Trait>::Assoc, Vec<u32>) を計算すると、impl が解決され、関連型 <() as Trait>::Assoc が得られます。次に、それを期待される型と等置するため、再び normalizes_to(<() as Trait>::Assoc, Vec<u32>) をチェックすることになります。これは永遠に続き、結果として無限の証明木になります。

これは、<() as Trait>::Assoc が他の任意の型と等しくなってしまうことを意味し、健全ではありません。

これを解決する方法

警告: これは微妙であり、間違っている可能性があります

トレイトゴールとは異なり、normalizes_to は productive¹ でなければなりません。 normalizes_to ゴールは、射影が rigid な型コンストラクタに正規化された時点で productive になります。したがって、<() as Trait>::Assoc が Vec<<() as Trait>::Assoc> に正規化される場合は productive になります。

normalizes_to ゴールには 2 種類のネストしたゴールがあります。射影を実際に正規化するために必要なネストした要件と、正規化された射影と期待される型との等価性です。productive でなければならないのは等価性だけです。証明木のある分岐は、それが有限であるか、エイリアスが rigid な型コンストラクタに解決される normalizes_to を少なくとも 1 つ含む場合に productive です。

あるいは、単純に normalizes_to の equate 分岐を常に帰納的として扱うこともできます。どのような循環も無限型をもたらすはずですが、無限型はいずれにせよサポートされておらず、 codegen のために深く正規化する際にオーバーフローを引き起こすだけです。

実験と例: https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view

要約の別の試み。

projection eq では、rhs を制約することで進捗を得なければならない
循環が許容されるのは、等置中に正規化後の lhs 上に少なくとも一度 rigid ty がある場合だけである
normalizes_to の再帰的な eq 呼び出しの外側にある循環は常に問題ない

関連: https://coq.inria.fr/refman/language/core/coinductive.html#top-level-definitions-of-corecursive-functions ↩

Keyboard shortcuts

Rust Compiler Development Guide