ゴールと節

論理プログラミングの用語では、ゴールとは証明しなければならないものであり、節とは真であることが分かっているものです。論理への lowering の章で説明したように、Rust のトレイトソルバーは hereditary harrop (HH) 節の拡張に基づいています。これは、従来の Prolog のホーン節にいくつかの新しい強力な機能を加えたものです。

ゴールと節のメタ構造

Rust のソルバーでは、ゴールと節は次の形式を取ります（2 つの定義が互いを参照していることに注意してください）。

Goal = DomainGoal           // 下のセクションで定義
        | Goal && Goal
        | Goal || Goal
        | exists<K> { Goal }   // 存在量化
        | forall<K> { Goal }   // 全称量化
        | if (Clause) { Goal } // 含意
        | true                 // 自明に真であるもの
        | ambiguous            // 決して証明できないもの

Clause = DomainGoal
        | Clause :- Goal     // Goal を証明できるなら、Clause は真
        | Clause && Clause
        | forall<K> { Clause }

K = <type>     // 「種別」
    | <lifetime>

この種のゴールに対する証明手続きは、実際にはかなり単純です。本質的には、深さ優先探索の一種です。論文 “A Proof Procedure for the Logic of Hereditary Harrop Formulas” に詳細があります。

コード上では、これらの型は rustc では rustc_middle/src/traits/mod.rs に、chalk では chalk-ir/src/lib.rs に定義されています。

ドメインゴール

ドメインゴールは、トレイト論理の原子です。上で示した定義から分かるように、一般的なゴールは基本的にドメインゴールの組み合わせで構成されます。

さらに、前述の節の定義を少し平坦化すると、節は常に次の形式であることが分かります。

forall<K1, ..., Kn> { DomainGoal :- Goal }

したがって、ドメインゴールは実際には節の左辺です。つまり、最も粒度の細かいレベルでは、ドメインゴールこそがトレイトソルバーが最終的に証明しようとするものです。

このシステムにおけるドメインゴールの集合を定義するには、まずいくつかの単純な定式化を導入する必要があります。トレイト参照は、トレイトの名前と、適切な入力の集合 P0..Pn から構成されます。

TraitRef = P0: TraitName<P1..Pn>

たとえば、u32: Display はトレイト参照であり、Vec<T>: IntoIterator も同様です。Rust の表層構文では、関連型束縛（Vec<T>: IntoIterator<Item = T>）のような追加のものも許可されていますが、それらはトレイト参照の一部ではないことに注意してください。

射影は、関連アイテム参照とその入力 P0..Pm から構成されます。

Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>

これらを踏まえると、DomainGoal は次のように定義できます。

DomainGoal = Holds(WhereClause)
            | FromEnv(TraitRef)
            | FromEnv(Type)
            | WellFormed(TraitRef)
            | WellFormed(Type)
            | Normalize(Projection -> Type)

WhereClause = Implemented(TraitRef)
            | ProjectionEq(Projection = Type)
            | Outlives(Type: Region)
            | Outlives(Region: Region)

WhereClause は、Rust ユーザーが実際に Rust プログラムで記述できる where 節を指します。この抽象化は、実質的に Rust で記述可能なドメインゴールだけを扱いたい場合があるため、便宜上存在しています。

これらを 1 つずつ分解して見ていきましょう。

Implemented(TraitRef)

例: Implemented(i32: Copy)

与えられたトレイトが、与えられた入力型およびライフタイムに対して実装されている場合に真です。

ProjectionEq(Projection = Type)

例: ProjectionEq<T as Iterator>::Item = u8

与えられた関連型 Projection は Type と等しい、ということです。これは正規化、またはプレースホルダー関連型を使用して証明できます。Chalk Book の関連型に関するセクションを参照してください。

Normalize(Projection -> Type)

例: ProjectionEq<T as Iterator>::Item -> u8

与えられた関連型 Projection は Type に正規化できます。

Chalk Book の関連型に関するセクションで説明されているように、Normalize は ProjectionEq を含意しますが、その逆は成り立ちません。一般に、Normalize(<T as Trait>::Item -> U) を証明するには、Implemented(T: Trait) の証明も必要です。

FromEnv(TraitRef)

例: FromEnv(Self: Add<i32>)

内側の TraitRef が真であると仮定されている場合、つまり、スコープ内の where 節から導出できる場合に真です。

たとえば、次の関数があるとします。

#![allow(unused)]
fn main() {
fn loud_clone<T: Clone>(stuff: &T) -> T {
    println!("cloning!");
    stuff.clone()
}
}

この関数の本体内では、FromEnv(T: Clone) を持つことになります。スコープ内の where 節は入れ子になるため、impl 本体の内側にある関数本体は、その impl 本体の where 節も継承します。

このルールと次のルールは、implied bounds を実装するために使用されます。lowering に関するセクションで見るように、FromEnv(TraitRef) は Implemented(TraitRef) を含意しますが、その逆は成り立ちません。この区別は implied bounds にとって重要です。

FromEnv(Type)

例: FromEnv(HashSet<K>)

内側の Type が well-formed であると仮定されている場合、つまり、それが関数または impl の入力型である場合に真です。

たとえば、次のコードがあるとします。

struct HashSet<K> where K: Hash { ... }

fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
    println!("inserting!");
    set.insert(item);
}

HashSet<K> は loud_insert 関数の入力型です。したがって、これは well-formed であると仮定されるため、この関数の本体内では FromEnv(HashSet<K>) を持つことになります。lowering に関するセクションで見るように、HashSet 宣言は K: Hash という where 節とともに記述されているため、FromEnv(HashSet<K>) は Implemented(K: Hash) を含意します。したがって、loud_insert 関数でその bound を繰り返す必要はありません。むしろ、それが真であると自動的に仮定します。

WellFormed(Item)

これらのゴールは、与えられたアイテムが well-formed であることを含意します。

well-formed であるアイテムには、さまざまな種類があります。

型、たとえば Rust では真である WellFormed(Vec<i32>) や、真ではない WellFormed(Vec<str>)（str が Sized ではないため）などです。
TraitRef、たとえば WellFormed(Vec<i32>: Clone) などです。

well-formedness は implied bounds にとって重要です。特に、loud_clone の例で FromEnv(T: Clone) を仮定してよい理由は、loud_clone の各呼び出し箇所について also WellFormed(T: Clone) を検証するためです。同様に、loud_insert の例で FromEnv(HashSet<K>) を仮定してよい理由は、loud_insert の各呼び出し箇所について WellFormed(HashSet<K>) を検証するためです。

Outlives(Type: Region), Outlives(Region: Region)

例: Outlives(&'a str: 'b), Outlives('a: 'static) 与えられた左側の型またはリージョンが、右側のリージョンより長く存続する場合に真です。

余帰納的ゴール

私たちのシステムにおけるほとんどのゴールは「帰納的」です。帰納的ゴールでは、循環論法は許可されません。次の例の節を考えてみましょう。

    Implemented(Foo: Bar) :-
        Implemented(Foo: Bar).

帰納的に考えると、この節は役に立ちません。Implemented(Foo: Bar) を証明しようとすると、その後再帰的に Implemented(Foo: Bar) を証明しなければならず、その循環は無限に続くことになります（trait solver はここで終了しますが、単に Implemented(Foo: Bar) が真であることはわかっていないと見なします）。

しかし、一部のゴールは余帰納的です。簡単に言えば、これは循環しても問題ないという意味です。そのため、もし Bar が余帰納的トレイトであれば、上のルールは完全に妥当であり、Implemented(Foo: Bar) が真であることを示します。

Auto traits は、Rust で余帰納的ゴールが使われる一例です。Send トレイトを考え、次の構造体があると想像してください。

#![allow(unused)]
fn main() {
struct Foo {
    next: Option<Box<Foo>>
}
}

auto traits のデフォルトルールでは、フィールドの型が Send であれば Foo は Send であるとされます。したがって、次のようなルールがあります。

Implemented(Foo: Send) :-
    Implemented(Option<Box<Foo>>: Send).

想像できると思いますが、Option<Box<Foo>>: Send を証明しようとすると、結局 Foo: Send をもう一度証明することが循環的に必要になります。したがって、これは循環に陥る例です。しかし、それで問題ありません。自己参照しているにもかかわらず、Foo: Send が成り立つと見なします。

一般に、余帰納的トレイトは、可能性の固定集合を列挙したい場合に Rust のトレイト解決で使用されます。auto traits の場合、与えられた開始点から到達可能な型の集合を列挙しています（つまり、Foo は型 Option<Box<Foo>> の値に到達でき、それは型 Box<Foo> の値に到達できることを意味し、さらに型 Foo の値に到達でき、そこで循環が完了します）。

auto traits に加えて、WellFormed 述語も余帰納的です。これらは、暗黙の境界のセクションで説明されているように、同様の「すべてのケースを列挙する」パターンを実現するために使用されます。

未完成の章

今後記述する予定のトピック:

証明手続きを詳しく説明する
SLG 解法 – 否定的推論を導入する

Keyboard shortcuts

Rust Compiler Development Guide